Theorem: IMOSL.IMO2012A5.zero_is_good (IMOSLLean4/IMO2012/A5/A5Answers/ZeroMap.lean)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
x✝¹ x✝ : R
⊢ (fun x => 0) (x✝¹ * x✝ + 1) = (fun x => 0) x✝¹ * (fun x => 0) x✝ + (fun x => 0) (x✝¹ + x✝)
Tactic:
rw [add_zero, zero_mul]
State after:
no goals