internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
case intro.intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k d : ℕ
h4 : f (g d) = f a
h5 : f d = a + k
⊢ ∃ x, g x = a
Tactic:
exact ⟨d, lem4 h h0 ((h1 _).mpr <| h3.trans <| (h2 _).mp ⟨d, rfl⟩)
  ((h1 a).mpr a.le_refl) h4⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
case inr
f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
this :
  ∀ {f g : ℕ → ℕ},
    good f g →
      good g f → ∀ {a b : ℕ}, (∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k) → (∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k) → a ≤ b → a = b
h3 : ¬a ≤ b
⊢ a = b
Tactic:
exact (this h0 h h2 h1 (le_of_not_le h3)).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
⊢ f a = a.succ
Tactic:
refine (Nat.succ_le_of_lt (lem3 h0 h1)).eq_or_gt.resolve_right λ h3 ↦ ?_
Proof state after:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : a.succ < f a
⊢ False
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : a.succ < f a
⊢ False
Tactic:
obtain ⟨t, h3⟩ := Nat.exists_eq_add_of_lt h3
Proof state after:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
⊢ False
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
⊢ False
Tactic:
obtain ⟨x, h4⟩ := (h1 (a + t)).mpr (a.le_add_right t)
Proof state after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
⊢ False
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
⊢ False
Tactic:
obtain ⟨y, h5⟩ := (h1 (g x)).mpr <| (h2 _).mp ⟨x, rfl⟩
Proof state after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
y : ℕ
h5 : f y = g x
⊢ False
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
y : ℕ
h5 : f y = g x
⊢ False
Tactic:
rw [Nat.succ_add, ← h4, ← h, ← Nat.succ_eq_add_one, ← h, ← h5] at h3
Proof state after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ False
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ False
Tactic:
refine (lem4 h h0 ((h1 a).mpr a.le_refl)
  ((h1 _).mpr <| (h2 _).mp ⟨f y, rfl⟩) h3).not_lt ?_
Proof state after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ a < g (f y)
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ a < g (f y)
Tactic:
rw [h0, Nat.lt_succ_iff, ← h2]
Proof state after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ ∃ x, g x = g y
Theorem: IMOSL.IMO2010A6.lem7
Proof state before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ ∃ x, g x = g y
Tactic:
exact ⟨y, rfl⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
⊢ f = g
Tactic:
obtain ⟨a, h1, h2⟩ := lem6 h h0
Proof state after:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
⊢ f = g
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
⊢ f = g
Tactic:
suffices h3 : ∀ n, a ≤ n → f n = n.succ ∧ g n = n.succ by
  ext x; rw [← Nat.succ_inj', ← h, (h3 _ <| (h2 _).mp ⟨x, rfl⟩).1]
Proof state after:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
⊢ ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
⊢ ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
Tactic:
refine Nat.le_induction ⟨lem7 h h0 h1 h2, lem7 h0 h h2 h1⟩
  (λ n _ h3 ↦ ⟨?_, ?_⟩)
Proof state after:
case intro.intro.refine_1
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ f (n + 1) = (n + 1).succ

case intro.intro.refine_2
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ g (n + 1) = (n + 1).succ
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
⊢ f = g
Tactic:
ext x
Proof state after:
case h
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
x : ℕ
⊢ f x = g x
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
case h
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
x : ℕ
⊢ f x = g x
Tactic:
rw [← Nat.succ_inj', ← h, (h3 _ <| (h2 _).mp ⟨x, rfl⟩).1]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
case intro.intro.refine_1
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ f (n + 1) = (n + 1).succ
Tactic:
rw [← Nat.succ_eq_add_one, ← h3.2, h, h3.1, h3.2]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.final_solution
Proof state before:
case intro.intro.refine_2
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ g (n + 1) = (n + 1).succ
Tactic:
rw [← Nat.succ_eq_add_one, ← h3.1, h0, h3.1, h3.2]
Proof state after:
no goals
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
f : ℕ+ → ℕ+
⊢ (∀ (m n : ℕ+), m * m + f n ∣ m * f m + n) ↔ f = id
Tactic:
refine ⟨λ h ↦ funext λ n ↦ le_antisymm ?_ ?_,
  λ h m n ↦ h.symm ▸ dvd_refl (m * m + n)⟩
Proof state after:
case refine_1
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ f n ≤ id n

case refine_2
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ id n ≤ f n
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_1
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ f n ≤ id n
Tactic:
specialize h (f n) n
Proof state after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * f n + f n ∣ f n * f (f n) + n
⊢ f n ≤ id n
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * f n + f n ∣ f n * f (f n) + n
⊢ f n ≤ id n
Tactic:
rw [← mul_add_one (α := ℕ+)] at h
Proof state after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * (f n + 1) ∣ f n * f (f n) + n
⊢ f n ≤ id n
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * (f n + 1) ∣ f n * f (f n) + n
⊢ f n ≤ id n
Tactic:
replace h := (dvd_mul_right _ _).trans h
Proof state after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ f n * f (f n) + n
⊢ f n ≤ id n
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ f n * f (f n) + n
⊢ f n ≤ id n
Tactic:
rw [PNat.dvd_iff, PNat.add_coe, PNat.mul_coe,
  Nat.dvd_add_right ⟨_, rfl⟩, ← PNat.dvd_iff] at h
Proof state after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ n
⊢ f n ≤ id n
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ n
⊢ f n ≤ id n
Tactic:
exact PNat.le_of_dvd h
Proof state after:
no goals
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_2
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ id n ≤ f n
Tactic:
rcases eq_or_ne n 1 with rfl | h0
Proof state after:
case refine_2.inl
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
⊢ id 1 ≤ f 1

case refine_2.inr
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
h0 : n ≠ 1
⊢ id n ≤ f n
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_2.inl
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
⊢ id 1 ≤ f 1
Tactic:
exact (f 1).one_le
Proof state after:
no goals
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_2.inr
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
h0 : n ≠ 1
⊢ id n ≤ f n
Tactic:
rcases PNat.exists_eq_succ_of_ne_one h0 with ⟨k, rfl⟩
Proof state after:
case refine_2.inr.intro
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
k : ℕ+
h0 : k + 1 ≠ 1
⊢ id (k + 1) ≤ f (k + 1)
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_2.inr.intro
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
k : ℕ+
h0 : k + 1 ≠ 1
⊢ id (k + 1) ≤ f (k + 1)
Tactic:
replace h := PNat.le_of_dvd (h (k + 1) (k + 1))
Proof state after:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : (k + 1) * (k + 1) + f (k + 1) ≤ (k + 1) * f (k + 1) + (k + 1)
⊢ id (k + 1) ≤ f (k + 1)
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : (k + 1) * (k + 1) + f (k + 1) ≤ (k + 1) * f (k + 1) + (k + 1)
⊢ id (k + 1) ≤ f (k + 1)
Tactic:
rw [add_one_mul (α := ℕ+), add_right_comm,
  add_assoc, add_one_mul (α := ℕ+), add_assoc] at h
Proof state after:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : k * (k + 1) + (f (k + 1) + (k + 1)) ≤ k * f (k + 1) + (f (k + 1) + (k + 1))
⊢ id (k + 1) ≤ f (k + 1)
Theorem: IMOSL.IMO2013N1.final_solution
Proof state before:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : k * (k + 1) + (f (k + 1) + (k + 1)) ≤ k * f (k + 1) + (f (k + 1) + (k + 1))
⊢ id (k + 1) ≤ f (k + 1)
Tactic:
exact le_of_mul_le_mul_left' <| le_of_add_le_add_right (α := ℕ+) h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.Eq1
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x * (x + 1) + 1) = f x * f (x + 1)
Tactic:
rw [hf.is_good, add_add_cancel_left, hf.map_one, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x * x + 1) = f x ^ 2 - 1
Tactic:
rw [sq, hf.is_good, add_self_eq_zero, hf.map_zero, sub_eq_add_neg]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.Eq2_v2
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x * x) = f (x + 1) ^ 2 - 1
Tactic:
rw [← Eq2 hf, add_one_mul_self, add_add_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.Eq3
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f x * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)
Tactic:
have h : x * (x + 1) = x * x + x := mul_add_one x x
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : x * (x + 1) = x * x + x
⊢ f x * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)
Theorem: IMOSL.IMO2012A5.Case3.Eq3
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : x * (x + 1) = x * x + x
⊢ f x * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)
Tactic:
rw [← Eq2_v2 hf, ← Eq1 hf, mul_sub_one, ← add_sub_right_comm, h, add_assoc,
  ← hf.is_good, mul_assoc, hf.is_good, h, add_add_cancel_middle₁, add_sub_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.Eq3_v2
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
Tactic:
have h := Eq3 hf (x + 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h :
  f (x + 1) * f ((x + 1) * (x + 1) + (x + 1)) =
    (f (x + 1 + 1) ^ 2 - 1) * (f (x + 1 + 1) - 1) + f (x + 1) * f (x + 1 + 1)
⊢ f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
Theorem: IMOSL.IMO2012A5.Case3.Eq3_v2
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h :
  f (x + 1) * f ((x + 1) * (x + 1) + (x + 1)) =
    (f (x + 1 + 1) ^ 2 - 1) * (f (x + 1 + 1) - 1) + f (x + 1) * f (x + 1 + 1)
⊢ f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
Tactic:
rwa [add_add_cancel_right, add_one_mul_self, add_add_add_cancel_right] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1_ring_id1
Proof state before:
R : Type ?u.23673
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
a b : S
⊢ a * ((a ^ 2 - 1) * (a - 1) + b * a) - b * ((b ^ 2 - 1) * (b - 1) + a * b) =
    (a ^ 2 + b ^ 2 - 1) * (a + b - 1) * (a - b)
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1_ring_id2
Proof state before:
R : Type ?u.29081
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
a : S
⊢ a ^ 2 * ((a ^ 2 - 1) ^ 2 + 1) - ((a ^ 2 - 1) * (a - 1) + a * a) ^ 2 = (1 - 2 * a) * (a ^ 2 - 1)
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
have h := Thm1_ring_id1 (f x) (f (x + 1))
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h :
  f x * ((f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x) -
      f (x + 1) * ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) =
    (f x ^ 2 + f (x + 1) ^ 2 - 1) * (f x + f (x + 1) - 1) * (f x - f (x + 1))
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h :
  f x * ((f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x) -
      f (x + 1) * ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) =
    (f x ^ 2 + f (x + 1) ^ 2 - 1) * (f x + f (x + 1) - 1) * (f x - f (x + 1))
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
rw [← Eq3 hf, ← Eq3_v2 hf, mul_left_comm, sub_self, zero_eq_mul,
  mul_eq_zero, sub_eq_zero, sub_eq_zero, sub_eq_zero] at h
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : (f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1) ∨ f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : (f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1) ∨ f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
cases h with | inl h => exact h | inr h => ?_
Proof state after:
case inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
right
Proof state after:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
⊢ f x + f (x + 1) = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
⊢ f x + f (x + 1) = 1
Tactic:
rw [← h, ← two_mul]
Proof state after:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
⊢ 2 * f x = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
⊢ 2 * f x = 1
Tactic:
have h0 : _ ^ 2 = _ ^ 2 := congrArg (λ x ↦ x ^ 2) (Eq3 hf x)
Proof state after:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : (f x * f (x * x + x)) ^ 2 = ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) ^ 2
⊢ 2 * f x = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : (f x * f (x * x + x)) ^ 2 = ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) ^ 2
⊢ 2 * f x = 1
Tactic:
rw [mul_pow, ← add_eq_of_eq_sub (Eq2 hf (x * x + x)), ← h, add_mul_self,
  ← mul_add_one (x * x), Eq1 hf, Eq2 hf, Eq2_v2 hf, ← h,
  ← sub_eq_zero, ← sq, Thm1_ring_id2, mul_eq_zero] at h0
Proof state after:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : 1 - 2 * f x = 0 ∨ f x ^ 2 - 1 = 0
⊢ 2 * f x = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : 1 - 2 * f x = 0 ∨ f x ^ 2 - 1 = 0
⊢ 2 * f x = 1
Tactic:
cases h0 with | inl h0 => exact (eq_of_sub_eq_zero h0).symm | inr h0 => ?_
Proof state after:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
⊢ 2 * f x = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
⊢ 2 * f x = 1
Tactic:
have h1 : f (x * x) = 0 := by rw [Eq2_v2 hf, ← h, h0]
Proof state after:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
⊢ 2 * f x = 1
Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1
Proof state before:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
⊢ 2 * f x = 1
Tactic:
replace h := Eq3_v2 hf (x * x)
Proof state after:
case inr.h.inr
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : f (x * x + 1) * f (x * x * (x * x) + x * x) = (f (x * x) ^ 2 - 1) * (f (x * x) - 1) + f (x * x + 1) * f (x * x)
⊢ 2 * f x = 1