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

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

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

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

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

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

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

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

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

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

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 : b n < c n - b n
h7 : c (n + 1) = c D
⊢ max (b n) (c n - b n) ≤ c D - b D
Tactic:
rw [max_eq_right h6.le, ← h7]
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
⊢ c n - b n ≤ c (n + 1) - b D

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 : b n < c n - b n
h7 : c (n + 1) = c D
⊢ c n - b n ≤ c (n + 1) - b D
Tactic:
exact sub_le_sub (h2 n.le_succ) (h1 h4)
State after:
no goals