internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : ∀ (a : ℤ), M ≤ a → IsPeriodicPt f (2 * a.natAbs ^ 2) 0
h2 : IsPeriodicPt f ((2 * M.natAbs ^ 2).gcd (2 * (M + 1).natAbs ^ 2)) 0
⊢ -1 * M + 1 * (M + 1) = 1
Tactic:
rw [one_mul, neg_one_mul, neg_add_cancel_left]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h1 : ∀ (a : ℤ), f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
⊢ f a = f (-a)
Tactic:
specialize h1 a
Proof state after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f a = f (-a)
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : f^[2 * a.natAbs ^ 2] 0 = a * (f a - f (-a))
⊢ f a = f (-a)
Tactic:
rw [h0.mul_const, zero_eq_mul] at h1
Proof state after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : a = 0 ∨ f a - f (-a) = 0
⊢ f a = f (-a)
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
a : ℤ
h3 : a ≠ 0
h1 : a = 0 ∨ f a - f (-a) = 0
⊢ f a = f (-a)
Tactic:
exact eq_of_sub_eq_zero (h1.resolve_left h3)
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
⊢ f = 0
Tactic:
have h3 : f (f 2) = 1 * f 1 + 1 * f 1 := h 1 1
Proof state after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f (f 2) = 1 * f 1 + 1 * f 1
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f (f 2) = 1 * f 1 + 1 * f 1
⊢ f = 0
Tactic:
rw [h2 1 one_ne_zero, h2 _ two_ne_zero] at h3
Proof state after:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f 0 = 1 * 0 + 1 * 0
⊢ f = 0
Theorem: IMOSL.IMO2020A6.eq_zero_of_not_injective
Proof state before:
f : ℤ → ℤ
h : good f
M : ℤ
h0 : IsPeriodicPt f 2 0
h1 : ∀ (a : ℤ), a ≠ 0 → f a = f (-a)
h2 : ∀ (a : ℤ), a ≠ 0 → f a = 0
h3 : f 0 = 1 * 0 + 1 * 0
⊢ f = 0
Tactic:
exact funext λ a ↦ (ne_or_eq a 0).elim (h2 a) (λ h4 ↦ h4.symm ▸ h3)
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
⊢ |a n| ≤ max (Extra.seqMax (-a) n) (2 • Extra.seqMax a n)
Tactic:
rw [le_max_iff]
Proof state after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
⊢ |a n| ≤ Extra.seqMax (-a) n ∨ |a n| ≤ 2 • Extra.seqMax a n
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
⊢ |a n| ≤ Extra.seqMax (-a) n ∨ |a n| ≤ 2 • Extra.seqMax a n
Tactic:
refine (le_total (a n) 0).imp (λ h ↦ ?_) (λ h ↦ ?_)
Proof state after:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ |a n| ≤ Extra.seqMax (-a) n

case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ |a n| ≤ 2 • Extra.seqMax a n
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ |a n| ≤ Extra.seqMax (-a) n
Tactic:
rw [abs_of_nonpos h]
Proof state after:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ -a n ≤ Extra.seqMax (-a) n
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
case refine_1
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : a n ≤ 0
⊢ -a n ≤ Extra.seqMax (-a) n
Tactic:
exact Extra.le_seqMax_self (-a) n
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ |a n| ≤ 2 • Extra.seqMax a n
Tactic:
rw [abs_of_nonneg h, two_nsmul]
Proof state after:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n
Tactic:
have h0 := Extra.le_seqMax_self a n
Proof state after:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
h0 : a n ≤ Extra.seqMax a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n
Theorem: IMOSL.IMO2017A4.abs_le_max_seqMax
Proof state before:
case refine_2
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
a : ℕ → G
n : ℕ
h : 0 ≤ a n
h0 : a n ≤ Extra.seqMax a n
⊢ a n ≤ Extra.seqMax a n + Extra.seqMax a n
Tactic:
exact le_add_of_le_of_nonneg h0 (h.trans h0)
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.good1_bdd_above
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Tactic:
rcases Extra.exists_map_eq_seqMax a n with ⟨i, h2, h1⟩
Proof state after:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : i ≤ n
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Theorem: IMOSL.IMO2017A4.good1_bdd_above
Proof state before:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : i ≤ n
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Tactic:
rw [le_iff_exists_add] at h2
Proof state after:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : ∃ c, n = i + c
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Theorem: IMOSL.IMO2017A4.good1_bdd_above
Proof state before:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good1 D a
h0 : D ≤ n
i : ℕ
h2 : ∃ c, n = i + c
h1 : a i = Extra.seqMax a n
⊢ a (n + 1) ≤ Extra.seqMax (-a) n - Extra.seqMax a n
Tactic:
rcases h2 with ⟨j, rfl⟩
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ a (i + j + 1) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)
Theorem: IMOSL.IMO2017A4.good1_bdd_above
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ a (i + j + 1) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)
Tactic:
apply (h i j h0).trans
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -(a i + a j) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)
Theorem: IMOSL.IMO2017A4.good1_bdd_above
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -(a i + a j) ≤ Extra.seqMax (-a) (i + j) - Extra.seqMax a (i + j)
Tactic:
rw [← h1, neg_add_rev, ← sub_eq_add_neg]
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -a j - a i ≤ Extra.seqMax (-a) (i + j) - a i
Theorem: IMOSL.IMO2017A4.good1_bdd_above
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good1 D a
i j : ℕ
h0 : D ≤ i + j
h1 : a i = Extra.seqMax a (i + j)
⊢ -a j - a i ≤ Extra.seqMax (-a) (i + j) - a i
Tactic:
exact sub_le_sub_right (Extra.le_seqMax_of_le (-a) (j.le_add_left i)) (a i)
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.good2_bdd_below
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D n : ℕ
a : ℕ → G
h : good2 D a
h0 : D ≤ n
⊢ -a (n + 1) ≤ 2 • Extra.seqMax a n
Tactic:
rcases h n h0 with ⟨i, j, rfl, h0⟩
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ -a (i + j + 1) ≤ 2 • Extra.seqMax a (i + j)
Theorem: IMOSL.IMO2017A4.good2_bdd_below
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ -a (i + j + 1) ≤ 2 • Extra.seqMax a (i + j)
Tactic:
rw [h0, neg_neg, two_nsmul]
Proof state after:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ a i + a j ≤ Extra.seqMax a (i + j) + Extra.seqMax a (i + j)
Theorem: IMOSL.IMO2017A4.good2_bdd_below
Proof state before:
case intro.intro.intro
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
D : ℕ
a : ℕ → G
h : good2 D a
i j : ℕ
h0✝ : D ≤ i + j
h0 : a (i + j + 1) = -(a i + a j)
⊢ a i + a j ≤ Extra.seqMax a (i + j) + Extra.seqMax a (i + j)
Tactic:
exact add_le_add (Extra.le_seqMax_of_le a (i.le_add_right j))
  (Extra.le_seqMax_of_le a (j.le_add_left i))
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : D ≤ K
h3 : c K ≤ 2 • b K
⊢ b (K + 1) = b K ∧ c (K + 1) ≤ 2 • b (K + 1)
Tactic:
suffices b K = b (K + 1) from
  ⟨this.symm, (h0 K h2).trans_eq (this ▸ max_eq_right h3)⟩
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : D ≤ K
h3 : c K ≤ 2 • b K
⊢ b K = b (K + 1)
Theorem: IMOSL.IMO2017A4.c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : D ≤ K
h3 : c K ≤ 2 • b K
⊢ b K = b (K + 1)
Tactic:
rw [two_nsmul, ← sub_le_iff_le_add] at h3
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : D ≤ K
h3 : c K - b K ≤ b K
⊢ b K = b (K + 1)
Theorem: IMOSL.IMO2017A4.c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : D ≤ K
h3 : c K - b K ≤ b K
⊢ b K = b (K + 1)
Tactic:
exact (h1 K.le_succ).antisymm ((h K h2).trans_eq (max_eq_left h3))
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.c_succ_eq_D_of_b_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
⊢ 2 • b K < c K → c (K + 1) = c D
Tactic:
have X {M : ℕ} : D ≤ M → 2 • b M < c M → c (M + 1) = c M := λ h3 h4 ↦
  ((h0 M h3).trans_eq (max_eq_left_of_lt h4)).antisymm (h2 M.le_succ)
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
X : ∀ {M : ℕ}, D ≤ M → 2 • b M < c M → c (M + 1) = c M
⊢ 2 • b K < c K → c (K + 1) = c D
Theorem: IMOSL.IMO2017A4.c_succ_eq_D_of_b_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
X : ∀ {M : ℕ}, D ≤ M → 2 • b M < c M → c (M + 1) = c M
⊢ 2 • b K < c K → c (K + 1) = c D
Tactic:
refine Nat.le_induction (X D.le_refl) (λ n h4 h5 h6 ↦ ?_) K h3
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
X : ∀ {M : ℕ}, D ≤ M → 2 • b M < c M → c (M + 1) = c M
n : ℕ
h4 : D ≤ n
h5 : 2 • b n < c n → c (n + 1) = c D
h6 : 2 • b (n + 1) < c (n + 1)
⊢ c (n + 1 + 1) = c D
Theorem: IMOSL.IMO2017A4.c_succ_eq_D_of_b_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
X : ∀ {M : ℕ}, D ≤ M → 2 • b M < c M → c (M + 1) = c M
n : ℕ
h4 : D ≤ n
h5 : 2 • b n < c n → c (n + 1) = c D
h6 : 2 • b (n + 1) < c (n + 1)
⊢ c (n + 1 + 1) = c D
Tactic:
rw [X (Nat.le_step h4) h6]
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
X : ∀ {M : ℕ}, D ≤ M → 2 • b M < c M → c (M + 1) = c M
n : ℕ
h4 : D ≤ n
h5 : 2 • b n < c n → c (n + 1) = c D
h6 : 2 • b (n + 1) < c (n + 1)
⊢ c n.succ = c D
Theorem: IMOSL.IMO2017A4.c_succ_eq_D_of_b_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
K : ℕ
h2 : Monotone c
h3 : D ≤ K
X : ∀ {M : ℕ}, D ≤ M → 2 • b M < c M → c (M + 1) = c M
n : ℕ
h4 : D ≤ n
h5 : 2 • b n < c n → c (n + 1) = c D
h6 : 2 • b (n + 1) < c (n + 1)
⊢ c n.succ = c D
Tactic:
exact h5 (lt_of_not_le λ h7 ↦ h6.not_le (c_bdd h h0 h1 h4 h7).2)
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n : ℕ
⊢ max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
have h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D)) := by
  refine max_le (le_max_of_two_nsmul_le_add ?_) (le_max_left _ _)
  rw [← nsmul_add, add_sub_cancel]
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
⊢ max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
⊢ max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
refine (le_total n D).elim (λ h4 ↦ h3.trans' (max_le_max (h2 h4) (nsmul_le_nsmul_right (h1 h4) 2)))
  (Nat.le_induction h3 (λ n h4 h5 ↦ ?_) n)
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
rcases le_or_lt (c n) (2 • b n) with h6 | h6
Proof state after:
case inl
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : c n ≤ 2 • b n
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))

case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : 2 • b n < c n
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n : ℕ
⊢ max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
refine max_le (le_max_of_two_nsmul_le_add ?_) (le_max_left _ _)
Proof state after:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n : ℕ
⊢ 2 • c D ≤ 2 • b D + 2 • (c D - b D)
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n : ℕ
⊢ 2 • c D ≤ 2 • b D + 2 • (c D - b D)
Tactic:
rw [← nsmul_add, add_sub_cancel]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inl
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : c n ≤ 2 • b n
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
rcases c_bdd h h0 h1 h4 h6 with ⟨h7, h8⟩
Proof state after:
case inl.intro
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : c n ≤ 2 • b n
h7 : b (n + 1) = b n
h8 : c (n + 1) ≤ 2 • b (n + 1)
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inl.intro
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : c n ≤ 2 • b n
h7 : b (n + 1) = b n
h8 : c (n + 1) ≤ 2 • b (n + 1)
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
rwa [max_eq_right h8, h7, ← max_eq_right h6]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : 2 • b n < c n
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
have h7 := c_succ_eq_D_of_b_bdd h h0 h1 h2 h4 h6
Proof state after:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : 2 • b n < c n
h7 : c (n + 1) = c D
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : 2 • b n < c n
h7 : c (n + 1) = c D
⊢ max (c (n + 1)) (2 • b (n + 1)) ≤ max (2 • b D) (2 • (c D - b D))
Tactic:
refine max_le (h7 ▸ h3.trans' (le_max_left _ _))
  (le_max_of_le_right <| nsmul_le_nsmul_right ((h _ h4).trans ?_) 2)
Proof state after:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : 2 • b n < c n
h7 : c (n + 1) = c D
⊢ max (b n) (c n - b n) ≤ c D - b D
Theorem: IMOSL.IMO2017A4.max_two_nsmul_b_and_c_bdd
Proof state before:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : 2 • b n < c n
h7 : c (n + 1) = c D
⊢ max (b n) (c n - b n) ≤ c D - b D
Tactic:
rw [two_nsmul, ← lt_sub_iff_add_lt] at h6
Proof state after:
case inr
G : Type u_1
D : ℕ
inst✝ : LinearOrderedAddCommGroup G
b c : ℕ → G
h : ∀ (n : ℕ), D ≤ n → b (n + 1) ≤ max (b n) (c n - b n)
h0 : ∀ (n : ℕ), D ≤ n → c (n + 1) ≤ max (c n) (2 • b n)
h1 : Monotone b
h2 : Monotone c
n✝ : ℕ
h3 : max (c D) (2 • b D) ≤ max (2 • b D) (2 • (c D - b D))
n : ℕ
h4 : D ≤ n
h5 : max (c n) (2 • b n) ≤ max (2 • b D) (2 • (c D - b D))
h6 : b n < c n - b n
h7 : c (n + 1) = c D
⊢ max (b n) (c n - b n) ≤ c D - b D