Theorem: LoVe.Fraction.ext (LoVe/Labs/Lab9Solution.lean)

State before:
a b : Fraction
hnum : a.num = b.num
hdenom : a.denom = b.denom
⊢ a = b
Tactic:
cases a with
| mk na da =>
  cases b with
  | mk nb db =>
    simp at *
    exact And.intro hnum hdenom
State after:
no goals

State before:
case mk
b : Fraction
na da : ℤ
denom_Neq_zero✝ : da ≠ 0
hnum : { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ }.num = b.num
hdenom : { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ }.denom = b.denom
⊢ { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ } = b
Tactic:
cases b with
| mk nb db =>
  simp at *
  exact And.intro hnum hdenom
State after:
no goals

State before:
case mk.mk
na da : ℤ
denom_Neq_zero✝¹ : da ≠ 0
nb db : ℤ
denom_Neq_zero✝ : db ≠ 0
hnum :
  { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝¹ }.num =
    { num := nb, denom := db, denom_Neq_zero := denom_Neq_zero✝ }.num
hdenom :
  { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝¹ }.denom =
    { num := nb, denom := db, denom_Neq_zero := denom_Neq_zero✝ }.denom
⊢ { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝¹ } =
    { num := nb, denom := db, denom_Neq_zero := denom_Neq_zero✝ }
Tactic:
simp at *
State after:
case mk.mk
na da : ℤ
denom_Neq_zero✝¹ : da ≠ 0
nb db : ℤ
denom_Neq_zero✝ : db ≠ 0
hnum : na = nb
hdenom : da = db
⊢ na = nb ∧ da = db

State before:
case mk.mk
na da : ℤ
denom_Neq_zero✝¹ : da ≠ 0
nb db : ℤ
denom_Neq_zero✝ : db ≠ 0
hnum : na = nb
hdenom : da = db
⊢ na = nb ∧ da = db
Tactic:
exact And.intro hnum hdenom
State after:
no goals