Theorem: LoVe.Fraction.Setoid_mul (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] 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.num * (a'.denom * b'.denom) = a'.num * b'.num * (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.num * (a'.denom * b'.denom) = a'.num * b'.num * (a.denom * b.denom)
Tactic:
calc
  num a * num b * (denom a' * denom b')
  = (num a * denom a') * (num b * denom b') :=
    by ac_rfl
  _ = (num a' * denom a) * (num b' * denom b) :=
    by simp [*]
  _ = num a' * num b' * (denom a * denom b) :=
    by 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.num * (a'.denom * b'.denom) = a.num * a'.denom * (b.num * b'.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.num * b'.denom) = a'.num * a.denom * (b'.num * b.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'.num * b.denom) = a'.num * b'.num * (a.denom * b.denom)
Tactic:
ac_rfl
State after:
no goals