Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₄_iff (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
r : R
⊢ r * (r + 1) + 1 = 0 ↔ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1
Tactic:
rw [reduced_eq_zero_iff hS hf, Eq1 hf.toNontrivialGood, iff_and_self]
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
r : R
⊢ f r * f (r + 1) = -1 → f r + f (r + 1) = 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
r : R
⊢ f r * f (r + 1) = -1 → f r + f (r + 1) = 1
Tactic:
intro 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
r : R
h : f r * f (r + 1) = -1
⊢ f r + f (r + 1) = 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
r : R
h : f r * f (r + 1) = -1
⊢ f r + f (r + 1) = 1
Tactic:
refine (main_cases hS hf.toNontrivialGood r).elim (λ h0 ↦ ?_) And.left
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
r : R
h : f r * f (r + 1) = -1
h0 : f r = 0 ∨ f (r + 1) = 0
⊢ f r + f (r + 1) = 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
r : R
h : f r * f (r + 1) = -1
h0 : f r = 0 ∨ f (r + 1) = 0
⊢ f r + f (r + 1) = 1
Tactic:
rw [← mul_eq_zero, h, neg_eq_zero] at h0
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
r : R
h : f r * f (r + 1) = -1
h0 : 1 = 0
⊢ f r + f (r + 1) = 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
r : R
h : f r * f (r + 1) = -1
h0 : 1 = 0
⊢ f r + f (r + 1) = 1
Tactic:
rw [← mul_one (_ + _), h0, mul_zero]
State after:
no goals