How to prove equality of `structure`s?

Stream: lean4

[Ian Wood]

I'm trying to create basic rational numbers:

structure Rat where
  num : Int
  den : Nat
  non_zero : den ≠ 0

theorem nat_mul_zero : ∀ (a b : Nat), a * b = 0 → (a = 0 ∨ b = 0) := sorry

def rat_add (a b : Rat) := Rat.mk (a.num * b.den + b.num * a.den) (a.den * b.den) (by
  intro h
  match nat_mul_zero _ _ h with
  | Or.inl h => exact a.non_zero h
  | Or.inr h => exact b.non_zero h)

instance : Add Rat where
  add := rat_add

theorem rat_add_comm (a b : Rat) : a + b = b + a := by
  exact sorry -- issue is here

The problem I'm running into is I can't see how to convert the goal a + b = b + a into the two goals (a.num * b.den + b.num * a.den) = (b.num * a.den + a.num * b.den) and (a.den * b.den) = (b.den * a.den). How can I do this?

[Yakov Pechersky]

You should write an extensionality lemma. It will involve doing cases on a and cases on b

[Ian Wood]

Yakov Pechersky said:

You should write an extensionality lemma. It will involve doing cases on a and cases on b

That worked, thank you!

[Justus Springer]

You are aware that what you're defining isn't yet a representation of the rational numbers? You are missing the relation Rat.mk x x = Rat.mk 1 1.

[Ian Wood]

Justus Springer said:

You are aware that what you're defining isn't yet a representation of the rational numbers? You are missing the relation Rat.mk x x = Rat.mk 1 1.

Yes, this is the first thing I thought to do to try out lean4. I don't plan to make it correct really.

[Casavaca]

I also came into this.

structure NatWrap where
  i : Nat := 0
  j : Nat := 0

example (a b : NatWrap) (h₁ : a.i = b.i) (h₂ : a.j = b.j) : a = b := by
  ???; exact h₁; exact h₂

Is there a tactic to convert the goal a=b into a list of goals a.i = b.i, a.j = b.j?

[Yaël Dillies]

This is called extensionality. If you tag natWrap with ext, then Lean will automatically generate an extensionality lemma for you. Then the tactic ext will call it for you.