internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f (f (f (f (f 0 + 1)))) = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h5, h1, zero_add] at h6
Proof state after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f (f (f (f 0 + 1))) = f (f 0 + 2) + 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h4, h1, zero_add] at h5
Proof state after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f 0 = 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f 0).succ.succ = 0
h4 : f (f 0).succ = (f 0).succ.succ
h5 : f 0 = 1
h6 : f 1 = f 0 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h5] at h1 h4 h6
Proof state after:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = Nat.succ ∨ f = answer2
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = Nat.succ ∨ f = answer2
Tactic:
right
Proof state after:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = answer2
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ f = answer2
Tactic:
refine funext (add_four_induction h5 h6 h4 h1 ?_)
Proof state after:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ ∀ (n : ℕ), f n = answer2 n → f (n + 4) = answer2 (n + 4)
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
⊢ ∀ (n : ℕ), f n = answer2 n → f (n + 4) = answer2 (n + 4)
Tactic:
intro n h7
Proof state after:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
n : ℕ
h7 : f n = answer2 n
⊢ f (n + 4) = answer2 (n + 4)
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inr.h
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (Nat.succ 1).succ = 0
h4 : f (Nat.succ 1) = (Nat.succ 1).succ
h5 : f 0 = 1
h6 : f 1 = 1 + 5
n : ℕ
h7 : f n = answer2 n
⊢ f (n + 4) = answer2 (n + 4)
Tactic:
rw [map_add_four h, h7, answer2]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f (f (f 0).succ) = 0 ∨ f (f (f 0).succ) = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
rw [h4, or_iff_right (h3 0)] at h1
Proof state after:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f 0 = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inl.inr.inl
f : ℕ → ℕ
h : good f
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h0 : (finChainFnOfgood h).rangeCompl = {(f 0).succ}
h1 : f 0 = (f 0).succ.succ
h4 : f (f 0).succ = 0
⊢ f = Nat.succ ∨ f = answer2
Tactic:
exact absurd h1 (Nat.lt_succ.mpr (f 0).le_succ).ne
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.good_imp_succ_or_answer2
Proof state before:
case intro.intro.intro.inr
f : ℕ → ℕ
h : good f
a : ℕ
h0 : (finChainFnOfgood h).rangeCompl = {a}
C : FinChainFn f := finChainFnOfgood h
h2 : ∀ (n : ℕ), f (f n) ≠ n
h3 : ∀ (n : ℕ), f n ≠ n
h1 : (f (f a) = 0 ∨ f (f a) = (f 0).succ) ∨ f (f a) = a.succ
h4 : (f a = 0 ∨ f a = (f 0).succ) ∨ f a = a.succ
h5 : a = a.succ
⊢ f = Nat.succ ∨ f = answer2
Tactic:
exact absurd h5 a.lt_succ_self.ne
Proof state after:
no goals
Theorem: IMOSL.Extra.exists_map_eq_seqMax
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
rcases le_total (seqMax f n) (f n.succ) with h | h
Proof state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : seqMax f n ≤ f n.succ
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)

case inr
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Theorem: IMOSL.Extra.exists_map_eq_seqMax
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : seqMax f n ≤ f n.succ
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
exact ⟨n + 1, le_refl (n + 1), (max_eq_right h).symm⟩
Proof state after:
no goals
Theorem: IMOSL.Extra.exists_map_eq_seqMax
Proof state before:
case inr
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
rcases exists_map_eq_seqMax n with ⟨k, h0, h1⟩
Proof state after:
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
k : ℕ
h0 : k ≤ n
h1 : f k = seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Theorem: IMOSL.Extra.exists_map_eq_seqMax
Proof state before:
case inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
f : ℕ → α
n : ℕ
h : f n.succ ≤ seqMax f n
k : ℕ
h0 : k ≤ n
h1 : f k = seqMax f n
⊢ ∃ k, k ≤ n + 1 ∧ f k = seqMax f (n + 1)
Tactic:
exact ⟨k, n.le_succ.trans' h0, h1.trans (max_eq_left h).symm⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq1
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ f (-x) = f (x + 1) * f (-1) + f x
Tactic:
have h0 := hf.is_good (x + 1) (-1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f (x + 1) * f (-1) + f x
Theorem: IMOSL.IMO2012A5.Case1.Eq1
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f (x + 1) * f (-1) + f x
Tactic:
rwa [add_neg_cancel_right, mul_neg_one (x + 1), neg_add, neg_add_cancel_right] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ f (-x) = -f (x + 2)
Tactic:
replace hf := Eq1 hf
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
⊢ f (-x) = -f (x + 2)
Theorem: IMOSL.IMO2012A5.Case1.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
⊢ f (-x) = -f (x + 2)
Tactic:
have h0 := hf (-(x + 1))
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (- -(x + 1)) = f (-(x + 1) + 1) * f (-1) + f (-(x + 1))
⊢ f (-x) = -f (x + 2)
Theorem: IMOSL.IMO2012A5.Case1.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (- -(x + 1)) = f (-(x + 1) + 1) * f (-1) + f (-(x + 1))
⊢ f (-x) = -f (x + 2)
Tactic:
rw [neg_neg, hf (x + 1), neg_add, neg_add_cancel_right, ← add_assoc, self_eq_add_left,
  ← add_mul, mul_eq_zero, or_iff_left h, add_assoc, one_add_one_eq_two] at h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (-x) + f (x + 2) = 0
⊢ f (-x) = -f (x + 2)
Theorem: IMOSL.IMO2012A5.Case1.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (-x) + f (x + 2) = 0
⊢ f (-x) = -f (x + 2)
Tactic:
exact eq_neg_of_add_eq_zero_left h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.map_two
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
⊢ f 2 = 1
Tactic:
rw [← zero_add 2, ← neg_inj, ← Eq2 hf h, neg_zero, hf.map_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq3
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x y : R
⊢ f (-x) * f (-y) + f (-(x + y)) = f x * f y + f (x + y)
Tactic:
rw [neg_add, ← hf.is_good, neg_mul_neg, hf.is_good]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq4
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ f (2 * x + 1) = f x - f (-x)
Tactic:
rw [hf.is_good, map_two hf h, one_mul, add_comm 2, Eq2 hf h, sub_neg_eq_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
have h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x)) := by
  have h0 : x * -x = -x * x := by rw [mul_neg, neg_mul]
  rw [sub_mul, mul_add, mul_add, map_commute_of_commute hf.is_good h0,
    add_comm, add_sub_add_left_eq_sub]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
have h1 := Eq3 hf x x
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f (-x) * f (-x) + f (-(x + x)) = f x * f x + f (x + x)
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f (-x) * f (-x) + f (-(x + x)) = f x * f x + f (x + x)
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
rw [add_comm, ← sub_eq_sub_iff_add_eq_add, h0, Eq1 hf, add_sub_cancel_right,
  ← two_mul, Eq4 hf h, ← sub_eq_zero, ← mul_sub, mul_eq_zero] at h1
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
refine h1.imp (λ h1 ↦ ?_) (λ h1 ↦ (eq_of_sub_eq_zero h1).symm)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f x - f (-x) = 0
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f x - f (-x) = 0
⊢ f (x + 1) = 0
Tactic:
rw [Eq1 hf, sub_add_cancel_right, neg_eq_zero, mul_eq_zero] at h1
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f (x + 1) = 0 ∨ f (-1) = 0
⊢ f (x + 1) = 0
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f (x + 1) = 0 ∨ f (-1) = 0
⊢ f (x + 1) = 0
Tactic:
exact h1.resolve_right h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
Tactic:
have h0 : x * -x = -x * x := by rw [mul_neg, neg_mul]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : x * -x = -x * x
⊢ f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : x * -x = -x * x
⊢ f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
Tactic:
rw [sub_mul, mul_add, mul_add, map_commute_of_commute hf.is_good h0,
  add_comm, add_sub_add_left_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ x * -x = -x * x
Tactic:
rw [mul_neg, neg_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
⊢ f x = -1
Tactic:
have h1 := Eq1 hf x
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x = -1
Tactic:
rw [h0, zero_mul, zero_add] at h1
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
⊢ f x = -1
Tactic:
have h2 := Eq3 hf x (-(x + 1))
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : f (-x) * f (- -(x + 1)) + f (-(x + -(x + 1))) = f x * f (-(x + 1)) + f (x + -(x + 1))
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : f (-x) * f (- -(x + 1)) + f (-(x + -(x + 1))) = f x * f (-(x + 1)) + f (x + -(x + 1))
⊢ f x = -1
Tactic:
rw [neg_neg, h0, mul_zero, zero_add, ← sub_eq_add_neg,
  sub_add_cancel_left, neg_neg, hf.map_one] at h2
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
⊢ f x = -1
Tactic:
have h3 := Eq3 hf x (x + 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-x) * f (-(x + 1)) + f (-(x + (x + 1))) = f x * f (x + 1) + f (x + (x + 1))
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-x) * f (-(x + 1)) + f (-(x + (x + 1))) = f x * f (x + 1) + f (x + (x + 1))
⊢ f x = -1
Tactic:
rw [h0, mul_zero, zero_add, ← add_assoc, ← two_mul,
  Eq4 hf h, h1, sub_self, h2, add_right_inj] at h3
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-(2 * x + 1)) = f (-1)
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-(2 * x + 1)) = f (-1)
⊢ f x = -1
Tactic:
replace h2 := Eq4 hf h (-x - 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f (2 * (-x - 1) + 1) = f (-x - 1) - f (-(-x - 1))
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f (2 * (-x - 1) + 1) = f (-x - 1) - f (-(-x - 1))
⊢ f x = -1
Tactic:
rw [two_mul, add_assoc, sub_add_cancel, ← add_sub_right_comm, ← two_mul, mul_neg,
  ← neg_add', h3, eq_comm, Eq1 hf, sub_add_cancel_right, sub_add_cancel,
  neg_eq_iff_add_eq_zero, h1, ← add_one_mul (f x), mul_eq_zero] at h2
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f x + 1 = 0 ∨ f (-1) = 0
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case1.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f x + 1 = 0 ∨ f (-1) = 0
⊢ f x = -1
Tactic:
exact eq_neg_of_add_eq_zero_left (h2.resolve_right h)
Proof state after:
no goals