Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
have h := Eq1 hf (2 + 1) 2
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f ((2 + 1) * 2 - 1) = f (2 + 1) * f 2 + f (2 + 1 - 2)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f ((2 + 1) * 2 - 1) = f (2 + 1) * f 2 + f (2 + 1 - 2)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [add_sub_cancel_left, hf.map_one, add_zero,
  mul_two, add_sub_assoc, add_sub_cancel_right] at h
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
have h0 := Eq6 hf (2 + 1 + 1)
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1 + 1 + 1) + f (2 + 1 + 1 - 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1 + 1 + 1) + f (2 + 1 + 1 - 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [add_sub_cancel_right, add_assoc, one_add_one_eq_two, h, ← mul_add_one (f _)] at h0
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
replace h := Eq6 hf (2 + 1)
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + f (2 + 1 - 1) = (f (2 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + f (2 + 1 - 1) = (f (2 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [add_sub_cancel_right, add_one_mul (α := S), add_sub_left_comm,
  add_comm, add_right_inj, eq_sub_iff_add_eq] at h
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [h, mul_assoc, eq_comm, ← sub_eq_zero, ← mul_sub, mul_eq_zero] at h0
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
clear h
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
revert h0
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
⊢ f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0 → f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
⊢ f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0 → f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
refine Or.imp (λ h ↦ ?_) (λ h ↦ ?_)
State after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
⊢ f 2 = 1

case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 0 ∨ f 2 = 3

State before:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
⊢ f 2 = 1
Tactic:
have h0 := Eq1 hf 2 (1 + 1)
State after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f (2 * (1 + 1) - 1) = f 2 * f (1 + 1) + f (2 - (1 + 1))
⊢ f 2 = 1

State before:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f (2 * (1 + 1) - 1) = f 2 * f (1 + 1) + f (2 - (1 + 1))
⊢ f 2 = 1
Tactic:
rw [two_mul, ← add_assoc, add_sub_cancel_right, one_add_one_eq_two, sub_self,
  hf.map_zero, h, eq_comm, add_neg_eq_zero, mul_self_eq_one_iff] at h0
State after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f 2 = 1 ∨ f 2 = -1
⊢ f 2 = 1

State before:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f 2 = 1 ∨ f 2 = -1
⊢ f 2 = 1
Tactic:
exact h0.resolve_right hf.map_two_ne_neg_one
State after:
no goals

State before:
case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [mul_sub_one, sub_one_mul, sub_sub, sub_add_add_cancel, ← two_mul,
  sub_sub, ← one_add_mul 2 (f 2), ← sub_mul, mul_eq_zero, add_comm] at h
State after:
case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f 2 - (2 + 1) = 0 ∨ f 2 = 0
⊢ f 2 = 0 ∨ f 2 = 3

State before:
case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f 2 - (2 + 1) = 0 ∨ f 2 = 0
⊢ f 2 = 0 ∨ f 2 = 3
Tactic:
exact h.symm.imp_right λ h ↦ (eq_of_sub_eq_zero h).trans two_add_one_eq_three
State after:
no goals