Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1 (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : r * s * (r * s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
rw [reduced_𝔽₂ε_iff hS hf, hf.is_good] at h
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
rw [reduced_𝔽₂ε_iff hS hf, map_add_one_eq_zero_iff_map_eq hS hf.toNontrivialGood,
  _root_.sq_eq_one_iff, or_comm] at hr hs
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
have h0 {x} : f x = -1 → x = 0 := map_eq_neg_one_reduced_imp hS hf
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ r = 0 ∨ s = 0 ∨ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : f r = -1 ∨ f r = 1
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ r = 0 ∨ s = 0 ∨ r = s
Tactic:
revert hr
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ f r = -1 ∨ f r = 1 → r = 0 ∨ s = 0 ∨ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
⊢ f r = -1 ∨ f r = 1 → r = 0 ∨ s = 0 ∨ r = s
Tactic:
refine Or.imp h0 λ hr ↦ ?_
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ s = 0 ∨ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hs : f s = -1 ∨ f s = 1
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ s = 0 ∨ r = s
Tactic:
revert hs
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ f s = -1 ∨ f s = 1 → s = 0 ∨ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
⊢ f s = -1 ∨ f s = 1 → s = 0 ∨ r = s
Tactic:
refine Or.imp h0 λ hs ↦ ?_
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f r * f s + f (r + s) = 0
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s
Tactic:
rw [hr, hs, mul_one, ← neg_eq_iff_add_eq_zero, eq_comm] at h
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f (r + s) = -1
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
h : f (r + s) = -1
h0 : ∀ {x : R}, f x = -1 → x = 0
hr : f r = 1
hs : f s = 1
⊢ r = s
Tactic:
exact add_eq_zero_iff_eq.mp (h0 h)
State after:
no goals

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
⊢ r * s * (r * s) = 0
Tactic:
have h : (r + s) * (r + s) = r * s + s * r := by
  rw [add_mul, mul_add, hr, zero_add, mul_add, hs, add_zero]
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
⊢ r * s * (r * s) = 0

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
⊢ r * s * (r * s) = 0
Tactic:
rcases R_elts_cases hS hf (r + s) with (h0 | h0) | h0
State after:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s + 1) * (r + s + 1) = 0
⊢ r * s * (r * s) = 0

case inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s) * (r + s) = 0
⊢ r * s * (r * s) = 0

case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s) * (r + s + 1) + 1 = 0
⊢ r * s * (r * s) = 0

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
⊢ (r + s) * (r + s) = r * s + s * r
Tactic:
rw [add_mul, mul_add, hr, zero_add, mul_add, hs, add_zero]
State after:
no goals

State before:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s + 1) * (r + s + 1) = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [add_one_mul_self, h, add_eq_zero_iff_eq] at h0
State after:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
⊢ r * s * (r * s) = 0

State before:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
⊢ r * s * (r * s) = 0
Tactic:
have h1 : (r * s) * (r * s) = r * s := by
  apply congrArg (λ x ↦ r * x * s) at h0
  rwa [mul_add, ← mul_assoc, hr, zero_mul, zero_add,
    mul_one, mul_assoc, mul_assoc, ← mul_assoc] at h0
State after:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
⊢ r * s * (r * s) = 0

State before:
case inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
⊢ r * s * (r * s) = 0
Tactic:
rcases R_elts_cases hS hf (r * s) with (h2 | h2) | h2
State after:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : (r * s + 1) * (r * s + 1) = 0
⊢ r * s * (r * s) = 0

case inl.inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s * (r * s) = 0
⊢ r * s * (r * s) = 0

case inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s * (r * s + 1) + 1 = 0
⊢ r * s * (r * s) = 0

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
⊢ r * s * (r * s) = r * s
Tactic:
apply congrArg (λ x ↦ r * x * s) at h0
State after:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * (r * s + s * r) * s = r * 1 * s
⊢ r * s * (r * s) = r * s

State before:
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * (r * s + s * r) * s = r * 1 * s
⊢ r * s * (r * s) = r * s
Tactic:
rwa [mul_add, ← mul_assoc, hr, zero_mul, zero_add,
  mul_one, mul_assoc, mul_assoc, ← mul_assoc] at h0
State after:
no goals

State before:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : (r * s + 1) * (r * s + 1) = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [add_one_mul_self, h1, add_eq_zero_iff_eq] at h2
State after:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
⊢ r * s * (r * s) = 0

State before:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
⊢ r * s * (r * s) = 0
Tactic:
rw [h2, add_right_eq_self] at h0
State after:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : s * r = 0
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
⊢ r * s * (r * s) = 0

State before:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
h0 : r * (s * r) = r * 0
⊢ r * s * (r * s) = 0
Tactic:
rw [mul_zero, ← mul_assoc, h2, one_mul] at h0
State after:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
h0 : r = 0
⊢ r * s * (r * s) = 0

State before:
case inl.inl.inl.inl
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h1 : r * s * (r * s) = r * s
h2 : r * s = 1
h0 : r = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [h0, zero_mul, zero_mul]
State after:
no goals

State before:
case inl.inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s * (r * s) = 0
⊢ r * s * (r * s) = 0
Tactic:
exact h2
State after:
no goals

State before:
case inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : r * s * (r * s + 1) + 1 = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [mul_add_one (r * s), h1, add_self_eq_zero, zero_add] at h2
State after:
case inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : 1 = 0
⊢ r * s * (r * s) = 0

State before:
case inl.inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r = 1
h1 : r * s * (r * s) = r * s
h2 : 1 = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [← mul_one (r * s * _), h2, mul_zero]
State after:
no goals

State before:
case inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s) * (r + s) = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [h, add_eq_zero_iff_eq] at h0
State after:
case inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s = s * r
⊢ r * s * (r * s) = 0

State before:
case inl.inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s = s * r
⊢ r * s * (r * s) = 0
Tactic:
rw [← mul_assoc, mul_assoc r, ← h0, mul_assoc, mul_assoc, hs, mul_zero, mul_zero]
State after:
no goals

State before:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : (r + s) * (r + s + 1) + 1 = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [mul_add_one (r + s), h] at h0
State after:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h : (r + s) * (r + s) = r * s + s * r
h0 : r * s + s * r + (r + s) + 1 = 0
⊢ r * s * (r * s) = 0

State before:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * (r * s + s * r + (r + s) + 1) = r * 0
⊢ r * s * (r * s) = 0
Tactic:
rw [mul_zero, mul_add_one r, mul_add, mul_add, ← mul_assoc,
  mul_add, hr, zero_mul, zero_add, zero_add, ← mul_assoc] at h
State after:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * s * r + r * s + r = 0
⊢ r * s * (r * s) = 0

State before:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * s * r + r * s + r = 0
h1 : (r * s * r + r * s + r) * r = 0 * r
⊢ r * s * (r * s) = 0
Tactic:
rw [zero_mul, add_mul, add_mul, mul_assoc, hr, add_zero, mul_zero, zero_add] at h1
State after:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * s * r + r * s + r = 0
h1 : r * s * r = 0
⊢ r * s * (r * s) = 0

State before:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * s * r + r * s + r = 0
h1 : r * s * r = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [h1, zero_add, add_eq_zero_iff_eq] at h
State after:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * s = r
h1 : r * s * r = 0
⊢ r * s * (r * s) = 0

State before:
case inr
R : Type u_1
S : Type ?u.159546
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
hs : s * s = 0
h0 : r * s + s * r + (r + s) + 1 = 0
h : r * s = r
h1 : r * s * r = 0
⊢ r * s * (r * s) = 0
Tactic:
rw [h, hr]
State after:
no goals