internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim1
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof 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
Proof state after:
no goals