Theorem: IMOSL.IMO2017A4.c_bdd (IMOSLLean4/IMO2017/A4/A4.lean)

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)⟩
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)

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
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)

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))
State after:
no goals