Theorem: LoVe.Fraction.Setoid_inv (LoVe/Lectures/LoVe14_RationalAndRealNumbers_Demo.lean)

State before:
a a' : Fraction
ha : a ≈ a'
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
cases Classical.em (num a = 0) with
| inl ha0 =>
  cases Classical.em (num a' = 0) with
  | inl ha'0 =>
    simp [ha0, ha'0, inv_zero]
  | inr ha'0 =>
    simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
| inr ha0 =>
  cases Classical.em (num a' = 0) with
  | inl ha'0 =>
    simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
  | inr ha'0 =>
    simp [Setoid_Iff, ha0, ha'0] at *
    linarith
State after:
no goals

State before:
case inl
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
cases Classical.em (num a' = 0) with
| inl ha'0 =>
  simp [ha0, ha'0, inv_zero]
| inr ha'0 =>
  simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
State after:
no goals

State before:
case inl.inl
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
ha'0 : a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [ha0, ha'0, inv_zero]
State after:
no goals

State before:
case inl.inr
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
ha'0 : ¬a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
State after:
no goals

State before:
case inr
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
cases Classical.em (num a' = 0) with
| inl ha'0 =>
  simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
| inr ha'0 =>
  simp [Setoid_Iff, ha0, ha'0] at *
  linarith
State after:
no goals

State before:
case inr.inl
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
ha'0 : a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
State after:
no goals

State before:
case inr.inr
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
ha'0 : ¬a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [Setoid_Iff, ha0, ha'0] at *
State after:
case inr.inr
a a' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
ha0 ha'0 : True
⊢ a.denom * a'.num = a'.denom * a.num

State before:
case inr.inr
a a' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
ha0 ha'0 : True
⊢ a.denom * a'.num = a'.denom * a.num
Tactic:
linarith
State after:
no goals