[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
⊢ ↑(if P then m else n) = if P then ↑m else ↑n
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : P
⊢ ↑m = ↑m
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : ¬P
⊢ ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1
[PROOFSTEP]
rw [cast_succ, Nat.cast_zero, zero_add]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
⊢ ↑(m + n) = ↑m + ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ ↑(m + zero) = ↑m + ↑zero
[PROOFSTEP]
simp [add_succ, add_assoc, Nat.add_zero, Nat.cast_one, Nat.cast_zero, *]
[GOAL]
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n✝ : ℕ
n_ih✝ : ↑(m + n✝) = ↑m + ↑n✝
⊢ ↑(m + succ n✝) = ↑m + ↑(succ n✝)
[PROOFSTEP]
simp [add_succ, add_assoc, Nat.add_zero, Nat.cast_one, Nat.cast_zero, *]
[GOAL]
n : ℕ
h✝ : (n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
n : ℕ
h✝ : (n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
n : ℕ
h✝ : ¬(n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
n : ℕ
h✝ : ¬(n + 1) % 2 = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 ((n + 1) / 2) (succ n)
[PROOFSTEP]
exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ Nat.binCast n = ↑n
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → Nat.binCast m = ↑m) → Nat.binCast n = ↑n
[PROOFSTEP]
intros k hk
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < k → Nat.binCast m = ↑m
⊢ Nat.binCast k = ↑k
[PROOFSTEP]
cases k with
| zero => rw [Nat.binCast, Nat.cast_zero]
| succ k =>
  rw [Nat.binCast]
  by_cases h : (k + 1) % 2 = 0
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
    rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
    simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n k : ℕ
hk : ∀ (m : ℕ), m < k → Nat.binCast m = ↑m
⊢ Nat.binCast k = ↑k
[PROOFSTEP]
cases k with
| zero => rw [Nat.binCast, Nat.cast_zero]
| succ k =>
  rw [Nat.binCast]
  by_cases h : (k + 1) % 2 = 0
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
    rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
    simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
hk : ∀ (m : ℕ), m < zero → Nat.binCast m = ↑m
⊢ Nat.binCast zero = ↑zero
[PROOFSTEP]

| zero => rw [Nat.binCast, Nat.cast_zero]
[GOAL]
case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
hk : ∀ (m : ℕ), m < zero → Nat.binCast m = ↑m
⊢ Nat.binCast zero = ↑zero
[PROOFSTEP]
rw [Nat.binCast, Nat.cast_zero]
[GOAL]
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)
[PROOFSTEP]

| succ k =>
  rw [Nat.binCast]
  by_cases h : (k + 1) % 2 = 0
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
  · rw [← Nat.mod_add_div (succ k) 2]
    rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
    have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
    rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
    simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
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)
[PROOFSTEP]
rw [Nat.binCast]
[GOAL]
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)
[PROOFSTEP]
by_cases h : (k + 1) % 2 = 0
[GOAL]
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)
[PROOFSTEP]
rw [← Nat.mod_add_div (succ k) 2]
[GOAL]
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))
[PROOFSTEP]
rw [if_pos h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
[GOAL]
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))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
[GOAL]
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)
[PROOFSTEP]
rw [← Nat.mod_add_div (succ k) 2]
[GOAL]
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))
[PROOFSTEP]
rw [if_neg h, hk _ $ Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
[GOAL]
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))
[PROOFSTEP]
have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
[GOAL]
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))
[PROOFSTEP]
rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
[GOAL]
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)
[PROOFSTEP]
simp only [Nat.cast_add, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑(bit1 n) = bit1 ↑n
[PROOFSTEP]
rw [bit1, cast_add_one, cast_bit0]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ bit0 ↑n + 1 = bit1 ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp only [Nat.binCast, Nat.cast]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
dsimp only [NatCast.natCast]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
n : ℕ
⊢ Nat.binCast (n + 1) = Nat.binCast n + 1
[PROOFSTEP]
letI : AddMonoidWithOne R := AddMonoidWithOne.unary
[GOAL]
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
src✝¹ : One R := inst✝
src✝ : AddMonoid R := inst✝¹
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ Nat.binCast (n + 1) = Nat.binCast n + 1
[PROOFSTEP]
rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
h : NeZero ↑n
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
h : NeZero ↑0
⊢ False
[PROOFSTEP]
exact h.out Nat.cast_zero
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add]
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1) = 2
[PROOFSTEP]
apply congrArg
[GOAL]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 2 + 1 = 3
[PROOFSTEP]
rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1 + 1) = 3
[PROOFSTEP]
apply congrArg
[GOAL]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 + 1 = 3
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 3 + 1 = 4
[PROOFSTEP]
rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]
[GOAL]
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1 + 1 + 1) = 4
[PROOFSTEP]
apply congrArg
[GOAL]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 + 1 + 1 = 4
[PROOFSTEP]
decide
