Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.solution (IMOSLLean4/IMO2012/A5/A5Cases/Case1.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : 1 = 0
⊢ f (-1) = 0
Tactic:
rw [h, neg_zero, ← h, hf.map_one]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : Function.Bijective 𝔽₃.cast
⊢ f 𝔽₃.𝔽₃0.cast = ↑(𝔽₃Map1 𝔽₃.𝔽₃0)
Tactic:
change f 0 = ((-1 : ℤ) : S)
State after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
State after:
no goals