Theorem: IMOSL.IMO2012A5.good_hom_comp (IMOSLLean4/IMO2012/A5/A5General/A5Hom.lean)

State before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
x y : R
⊢ (⇑φ ∘ f) (x * y + 1) = (⇑φ ∘ f) x * (⇑φ ∘ f) y + (⇑φ ∘ f) (x + y)
Tactic:
simp only [Function.comp_apply]
State after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
x y : R
⊢ φ (f (x * y + 1)) = φ (f x) * φ (f y) + φ (f (x + y))

State before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
x y : R
⊢ φ (f (x * y + 1)) = φ (f x) * φ (f y) + φ (f (x + y))
Tactic:
rw [h, φ.map_add, φ.map_mul]
State after:
no goals