Theorem: IMOSL.IMO2017A4.c_succ_eq_D_of_b_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 : 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)
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

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

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

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