Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂_solution (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : 1 = 0
⊢ 2 = 0
Tactic:
apply congrArg f at h
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : f 1 = f 0
⊢ 2 = 0

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : f 1 = f 0
⊢ 2 = 0
Tactic:
rw [hf.map_one, hf.map_zero, zero_eq_neg] at h
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : 1 = 0
⊢ 2 = 0

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : 1 = 0
⊢ 2 = 0
Tactic:
rw [← mul_one 2, h, mul_zero]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : Function.Bijective 𝔽₂.cast
⊢ f 𝔽₂.O.cast = ↑(𝔽₂Map 𝔽₂.O)
Tactic:
change f 0 = ((-1 : ℤ) : S)
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : Function.Bijective 𝔽₂.cast
⊢ f 0 = ↑(-1)

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
hR : ∀ (r : R), r = 0 ∨ r = 1
h : Function.Bijective 𝔽₂.cast
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
State after:
no goals