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

State before:
a a' b b' : Fraction
ha : a ≈ a'
hb : b ≈ b'
⊢ a + b ≈ a' + b'
Tactic:
simp [Setoid_Iff, add_denom, add_num] at *
State after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)

State before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)
Tactic:
calc
  (num a * denom b + num b * denom a)
      * (denom a' * denom b')
  = num a * denom a' * denom b * denom b'
    + num b * denom b' * denom a * denom a' :=
    by
      simp [add_mul, mul_add]
      ac_rfl
  _ = num a' * denom a * denom b * denom b'
        + num b' * denom b * denom a * denom a' :=
    by simp [*]
  _ = (num a' * denom b' + num b' * denom a')
        * (denom a * denom b) :=
    by
      simp [add_mul, mul_add]
      ac_rfl
State after:
no goals

State before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom
Tactic:
simp [add_mul, mul_add]
State after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.denom * (a'.denom * b'.denom) + b.num * a.denom * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom

State before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.denom * (a'.denom * b'.denom) + b.num * a.denom * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom
Tactic:
ac_rfl
State after:
no goals

State before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom =
    a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom
Tactic:
simp [*]
State after:
no goals

State before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)
Tactic:
simp [add_mul, mul_add]
State after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    a'.num * b'.denom * (a.denom * b.denom) + b'.num * a'.denom * (a.denom * b.denom)

State before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    a'.num * b'.denom * (a.denom * b.denom) + b'.num * a'.denom * (a.denom * b.denom)
Tactic:
ac_rfl
State after:
no goals