R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → Nat.binCast m = ↑m) → Nat.binCast n = ↑n
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ Nat.binCast n = ↑n
apply Nat.strongInductionOn n
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < k → Nat.binCast m = ↑m
⊢ Nat.binCast k = ↑k
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → Nat.binCast m = ↑m) → Nat.binCast n = ↑n
intros k hk
no goals
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
hk : ∀ (m : ℕ), m < zero → Nat.binCast m = ↑m
⊢ Nat.binCast zero = ↑zero
rw [Nat.binCast, Nat.cast_zero]
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
⊢ Nat.binCast (succ k) = ↑(succ k)
rw [Nat.binCast]
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)

case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
by_cases h : (k + 1) % 2 = 0
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k % 2 + 2 * (succ k / 2))
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
rw [←Nat.mod_add_div (succ k) 2]
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ ↑(succ k / 2 + succ k / 2) = ↑(succ k % 2 + 2 * (succ k / 2))
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k % 2 + 2 * (succ k / 2))
rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ←Nat.cast_add]
no goals
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : (k + 1) % 2 = 0
⊢ ↑(succ k / 2 + succ k / 2) = ↑(succ k % 2 + 2 * (succ k / 2))
rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k % 2 + 2 * (succ k / 2))
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k)
rw [←Nat.mod_add_div (succ k) 2]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k % 2 + 2 * (succ k / 2))
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2)
    else Nat.binCast ((k + 1) / 2) + Nat.binCast ((k + 1) / 2) + 1) =
    ↑(succ k % 2 + 2 * (succ k / 2))
rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ←Nat.cast_add]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
h1 : succ k % 2 = 1
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k % 2 + 2 * (succ k / 2))
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k % 2 + 2 * (succ k / 2))
have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
h1 : succ k % 2 = 1
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k / 2 + succ k / 2 + 1)
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
h1 : succ k % 2 = 1
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k % 2 + 2 * (succ k / 2))
rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
no goals
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < succ k → Nat.binCast m = ↑m
h : ¬(k + 1) % 2 = 0
h1 : succ k % 2 = 1
⊢ ↑(succ k / 2 + succ k / 2) + 1 = ↑(succ k / 2 + succ k / 2 + 1)
simp only [Nat.cast_add, Nat.cast_one]