Theorem: AlmostHom.add_comp (RealsQuasiMorphisms/Ring.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
⊢ AlmostHom.comp (f₁ + f₂) g = AlmostHom.comp f₁ g + AlmostHom.comp f₂ g
Tactic:
ext
State after:
case a.h
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
x✝ : G
⊢ toFun (AlmostHom.comp (f₁ + f₂) g) x✝ = toFun (AlmostHom.comp f₁ g + AlmostHom.comp f₂ g) x✝

State before:
case a.h
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
x✝ : G
⊢ toFun (AlmostHom.comp (f₁ + f₂) g) x✝ = toFun (AlmostHom.comp f₁ g + AlmostHom.comp f₂ g) x✝
Tactic:
rfl
State after:
no goals