Theorem: IMOSL.IMO2021A3.lowerBoundMk_targetSum (IMOSLLean4/IMO2021/A3/A3.lean)

State before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
⊢ targetSum (lowerBoundMk (Nat.bit false (k + 1))) = (Nat.bit false (k + 1)).size
Tactic:
have h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ :=
  congr_arg Nat.succ (lowerBoundMk_length (k + 1))
State after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ targetSum (lowerBoundMk (Nat.bit false (k + 1))) = (Nat.bit false (k + 1)).size

State before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ targetSum (lowerBoundMk (Nat.bit false (k + 1))) = (Nat.bit false (k + 1)).size
Tactic:
rw [lowerBoundMk_bit0_succ, Nat.bit_false, Nat.size_bit0 k.succ_ne_zero,
  (k + 1).size.succ_eq_add_one, targetSum_map_add_iota_length_succ h0,
  targetSum, h0, h, add_comm, Nat.add_right_inj]
State after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ (2 * k + 2) / (k + 1).succ = 1

State before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n k : ℕ
h : targetSum (lowerBoundMk (k + 1)) = (k + 1).size
h0 : ((2 * k + 2) :: lowerBoundMk (k + 1)).length = (k + 1).succ
⊢ (2 * k + 2) / (k + 1).succ = 1
Tactic:
exact Nat.div_eq_of_lt_le
  ((one_mul _).trans_le <| Nat.add_le_add_right (X0 _) 2)
  (Nat.mul_lt_mul_of_pos_left (k + 1).lt_succ_self X)
State after:
no goals

State before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
⊢ targetSum (lowerBoundMk (Nat.bit true n)) = (Nat.bit true n).size
Tactic:
have h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ :=
  congr_arg Nat.succ (lowerBoundMk_length n)
State after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ targetSum (lowerBoundMk (Nat.bit true n)) = (Nat.bit true n).size

State before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ targetSum (lowerBoundMk (Nat.bit true n)) = (Nat.bit true n).size
Tactic:
rw [lowerBoundMk_bit1, Nat.bit_true, Nat.size_bit1,
  targetSum_map_add_iota_length_succ h0, targetSum, h0, h,
  n.size.succ_eq_add_one, add_comm, Nat.add_right_inj]
State after:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ (2 * n + 1) / n.succ = 1

State before:
X : 0 < Nat.succ 1
X0 : ∀ (m : ℕ), m ≤ 2 * m
b : Bool
n✝ n : ℕ
h : targetSum (lowerBoundMk n) = n.size
h0 : ((2 * n + 1) :: lowerBoundMk n).length = n.succ
⊢ (2 * n + 1) / n.succ = 1
Tactic:
exact Nat.div_eq_of_lt_le
  ((one_mul _).trans_le <| Nat.succ_le_succ (X0 _)) (Nat.le_refl _)
State after:
no goals