Theorem: IMOSL.IMO2022A1.final_solution (IMOSLLean4/IMO2022/A1/A1.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
N : ℕ
h1 : 2 ≤ N
⊢ a N ≤ 1
Tactic:
have h2 (i : ℕ) (h1 : 1 < a (i + 1)) (h2 : 1 < a (i + 2)) : False :=
  (main_ineq h1.le h2 (h _) (h0 _)).asymm <| main_ineq2 (h i) h1 h2.le (h0 _)
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
N : ℕ
h1 : 2 ≤ N
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
⊢ a N ≤ 1

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
N : ℕ
h1 : 2 ≤ N
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
⊢ a N ≤ 1
Tactic:
rcases Nat.exists_eq_add_of_le' h1 with ⟨n, rfl⟩
State after:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1 : 2 ≤ n + 2
⊢ a (n + 2) ≤ 1

State before:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1 : 2 ≤ n + 2
⊢ a (n + 2) ≤ 1
Tactic:
refine le_of_not_lt λ h1 ↦ (h0 (n + 1)).not_lt ?_
State after:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + a (n + 1 + 2) < a (n + 1 + 1) ^ 2 + a (n + 1) * a (n + 1 + 2)

State before:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + a (n + 1 + 2) < a (n + 1 + 1) ^ 2 + a (n + 1) * a (n + 1 + 2)
Tactic:
rw [← sub_lt_iff_lt_add, add_sub_assoc, ← one_sub_mul]
State after:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + (1 - a (n + 1)) * a (n + 1 + 2) < a (n + 1 + 1) ^ 2

State before:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + (1 - a (n + 1)) * a (n + 1 + 2) < a (n + 1 + 1) ^ 2
Tactic:
exact (one_lt_pow h1 <| Nat.succ_ne_zero 1).trans_le' <|
  add_le_of_le_sub_left <| mul_le_of_le_one_right
    (sub_nonneg_of_le <| le_of_not_lt <| λ h3 ↦ h2 _ h3 h1)
    (le_of_not_lt <| h2 _ h1)
State after:
no goals