internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ f (f x)
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h1 : ∀ x : R, f x ≤ 0 := λ x ↦
  le_of_not_lt λ h2 ↦ (h0 (f x)).not_lt <| mul_pos h2 (h2.trans_le (h1 x))
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h0 : ∀ x : R, x < 0 → f x = 0 := λ x h2 ↦
  (h1 x).antisymm (nonneg_of_mul_nonpos_right (h0 x) h2)
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
intros x h2
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2 : x ≤ 0
⊢ f x = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2 : x ≤ 0
⊢ f x = 0
Tactic:
rcases h2.lt_or_eq with h2 | rfl
Proof state after:
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2✝ : x ≤ 0
h2 : x < 0
⊢ f x = 0

case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ f 0 = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) - f (f x) ≤ (f t - x) * f x
Tactic:
rw [sub_le_iff_le_add]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) ≤ (f t - x) * f x + f (f x)
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) ≤ (f t - x) * f x + f (f x)
Tactic:
apply (h _ _).trans_eq'
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) = f (x + (f t - x))
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
t x : R
⊢ f (f t) = f (x + (f t - x))
Tactic:
rw [add_sub_cancel]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
t x : R
⊢ 0 ≤ (f t - x) * f x + (f x - t) * f t
Tactic:
rw [← sub_self (f (f t)), ← sub_add_sub_cancel _ (f (f x))]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
t x : R
⊢ f (f t) - f (f x) + (f (f x) - f (f t)) ≤ (f t - x) * f x + (f x - t) * f t
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
t x : R
⊢ f (f t) - f (f x) + (f (f x) - f (f t)) ≤ (f t - x) * f x + (f x - t) * f t
Tactic:
exact add_le_add (h0 t x) (h0 x t)
Proof state after:
no goals
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
x : R
⊢ x * f x ≤ 0
Tactic:
have h1 := h0 x (f x + f x)
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
x : R
h1 : 0 ≤ (f x - (f x + f x)) * f (f x + f x) + (f (f x + f x) - x) * f x
⊢ x * f x ≤ 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
x : R
h1 : 0 ≤ (f x - (f x + f x)) * f (f x + f x) + (f (f x + f x) - x) * f x
⊢ x * f x ≤ 0
Tactic:
rwa [sub_add_cancel_left, sub_mul, neg_mul, mul_comm,
  ← add_sub_assoc, neg_add_self, zero_sub, neg_nonneg] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
x : R
⊢ f x ≤ f (f x)
Tactic:
have h1 := h x 0
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
x : R
h1 : f (x + 0) ≤ 0 * f x + f (f x)
⊢ f x ≤ f (f x)
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
x : R
h1 : f (x + 0) ≤ 0 * f x + f (f x)
⊢ f x ≤ f (f x)
Tactic:
rwa [add_zero, zero_mul, zero_add] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
x : R
h2✝ : x ≤ 0
h2 : x < 0
⊢ f x = 0
Tactic:
exact h0 x h2
Proof state after:
no goals
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ f 0 = 0
Tactic:
apply (h1 0).antisymm
Proof state after:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ 0 ≤ f 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
⊢ 0 ≤ f 0
Tactic:
specialize h (-1) 0
Proof state after:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
h : f (-1 + 0) ≤ 0 * f (-1) + f (f (-1))
⊢ 0 ≤ f 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h1 : ∀ (x : R), f x ≤ 0
h0 : ∀ (x : R), x < 0 → f x = 0
h2 : 0 ≤ 0
h : f (-1 + 0) ≤ 0 * f (-1) + f (f (-1))
⊢ 0 ≤ f 0
Tactic:
rwa [add_zero, zero_mul, zero_add, h0 _ neg_one_lt_zero] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2007A1.final_solution_part1
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ a k - a m ≤ 2 • seqMax (fun i => |x i - a i|) n
Tactic:
apply (le_add_of_nonneg_left (sub_nonneg_of_le (h h0))).trans
Proof state after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - x k + (a k - a m) ≤ 2 • seqMax (fun i => |x i - a i|) n
Theorem: IMOSL.IMO2007A1.final_solution_part1
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - x k + (a k - a m) ≤ 2 • seqMax (fun i => |x i - a i|) n
Tactic:
rw [← add_comm_sub, sub_add, sub_sub_sub_comm, two_nsmul]
Proof state after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n
Theorem: IMOSL.IMO2007A1.final_solution_part1
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n
Tactic:
have X {i} : i ≤ n → |x i - a i| ≤ seqMax (λ i ↦ |x i - a i|) n :=
  le_seqMax_of_le (λ i ↦ |x i - a i|)
Proof state after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
X : ∀ {i : ℕ}, i ≤ n → |x i - a i| ≤ seqMax (fun i => |x i - a i|) n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n
Theorem: IMOSL.IMO2007A1.final_solution_part1
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n k m : ℕ
x : ℕ → G
h : Monotone x
h0 : k ≤ m
h1 : m ≤ n
X : ∀ {i : ℕ}, i ≤ n → |x i - a i| ≤ seqMax (fun i => |x i - a i|) n
⊢ x m - a m - (x k - a k) ≤ seqMax (fun i => |x i - a i|) n + seqMax (fun i => |x i - a i|) n
Tactic:
exact (le_abs_self _).trans <| (abs_sub _ _).trans <|
  add_le_add (X h1) (X (h0.trans h1))
Proof state after:
no goals
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n = g
Tactic:
apply le_antisymm
Proof state after:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g

case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g
Tactic:
rcases exists_map_eq_seqMax (λ i ↦ |seqMax a i - g - a i|) n with ⟨i, h0, h1⟩
Proof state after:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n ≤ g
Tactic:
rw [← h1, sub_right_comm, abs_le]
Proof state after:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
h1 : |seqMax a i - g - a i| = seqMax (fun i => |seqMax a i - g - a i|) n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g
Tactic:
clear h1
Proof state after:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g ∧ seqMax a i - a i - g ≤ g
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g

case a.intro.intro.refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ seqMax a i - a i - g ≤ g
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ -g ≤ seqMax a i - a i - g
Tactic:
rw [le_sub_iff_add_le, neg_add_self, sub_nonneg]
Proof state after:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ a i ≤ seqMax a i
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro.refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ a i ≤ seqMax a i
Tactic:
exact le_seqMax_self a i
Proof state after:
no goals
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro.refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
⊢ seqMax a i - a i - g ≤ g
Tactic:
rcases exists_map_eq_seqMax a i with ⟨j, h1, h2⟩
Proof state after:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ seqMax a i - a i - g ≤ g
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ seqMax a i - a i - g ≤ g
Tactic:
rw [← h2, sub_le_iff_le_add, ← two_nsmul]
Proof state after:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ a j - a i ≤ 2 • g
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a.intro.intro.refine_2.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
i : ℕ
h0 : i ≤ n
j : ℕ
h1 : j ≤ i
h2 : a j = seqMax a i
⊢ a j - a i ≤ 2 • g
Tactic:
exact h j i h1 h0
Proof state after:
no goals
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ seqMax (fun i => |(fun i => seqMax a i - g) i - a i|) n
Tactic:
apply (le_seqMax_of_le _ n.zero_le).trans'
Proof state after:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |(fun i => seqMax a i - g) 0 - a 0|
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |(fun i => seqMax a i - g) 0 - a 0|
Tactic:
rw [sub_sub, seqMax, sub_add_cancel_right, abs_neg]
Proof state after:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |g|
Theorem: IMOSL.IMO2007A1.final_solution_part2
Proof state before:
case a
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
g : G
h : ∀ (k m : ℕ), k ≤ m → m ≤ n → a k - a m ≤ 2 • g
⊢ g ≤ |g|
Tactic:
exact le_abs_self g
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.surjective_iff
Proof state before:
α : Type u_1
f : α → α
h : FinChainFn f
⊢ Surjective f ↔ h.rangeCompl = ∅
Tactic:
rw [← Set.range_iff_surjective, ← compl_inj_iff,
  ← h.rangeCompl_spec, Set.compl_univ, coe_eq_empty]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
⊢ f^[m] a ≠ f^[n] b
Tactic:
wlog h3 : m < n
Proof state after:
case inr
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
this :
  ∀ {α : Type u_1} {f : α → α} (h : FinChainFn f) {m n : ℕ} {a b : α},
    m ≠ n → a ∈ h.rangeCompl → b ∈ h.rangeCompl → m < n → f^[m] a ≠ f^[n] b
h3 : ¬m < n
⊢ f^[m] a ≠ f^[n] b

α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case inr
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
this :
  ∀ {α : Type u_1} {f : α → α} (h : FinChainFn f) {m n : ℕ} {a b : α},
    m ≠ n → a ∈ h.rangeCompl → b ∈ h.rangeCompl → m < n → f^[m] a ≠ f^[n] b
h3 : ¬m < n
⊢ f^[m] a ≠ f^[n] b

α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b
Tactic:
exact (this h h0.symm h2 h1 <| (le_of_not_lt h3).lt_of_ne h0.symm).symm
Proof state after:
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m n : ℕ
a b : α
h0 : m ≠ n
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
h3 : m < n
⊢ f^[m] a ≠ f^[n] b
Tactic:
rcases Nat.exists_eq_add_of_le h3.le with ⟨k, rfl⟩
Proof state after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : m < m + k
⊢ f^[m] a ≠ f^[m + k] b
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : m < m + k
⊢ f^[m] a ≠ f^[m + k] b
Tactic:
rw [Nat.lt_add_right_iff_pos] at h3
Proof state after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ f^[m] a ≠ f^[m + k] b
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ f^[m] a ≠ f^[m + k] b
Tactic:
rw [f.iterate_add_apply m k b, (h.injective.iterate m).ne_iff]
Proof state after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ a ≠ f^[k] b
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
a b : α
h1 : a ∈ h.rangeCompl
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
⊢ a ≠ f^[k] b
Tactic:
rintro rfl
Proof state after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : f^[k] b ∈ h.rangeCompl
⊢ False
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : f^[k] b ∈ h.rangeCompl
⊢ False
Tactic:
rw [mem_rangeCompl_iff, Set.mem_range] at h1
Proof state after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ False
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ False
Tactic:
refine h1 ⟨f^[k.pred] b, ?_⟩
Proof state after:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ f (f^[k.pred] b) = f^[k] b
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_apply_ne_of_mem_rangeCompl_iter_ne
Proof state before:
case intro
α✝ : Type u_1
f✝ : α✝ → α✝
h✝ : FinChainFn f✝
α : Type u_1
f : α → α
h : FinChainFn f
m : ℕ
b : α
h2 : b ∈ h.rangeCompl
k : ℕ
h0 : m ≠ m + k
h3 : 0 < k
h1 : ¬∃ y, f y = f^[k] b
⊢ f (f^[k.pred] b) = f^[k] b
Tactic:
rw [← f.iterate_succ_apply', Nat.succ_pred_eq_of_pos h3]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_spec
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
a : α
⊢ a ∈ ↑(h.exactIterRange n) ↔ a ∈ Set.range f^[n] \ Set.range f^[n + 1]
Tactic:
rw [exactIterRange, coe_image, h.rangeCompl_spec, iterate_succ,
  Set.range_comp _ f, Set.range_diff_image (h.injective.iterate n)]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_disjoint_of_ne
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
⊢ Disjoint (h.exactIterRange m) (h.exactIterRange n)
Tactic:
rw [disjoint_iff_ne]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
⊢ ∀ a ∈ h.exactIterRange m, ∀ b ∈ h.exactIterRange n, a ≠ b
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_disjoint_of_ne
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
⊢ ∀ a ∈ h.exactIterRange m, ∀ b ∈ h.exactIterRange n, a ≠ b
Tactic:
intro a h1 b h2
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.exactIterRange m
b : α
h2 : b ∈ h.exactIterRange n
⊢ a ≠ b
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_disjoint_of_ne
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.exactIterRange m
b : α
h2 : b ∈ h.exactIterRange n
⊢ a ≠ b
Tactic:
rw [h.mem_exactIterRange_iff] at h1 h2
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : ∃ b ∈ h.rangeCompl, f^[m] b = a
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
⊢ a ≠ b