Theorem: IMOSL.IMO2012A5.NontrivialGood.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
hf : NontrivialGood f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
⊢ (⇑φ ∘ f) 0 + 1 = 0
Tactic:
rw [← φ.map_one, ← φ.map_zero, ← hf.map_zero_add_one, φ.map_add]
State after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
hf : NontrivialGood f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
⊢ (⇑φ ∘ f) 0 + φ 1 = φ (f 0) + φ 1

State before:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
f : R → S
S₀ : Type u_1
hf : NontrivialGood f
inst✝ : NonAssocSemiring S₀
φ : S →+* S₀
⊢ (⇑φ ∘ f) 0 + φ 1 = φ (f 0) + φ 1
Tactic:
rfl
State after:
no goals