[GOAL]
n✝ n : ℕ
⊢ boddDiv2 n = (bodd n, div2 n)
[PROOFSTEP]
unfold bodd div2
[GOAL]
n✝ n : ℕ
⊢ boddDiv2 n = ((boddDiv2 n).fst, (boddDiv2 n).snd)
[PROOFSTEP]
cases boddDiv2 n
[GOAL]
case mk
n✝ n : ℕ
fst✝ : Bool
snd✝ : ℕ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
h : m = n
⊢ bit0 m = bit0 n
[PROOFSTEP]
subst h
[GOAL]
n m : ℕ
⊢ bit0 m = bit0 m
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
h : m = n
⊢ bit1 m = bit1 n
[PROOFSTEP]
subst h
[GOAL]
n m : ℕ
⊢ bit1 m = bit1 m
[PROOFSTEP]
rfl
[GOAL]
n✝ n : ℕ
h : n = 0
⊢ bit1 n = 1
[PROOFSTEP]
subst h
[GOAL]
n : ℕ
⊢ bit1 0 = 1
[PROOFSTEP]
rfl
[GOAL]
n✝ n : ℕ
h : n = 0
⊢ 1 = bit1 n
[PROOFSTEP]
subst h
[GOAL]
n : ℕ
⊢ 1 = bit1 0
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0
[PROOFSTEP]
cases b <;> [exact Nat.bit0_ne_zero h; exact Nat.bit1_ne_zero _]
[GOAL]
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0
[PROOFSTEP]
cases b
[GOAL]
case false
n✝ n : ℕ
h : n ≠ 0
⊢ bit false n ≠ 0
[PROOFSTEP]
exact Nat.bit0_ne_zero h
[GOAL]
case true
n✝ n : ℕ
h : n ≠ 0
⊢ bit true n ≠ 0
[PROOFSTEP]
exact Nat.bit1_ne_zero _
[GOAL]
n : ℕ
⊢ bit0 n % 2 = 0
[PROOFSTEP]
rw [Nat.mod_two_of_bodd]
[GOAL]
n : ℕ
⊢ (bif bodd (bit0 n) then 1 else 0) = 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ bit1 n % 2 = 1
[PROOFSTEP]
rw [Nat.mod_two_of_bodd]
[GOAL]
n : ℕ
⊢ (bif bodd (bit1 n) then 1 else 0) = 1
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
h : 0 < bit0 n
⊢ 0 < n
[PROOFSTEP]
cases n
[GOAL]
case zero
n : ℕ
h : 0 < bit0 zero
⊢ 0 < zero
[PROOFSTEP]
cases h
[GOAL]
case succ
n n✝ : ℕ
h : 0 < bit0 (succ n✝)
⊢ 0 < succ n✝
[PROOFSTEP]
apply succ_pos
[GOAL]
n✝ : ℕ
C : ℕ → Sort u
H : (b : Bool) → (n : ℕ) → C (bit b n)
b : Bool
n : ℕ
⊢ HEq (H (bodd (bit b n)) (div2 (bit b n))) (H b n)
[PROOFSTEP]
rw [bodd_bit, div2_bit]
[GOAL]
n : ℕ
C : ℕ → Sort u
⊢ Function.Injective fun H n => bitCasesOn n H
[PROOFSTEP]
intro H₁ H₂ h
[GOAL]
n : ℕ
C : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → C (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
⊢ H₁ = H₂
[PROOFSTEP]
ext b n
[GOAL]
case h.h
n✝ : ℕ
C : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → C (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n
[PROOFSTEP]
simpa only [bitCasesOn_bit] using congr_fun h (bit b n)
[GOAL]
n✝ n : ℕ
h : n = 0
⊢ bit0 n = 0
[PROOFSTEP]
simp [h]
[GOAL]
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false
[PROOFSTEP]
constructor
[GOAL]
case mp
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 → n = 0 ∧ b = false
[PROOFSTEP]
cases b
[GOAL]
case mp.false
n✝ n : ℕ
⊢ bit false n = 0 → n = 0 ∧ false = false
[PROOFSTEP]
simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
[GOAL]
case mp.true
n✝ n : ℕ
⊢ bit true n = 0 → n = 0 ∧ true = false
[PROOFSTEP]
simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
[GOAL]
case mpr
n✝ n : ℕ
b : Bool
⊢ n = 0 ∧ b = false → bit b n = 0
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case mpr.intro
n : ℕ
⊢ bit false 0 = 0
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [binaryRec]
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
rcases bit_eq_zero_iff.mp h' with ⟨rfl, rfl⟩
[GOAL]
case pos.intro
n : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z ∨ (0 = 0 → false = true)
h' : bit false 0 = 0
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 (binaryRec z f 0)
[PROOFSTEP]
rw [binaryRec_zero]
[GOAL]
case pos.intro
n : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z ∨ (0 = 0 → false = true)
h' : bit false 0 = 0
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
simp only [imp_false, or_false_iff, eq_self_iff_true, not_true] at h 
[GOAL]
case pos.intro
n : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : bit false 0 = 0
h : f false 0 z = z
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
exact h.symm
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ (let n' := div2 (bit b n);
    let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
    Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
dsimp only []
  -- Porting note: this line was `generalize_proofs e`:
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
generalize
  @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
    (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
  e
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))
⊢ Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
revert e
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))),
    Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [bodd_bit, div2_bit]
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit b n)), Eq.mpr e (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
intros
[GOAL]
case neg
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
b : Bool
n : ℕ
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e✝ : C (bit b n) = C (bit b n)
⊢ Eq.mpr e✝ (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (bit b n)
b : Bool
n : ℕ
ih : C n
h : ¬(n = 0 → b = true)
⊢ C (bit b n)
[PROOFSTEP]
convert z
[GOAL]
case h.e'_1
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (bit b n)
b : Bool
n : ℕ
ih : C n
h : ¬(n = 0 → b = true)
⊢ bit b n = 0
[PROOFSTEP]
rw [bit_eq_zero_iff]
[GOAL]
case h.e'_1
n✝ : ℕ
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (bit b n)
b : Bool
n : ℕ
ih : C n
h : ¬(n = 0 → b = true)
⊢ n = 0 ∧ b = false
[PROOFSTEP]
simpa using h
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z₀ : C 0
z₁ : C 1
f : (b : Bool) → (n : ℕ) → n ≠ 0 → C n → C (bit b n)
b : Bool
n : ℕ
h : n = 0 → b = true
ih : C n
h' : n = 0
⊢ C (bit b n)
[PROOFSTEP]
rw [h', h h']
[GOAL]
n✝ : ℕ
C : ℕ → Sort u_1
z₀ : C 0
z₁ : C 1
f : (b : Bool) → (n : ℕ) → n ≠ 0 → C n → C (bit b n)
b : Bool
n : ℕ
h : n = 0 → b = true
ih : C n
h' : n = 0
⊢ C (bit true 0)
[PROOFSTEP]
exact z₁
[GOAL]
n : ℕ
⊢ bits 0 = []
[PROOFSTEP]
simp [Nat.bits]
[GOAL]
n✝ n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ bits (bit b n) = b :: bits n
[PROOFSTEP]
rw [Nat.bits, binaryRec_eq']
[GOAL]
case h
n✝ n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
⊢ bits 1 = [true]
[PROOFSTEP]
convert bit1_bits 0
[GOAL]
n✝ n : ℕ
⊢ bodd n = List.headI (bits n)
[PROOFSTEP]
induction' n using Nat.binaryRec' with b n h _
[GOAL]
case z
n : ℕ
⊢ bodd 0 = List.headI (bits 0)
[PROOFSTEP]
simp
[GOAL]
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bodd n = List.headI (bits n)
⊢ bodd (bit b n) = List.headI (bits (bit b n))
[PROOFSTEP]
simp [bodd_bit, bits_append_bit _ _ h]
[GOAL]
n✝ n : ℕ
⊢ bits (div2 n) = List.tail (bits n)
[PROOFSTEP]
induction' n using Nat.binaryRec' with b n h _
[GOAL]
case z
n : ℕ
⊢ bits (div2 0) = List.tail (bits 0)
[PROOFSTEP]
simp
[GOAL]
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bits (div2 n) = List.tail (bits n)
⊢ bits (div2 (bit b n)) = List.tail (bits (bit b n))
[PROOFSTEP]
simp [div2_bit, bits_append_bit _ _ h]
