Theorem: EudoxusReal.mul_comm (RealsQuasiMorphisms/Ring.lean)

State before:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ AlmostHom.comp f₁ f₂ ≈ AlmostHom.comp f₂ f₁
Tactic:
show (QuotientAddGroup.leftRel ..).r ..
State after:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Setoid.r (AlmostHom.comp f₁ f₂) (AlmostHom.comp f₂ f₁)

State before:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Setoid.r (AlmostHom.comp f₁ f₂) (AlmostHom.comp f₂ f₁)
Tactic:
rewrite [QuotientAddGroup.leftRel_apply]
State after:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ -AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁ ∈ boundedAlmostHoms ℤ

State before:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ -AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁ ∈ boundedAlmostHoms ℤ
Tactic:
exact AlmostHom.comp_almost_comm f₁ f₂
State after:
no goals