Theorem: IMOSL.IMO2012A5.good_comp_hom (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
R₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring R₀
φ : R₀ →+* R
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
R₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring R₀
φ : R₀ →+* R
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
R₀ : Type u_1
h : good f
inst✝ : NonAssocSemiring R₀
φ : R₀ →+* R
x y : R₀
⊢ f (φ (x * y + 1)) = f (φ x) * f (φ y) + f (φ (x + y))
Tactic:
rw [φ.map_add, φ.map_mul, φ.map_one, h, φ.map_add]
State after:
no goals