In Lean 4 how to substitute equals in an expression with other variables?

Question

I can use 'subst' to prove that if a=b and a is positive then b is positive:

example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2

How do I prove that if a=b and a > c then b > c:

example (a b c: Peano) (h1 : a = b) (h2 : gt a c) : gt b c := Eq.subst h1 h2 -- does not work

Note that I am learning Lean 4 by using my own 'Peano' natural numbers, so I only want a solution that uses non-numeric tactics (i.e. propositional logic and equality). It appears that 'congr' or 'congrArg' may help (do I need to specify a lambda expression?) but I have not succeeded.

Answer 1

I recommend the ▸ macro, which you can write using \t in VSCode.

-- definitions of Peano and gt don't matter here
axiom Peano : Type  
axiom gt (a b : Peano): Prop

example (a b c : Peano) (h1 : a = b) (h2 : gt a c) : gt b c :=
  h1 ▸ h2

The macro is quite flexible and can be used in a number of situations where you want to do substitution using an equality.

As for the more direct approach, I'm not sure why Eq.subst h1 h2 doesn't work, but if you fill in all the implicit arguments it works:

example (a b c : Peano) (h1 : a = b) (h2 : gt a c) : gt b c :=
  @Eq.subst Peano (fun x => gt x c) a b h1 h2

If you are fine with the rewrite tactic (which is a purely logical tactic), then that works well also:

example (a b c : Peano) (h1 : a = b) (h2 : gt a c) : gt b c := by
  rewrite [<- h1]
  exact h2

---

As for learning how equality actually works in Lean, I highly recommend you read the Equality section in Theorem Proving in Lean 4.

In particular, equality is defined inductively (just like the natural numbers) with one constructor refl. You can even define your own version:

inductive MyEq : α → α → Prop where
  | refl (a : α) : MyEq a a

Since it is an inductive, we can use induction (sometimes called "path induction"):

example (a b c : Peano) (h1 : MyEq a b) (h2 : gt a c) : gt b c := by 
  induction h1
  exact h2

The idea is that if we can construct or prove P a and we have MyEq a b, then we can construct or prove P b as well.

This is also easy to write as a case analysis using the single refl constructor for MyEq.

example (a b c : Peano) (h1 : MyEq a b) (h2 : gt a c) : gt b c :=
  match h1 with
  | MyEq.refl a => h2

Finally, if you really want to get to the very inner guts of Lean, you can directly use the rec recursor (which I don't recommend for actual Lean code, but in this case, it is really simple to use).

example (a b c : Peano) (h1 : MyEq a b) (h2 : gt a c) : gt b c :=
  MyEq.rec h2 h1