Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.solution (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0 : 3 ≠ 0
h : 1 = 0
⊢ 3 = 0
Tactic:
have h0 := hf.map_one
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : f 1 = 0
⊢ 3 = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : f 1 = 0
⊢ 3 = 0
Tactic:
rw [h, hf.map_zero, neg_eq_zero] at h0
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : 1 = 0
⊢ 3 = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : 1 = 0
⊢ 3 = 0
Tactic:
rw [← mul_one 3, h0, mul_zero]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
h1 : Function.Bijective 𝔽₃.cast
⊢ f 𝔽₃.𝔽₃0.cast = ↑(𝔽₃Map2 𝔽₃.𝔽₃0)
Tactic:
change f 0 = ((-1 : ℤ) : S)
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
h1 : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)

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