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
r : R
hr : r * (r + 1) + 1 = 0
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
have X : (1 : R) ≠ 0 := λ X ↦ hS <| by
  apply congrArg f at X; rw [hf.map_one, hf.map_zero, zero_eq_neg] at X
  rw [← mul_one 2, X, mul_zero]
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
obtain ⟨hr0, hr1⟩ := (reduced_𝔽₄_iff hS hf).mp hr
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
have hr' : r * r + r = 1 := by rwa [← mul_add_one r, ← add_eq_zero_iff_eq]
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
rw [← eq_sub_iff_add_eq'] at hr0
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
rw [hr0, ← neg_sub, mul_neg, neg_inj, mul_sub_one, sub_eq_iff_eq_add'] at hr1
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
let ι := ℤφ.castRingHom hr1
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
have h0 : ∀ x, f (𝔽₄.cast r x) = ι (𝔽₄Map x)
  | 𝔽₄.O => by change f 0 = ι (-1)
               rw [hf.map_zero, ι.map_neg, ι.map_one]
  | 𝔽₄.I => (hf.map_one).trans ι.map_zero.symm
  | 𝔽₄.X => (ℤφ.cast_φ _).symm
  | 𝔽₄.Y => by change f (r + 1) = ((1 : ℤ) : S) + (-1 : ℤ) • f r
               rw [Int.cast_one, neg_one_zsmul, hr0, sub_eq_add_neg]
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
let ρ := RingEquiv.ofBijective (𝔽₄.castRingHom hr') h
State after:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
ρ : 𝔽₄ ≃+* R := RingEquiv.ofBijective (𝔽₄.castRingHom hr') h
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))

State before:
case intro
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
ρ : 𝔽₄ ≃+* R := RingEquiv.ofBijective (𝔽₄.castRingHom hr') h
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
exact ⟨ρ.symm, ι, λ x ↦ h0 _ ▸ congrArg f (Equiv.apply_symm_apply ρ.toEquiv _).symm⟩
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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 = 0
⊢ 2 = 0
Tactic:
apply congrArg f at X
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
hr : r * (r + 1) + 1 = 0
X : 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
r : R
hr : r * (r + 1) + 1 = 0
X : f 1 = f 0
⊢ 2 = 0
Tactic:
rw [hf.map_one, hf.map_zero, zero_eq_neg] at X
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
hr : r * (r + 1) + 1 = 0
X : 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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 = 0
⊢ 2 = 0
Tactic:
rw [← mul_one 2, X, 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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
⊢ r * r + r = 1
Tactic:
rwa [← mul_add_one r, ← add_eq_zero_iff_eq]
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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
⊢ Function.Bijective (𝔽₄.cast r)
Tactic:
refine ⟨𝔽₄.castRingHom_injective hr' X, λ x ↦ ?_⟩
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
⊢ ∃ a, 𝔽₄.cast r a = x

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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
have h0 {x} (h0 : x * x = 0) : x = 0 := R_elts_claim2 hS hf h0 hr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
⊢ ∃ a, 𝔽₄.cast r a = x

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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rcases R_elts_cases hS hf x with (h1 | h1) | h1
State after:
case inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : (x + 1) * (x + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rcases R_elts_cases hS hf (x + r) with (h2 | h2) | h2
State after:
case inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r + 1) * (x + r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r) * (x + r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r) * (x + r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r) * (x + r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [_root_.add_comm x r, add_assoc, mul_add, add_mul, add_mul, add_assoc, add_assoc,
  add_assoc, h1, add_zero, mul_add_one r, ← add_assoc (x * r), add_left_comm, hr'] at h2
State after:
case inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rcases R_elts_cases hS hf (x * r) with (h3 | h3) | h3
State after:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : (x * r + 1) * (x * r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r * (x * r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : (x + 1) * (x + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact ⟨1, (add_eq_zero_iff_eq.mp (h0 h1)).symm⟩
State after:
no goals

State before:
case inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact ⟨0, (h0 h1).symm⟩
State after:
no goals

State before:
case inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r + 1) * (x + r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact ⟨𝔽₄.Y, (add_eq_zero_iff_eq.mp <| (add_assoc x r 1).symm.trans (h0 h2)).symm⟩
State after:
no goals

State before:
case inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r) * (x + r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact ⟨𝔽₄.X, (add_eq_zero_iff_eq.mp (h0 h2)).symm⟩
State after:
no goals

State before:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : (x * r + 1) * (x * r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
apply h0 at h3
State after:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [add_right_comm, h3, zero_add] at h2
State after:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 0
h3 : x * r + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 0
h3 : r * (x * r + 1) = r * 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [mul_zero, mul_add_one r, ← mul_assoc, h2, zero_mul, zero_add] at h3
State after:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inl
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h3, zero_mul, zero_add] at hr
State after:
case inr.inr.inl.inl
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
hr : 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inl
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
hr : 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact absurd hr X
State after:
no goals

State before:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r * (x * r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
apply h0 at h3
State after:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h3, zero_add, add_eq_zero_iff_eq] at h2
State after:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
have h4 : r = 0 := by rw [← one_mul r, ← h2, mul_assoc, h3, mul_zero]
State after:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h4, zero_mul, zero_add] at hr
State after:
case inr.inr.inl.inr
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
hr : 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inl.inr
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
hr : 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact absurd hr X
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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
⊢ r = 0
Tactic:
rw [← one_mul r, ← h2, mul_assoc, h3, mul_zero]
State after:
no goals

State before:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + r * x + 1 = 0
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [add_right_comm, add_eq_zero_iff_eq] at h2
State after:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : x * r + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [mul_add_one x, add_assoc, add_eq_zero_iff_eq] at h1
State after:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h2, ← mul_assoc, mul_assoc x, add_eq_iff_eq_add'.mp hr', mul_add_one x, add_mul,
  h1, add_assoc, add_add_cancel_right, ← add_one_mul _ x, h2, mul_assoc, h1] at h3
State after:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : r * (x + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : r * (x + 1) * x = 0 * x
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [zero_mul, mul_assoc, add_one_mul x, h1, add_add_cancel_middle₂, mul_one] at h3
State after:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inr
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h3, zero_mul, zero_add] at hr
State after:
case inr.inr.inr
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
hr : 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x

State before:
case inr.inr.inr
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
hr : 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * x = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact absurd hr X
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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ f (𝔽₄.cast r 𝔽₄.O) = ι (𝔽₄Map 𝔽₄.O)
Tactic:
change f 0 = ι (-1)
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ 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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ f 0 = ι (-1)
Tactic:
rw [hf.map_zero, ι.map_neg, ι.map_one]
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
r : R
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ f (𝔽₄.cast r 𝔽₄.Y) = ι (𝔽₄Map 𝔽₄.Y)
Tactic:
change f (r + 1) = ((1 : ℤ) : S) + (-1 : ℤ) • f r
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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ f (r + 1) = ↑1 + -1 • f r

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
hr : r * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ f (r + 1) = ↑1 + -1 • f r
Tactic:
rw [Int.cast_one, neg_one_zsmul, hr0, sub_eq_add_neg]
State after:
no goals