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

State before:
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
⊢ r = 0
Tactic:
rcases R_elts_cases hS hf (r + s) with (h | h) | h
State after:
case inl.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
⊢ r = 0

case inl.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
⊢ r = 0

case inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s + 1) + 1 = 0
⊢ r = 0

State before:
case inl.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
⊢ r = 0
Tactic:
rcases R_elts_claim1 hS hf hr h with hr | h | h0
State after:
case inl.inl.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
hr : r = 0
⊢ r = 0

case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r + s + 1 = 0
⊢ r = 0

case inl.inl.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
h0 : r = r + s + 1
⊢ r = 0

State before:
case inl.inl.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
hr : r = 0
⊢ r = 0
Tactic:
exact hr
State after:
no goals

State before:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r + s + 1 = 0
⊢ r = 0
Tactic:
rw [add_assoc, add_eq_zero_iff_eq] at h
State after:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r = s + 1
⊢ r = 0

State before:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r = s + 1
⊢ r = 0
Tactic:
rw [h, add_one_mul s, add_eq_zero_iff_eq] at hr
State after:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 : s * (s + 1) = s + 1
hs : s * (s + 1) + 1 = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r = s + 1
⊢ r = 0

State before:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 : s * (s + 1) = s + 1
hs : s * (s + 1) + 1 = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r = s + 1
⊢ r = 0
Tactic:
rw [hr, add_add_cancel_right] at hs
State after:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 : s * (s + 1) = s + 1
hs : s = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r = s + 1
⊢ r = 0

State before:
case inl.inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 : s * (s + 1) = s + 1
hs : s = 0
h✝ : (r + s + 1) * (r + s + 1) = 0
h : r = s + 1
⊢ r = 0
Tactic:
rwa [← h, hs, zero_mul, eq_comm] at hr
State after:
no goals

State before:
case inl.inl.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
h0 : r = r + s + 1
⊢ r = 0
Tactic:
rw [add_assoc, self_eq_add_right] at h0
State after:
case inl.inl.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
h0 : s + 1 = 0
⊢ r = 0

State before:
case inl.inl.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
h0 : s + 1 = 0
⊢ r = 0
Tactic:
rw [h0, mul_zero, zero_add] at hs
State after:
case inl.inl.inr.inr
R : Type u_1
S : Type ?u.172967
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 : 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
h0 : s + 1 = 0
⊢ r = 0

State before:
case inl.inl.inr.inr
R : Type u_1
S : Type ?u.172967
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 : 1 = 0
h : (r + s + 1) * (r + s + 1) = 0
h0 : s + 1 = 0
⊢ r = 0
Tactic:
rw [← mul_one r, hs, mul_zero]
State after:
no goals

State before:
case inl.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
⊢ r = 0
Tactic:
rcases R_elts_claim1 hS hf hr h with hr | h | h0
State after:
case inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
hr : r = 0
⊢ r = 0

case inl.inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h✝ : (r + s) * (r + s) = 0
h : r + s = 0
⊢ r = 0

case inl.inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
h0 : r = r + s
⊢ r = 0

State before:
case inl.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
hr : r = 0
⊢ r = 0
Tactic:
exact hr
State after:
no goals

State before:
case inl.inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h✝ : (r + s) * (r + s) = 0
h : r + s = 0
⊢ r = 0
Tactic:
rw [← add_eq_zero_iff_eq.mp h, mul_add_one r, hr, zero_add] at hs
State after:
case inl.inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 : r + 1 = 0
h✝ : (r + s) * (r + s) = 0
h : r + s = 0
⊢ r = 0

State before:
case inl.inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 : r + 1 = 0
h✝ : (r + s) * (r + s) = 0
h : r + s = 0
⊢ r = 0
Tactic:
rw [add_eq_zero_iff_eq.mp hs, mul_one] at hr
State after:
case inl.inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 : 1 = 0
hs : r + 1 = 0
h✝ : (r + s) * (r + s) = 0
h : r + s = 0
⊢ r = 0

State before:
case inl.inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 : 1 = 0
hs : r + 1 = 0
h✝ : (r + s) * (r + s) = 0
h : r + s = 0
⊢ r = 0
Tactic:
rwa [hr, add_zero] at hs
State after:
no goals

State before:
case inl.inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
h0 : r = r + s
⊢ r = 0
Tactic:
rw [self_eq_add_right] at h0
State after:
case inl.inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
h0 : s = 0
⊢ r = 0

State before:
case inl.inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s) = 0
h0 : s = 0
⊢ r = 0
Tactic:
rw [h0, zero_mul, zero_add] at hs
State after:
case inl.inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 : 1 = 0
h : (r + s) * (r + s) = 0
h0 : s = 0
⊢ r = 0

State before:
case inl.inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 : 1 = 0
h : (r + s) * (r + s) = 0
h0 : s = 0
⊢ r = 0
Tactic:
rw [← mul_one r, hs, mul_zero]
State after:
no goals

State before:
case inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : (r + s) * (r + s + 1) + 1 = 0
⊢ r = 0
Tactic:
rw [add_assoc, mul_add, add_mul, hr, zero_add,
  add_mul, ← add_assoc, add_assoc, hs, add_zero] at h
State after:
case inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
⊢ r = 0

State before:
case inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0 : r * (s * r + r * (s + 1)) * s = r * 0 * s
⊢ r = 0
Tactic:
rw [mul_zero, zero_mul, mul_add, ← mul_assoc,
  ← mul_assoc, hr, zero_mul, add_zero, mul_assoc] at h0
State after:
case inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0 : r * s * (r * s) = 0
⊢ r = 0

State before:
case inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0 : r * s * (r * s) = 0
⊢ r = 0
Tactic:
rcases R_elts_claim1 hS hf hr h0 with hr | h0 | h0
State after:
case inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0 : r * s * (r * s) = 0
hr : r = 0
⊢ r = 0

case inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0✝ : r * s * (r * s) = 0
h0 : r * s = 0
⊢ r = 0

case inr.inr.inr
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0✝ : r * s * (r * s) = 0
h0 : r = r * s
⊢ r = 0

State before:
case inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0 : r * s * (r * s) = 0
hr : r = 0
⊢ r = 0
Tactic:
exact hr
State after:
no goals

State before:
case inr.inr.inl
R : Type u_1
S : Type ?u.172967
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 + 1) + 1 = 0
h : s * r + r * (s + 1) = 0
h0✝ : r * s * (r * s) = 0
h0 : r * s * (s + 1) = 0 * (s + 1)
⊢ r = 0
Tactic:
rwa [zero_mul, mul_assoc, add_eq_zero_iff_eq.mp hs, mul_one] at h0
State after:
no goals

State before:
case inr.inr.inr
R : Type u_1
S : Type ?u.172967
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
h : s * r + r * (s + 1) = 0
h0✝ : r * s * (r * s) = 0
h0 : r = r * s
hs : r * (s * (s + 1) + 1) = r * 0
⊢ r = 0
Tactic:
rwa [mul_zero, mul_add_one r, ← mul_assoc, ← h0,
  mul_add_one r, ← h0, add_add_cancel_right] at hs
State after:
no goals