internlm/Lean-Github huggingface dataset:
Theorem: Int.odd_part_le_self_nat
Proof state before:
case zero

⊢ ∀ (y : ℕ), y ≤ zero → (val_bin_nat y).snd ≤ zero
Tactic:
intro y h
Proof state after:
case zero
y : ℕ
h : y ≤ zero
⊢ (val_bin_nat y).snd ≤ zero
Theorem: Int.odd_part_le_self_nat
Proof state before:
case zero
y : ℕ
h : y ≤ zero
⊢ (val_bin_nat y).snd ≤ zero
Tactic:
rw [le_zero_eq] at h
Proof state after:
case zero
y : ℕ
h : y = 0
⊢ (val_bin_nat y).snd ≤ zero
Theorem: Int.odd_part_le_self_nat
Proof state before:
case zero
y : ℕ
h : y = 0
⊢ (val_bin_nat y).snd ≤ zero
Tactic:
rw [h]
Proof state after:
case zero
y : ℕ
h : y = 0
⊢ (val_bin_nat 0).snd ≤ zero
Theorem: Int.odd_part_le_self_nat
Proof state before:
case zero
y : ℕ
h : y = 0
⊢ (val_bin_nat 0).snd ≤ zero
Tactic:
exact Nat.zero_le 0
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
⊢ ∀ (y : ℕ), y ≤ Nat.succ x → (val_bin_nat y).snd ≤ Nat.succ x
Tactic:
intro y y_le_sx
Proof state after:
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
y : ℕ
y_le_sx : y ≤ Nat.succ x
⊢ (val_bin_nat y).snd ≤ Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
y : ℕ
y_le_sx : y ≤ Nat.succ x
⊢ (val_bin_nat y).snd ≤ Nat.succ x
Tactic:
cases y_le_sx with
| refl =>
  cases mod_two_eq_zero_or_one (Nat.succ x) with
  | inl even =>
    have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
    And.intro (zero_lt_succ x) even;
    show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
    let vbn_half := val_bin_nat (Nat.succ x / 2);
    (vbn_half.fst + 1, vbn_half.snd)
    else if 0 < Nat.succ x then
    (0, Nat.succ x)
    else
    (0, 0)).snd ≤ Nat.succ x
    rw [if_pos h]
    have h' := ih (Nat.succ x / 2) (div2_succ_le_self x);
    exact le_trans h' (le_succ x)
  | inr odd =>
    show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
    let vbn_half := val_bin_nat (Nat.succ x / 2);
    (vbn_half.fst + 1, vbn_half.snd)
    else if 0 < Nat.succ x then
    (0, Nat.succ x)
    else
    (0, 0)).snd ≤ Nat.succ x
    have not_even : Nat.succ x % 2 ≠ 0 := by
      rw [odd]
      simp;
    rw [if_neg (not_and_of_not_right (0 < Nat.succ x) not_even)]
    rw [if_pos (zero_lt_succ x)]
| step y_le_x => exact le_trans (ih y y_le_x) (le_succ x);
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
⊢ (val_bin_nat (Nat.succ x)).snd ≤ Nat.succ x
Tactic:
cases mod_two_eq_zero_or_one (Nat.succ x) with
| inl even =>
  have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
  And.intro (zero_lt_succ x) even;
  show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
  let vbn_half := val_bin_nat (Nat.succ x / 2);
  (vbn_half.fst + 1, vbn_half.snd)
  else if 0 < Nat.succ x then
  (0, Nat.succ x)
  else
  (0, 0)).snd ≤ Nat.succ x
  rw [if_pos h]
  have h' := ih (Nat.succ x / 2) (div2_succ_le_self x);
  exact le_trans h' (le_succ x)
| inr odd =>
  show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
  let vbn_half := val_bin_nat (Nat.succ x / 2);
  (vbn_half.fst + 1, vbn_half.snd)
  else if 0 < Nat.succ x then
  (0, Nat.succ x)
  else
  (0, 0)).snd ≤ Nat.succ x
  have not_even : Nat.succ x % 2 ≠ 0 := by
    rw [odd]
    simp;
  rw [if_neg (not_and_of_not_right (0 < Nat.succ x) not_even)]
  rw [if_pos (zero_lt_succ x)]
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
⊢ (val_bin_nat (Nat.succ x)).snd ≤ Nat.succ x
Tactic:
have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
And.intro (zero_lt_succ x) even
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (val_bin_nat (Nat.succ x)).snd ≤ Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (val_bin_nat (Nat.succ x)).snd ≤ Nat.succ x
Tactic:
show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
let vbn_half := val_bin_nat (Nat.succ x / 2);
(vbn_half.fst + 1, vbn_half.snd)
else if 0 < Nat.succ x then
(0, Nat.succ x)
else
(0, 0)).snd ≤ Nat.succ x
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤
    Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤
    Nat.succ x
Tactic:
rw [if_pos h]
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)).snd ≤
    Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
⊢ (let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)).snd ≤
    Nat.succ x
Tactic:
have h' := ih (Nat.succ x / 2) (div2_succ_le_self x)
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
h' : (val_bin_nat (Nat.succ x / 2)).snd ≤ x
⊢ (let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)).snd ≤
    Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
even : Nat.succ x % 2 = 0
h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0
h' : (val_bin_nat (Nat.succ x / 2)).snd ≤ x
⊢ (let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)).snd ≤
    Nat.succ x
Tactic:
exact le_trans h' (le_succ x)
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
⊢ (val_bin_nat (Nat.succ x)).snd ≤ Nat.succ x
Tactic:
show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
let vbn_half := val_bin_nat (Nat.succ x / 2);
(vbn_half.fst + 1, vbn_half.snd)
else if 0 < Nat.succ x then
(0, Nat.succ x)
else
(0, 0)).snd ≤ Nat.succ x
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
⊢ (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤
    Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
⊢ (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤
    Nat.succ x
Tactic:
have not_even : Nat.succ x % 2 ≠ 0 := by
  rw [odd]
  simp;
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
not_even : Nat.succ x % 2 ≠ 0
⊢ (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤
    Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
not_even : Nat.succ x % 2 ≠ 0
⊢ (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤
    Nat.succ x
Tactic:
rw [if_neg (not_and_of_not_right (0 < Nat.succ x) not_even)]
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
not_even : Nat.succ x % 2 ≠ 0
⊢ (if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤ Nat.succ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
not_even : Nat.succ x % 2 ≠ 0
⊢ (if 0 < Nat.succ x then (0, Nat.succ x) else (0, 0)).snd ≤ Nat.succ x
Tactic:
rw [if_pos (zero_lt_succ x)]
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
⊢ Nat.succ x % 2 ≠ 0
Tactic:
rw [odd]
Proof state after:
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
⊢ 1 ≠ 0
Theorem: Int.odd_part_le_self_nat
Proof state before:
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
odd : Nat.succ x % 2 = 1
⊢ 1 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
case succ.step
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
y : ℕ
y_le_x : Nat.le y x
⊢ (val_bin_nat y).snd ≤ Nat.succ x
Tactic:
exact le_trans (ih y y_le_x) (le_succ x)
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
x : ℕ
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
Tactic:
have acc : ∀ y, (y ≤ x → 0 < (val_bin_nat (Nat.succ y)).2) := by
  induction x with
  | zero =>
    intro y y_le_x
    rw [le_zero_eq] at y_le_x
    rw [y_le_x]
    exact Nat.lt_succ_self 0 | succ x ih =>
    intro y y_le_sx
    cases y_le_sx with
    | refl =>
      cases mod_two_eq_zero_or_one (Nat.succ (Nat.succ x)) with
      | inl even =>
        have h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 :=
        And.intro (zero_lt_succ (Nat.succ x)) even;
        show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
        else if 0 < Nat.succ (Nat.succ x) then
        (0, Nat.succ (Nat.succ x))
        else
        (0, 0)).snd
        rw [if_pos h, div2_succ_succ_eq_succ_div2]
        exact ih (x / 2) (Nat.div_le_self x 2)
      | inr odd =>
        show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
        else if 0 < Nat.succ (Nat.succ x) then
        (0, Nat.succ (Nat.succ x))
        else
        (0, 0)).snd
        have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
          rw [odd]
          simp;
        rw [if_neg (not_and_of_not_right (0 < Nat.succ (Nat.succ x)) not_even)]
        rw [if_pos (zero_lt_succ (Nat.succ x))]
        exact zero_lt_succ (Nat.succ x)
    | step y_le_x => exact ih y y_le_x;
Proof state after:
x : ℕ
acc : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
x : ℕ
acc : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
Tactic:
exact acc x (le_refl x)
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
x : ℕ
⊢ ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
induction x with
| zero =>
  intro y y_le_x
  rw [le_zero_eq] at y_le_x
  rw [y_le_x]
  exact Nat.lt_succ_self 0 | succ x ih =>
  intro y y_le_sx
  cases y_le_sx with
  | refl =>
    cases mod_two_eq_zero_or_one (Nat.succ (Nat.succ x)) with
    | inl even =>
      have h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 :=
      And.intro (zero_lt_succ (Nat.succ x)) even;
      show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
      let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
      (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then
      (0, Nat.succ (Nat.succ x))
      else
      (0, 0)).snd
      rw [if_pos h, div2_succ_succ_eq_succ_div2]
      exact ih (x / 2) (Nat.div_le_self x 2)
    | inr odd =>
      show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
      let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
      (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then
      (0, Nat.succ (Nat.succ x))
      else
      (0, 0)).snd
      have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
        rw [odd]
        simp;
      rw [if_neg (not_and_of_not_right (0 < Nat.succ (Nat.succ x)) not_even)]
      rw [if_pos (zero_lt_succ (Nat.succ x))]
      exact zero_lt_succ (Nat.succ x)
  | step y_le_x => exact ih y y_le_x;
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
case zero

⊢ ∀ (y : ℕ), y ≤ zero → 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
intro y y_le_x
Proof state after:
case zero
y : ℕ
y_le_x : y ≤ zero
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case zero
y : ℕ
y_le_x : y ≤ zero
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
rw [le_zero_eq] at y_le_x
Proof state after:
case zero
y : ℕ
y_le_x : y = 0
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case zero
y : ℕ
y_le_x : y = 0
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
rw [y_le_x]
Proof state after:
case zero
y : ℕ
y_le_x : y = 0
⊢ 0 < (val_bin_nat (Nat.succ 0)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case zero
y : ℕ
y_le_x : y = 0
⊢ 0 < (val_bin_nat (Nat.succ 0)).snd
Tactic:
exact Nat.lt_succ_self 0
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
⊢ ∀ (y : ℕ), y ≤ Nat.succ x → 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
intro y y_le_sx
Proof state after:
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
y : ℕ
y_le_sx : y ≤ Nat.succ x
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
y : ℕ
y_le_sx : y ≤ Nat.succ x
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
cases y_le_sx with
| refl =>
  cases mod_two_eq_zero_or_one (Nat.succ (Nat.succ x)) with
  | inl even =>
    have h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 :=
    And.intro (zero_lt_succ (Nat.succ x)) even;
    show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
    let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
    (vbn_half.fst + 1, vbn_half.snd)
    else if 0 < Nat.succ (Nat.succ x) then
    (0, Nat.succ (Nat.succ x))
    else
    (0, 0)).snd
    rw [if_pos h, div2_succ_succ_eq_succ_div2]
    exact ih (x / 2) (Nat.div_le_self x 2)
  | inr odd =>
    show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
    let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
    (vbn_half.fst + 1, vbn_half.snd)
    else if 0 < Nat.succ (Nat.succ x) then
    (0, Nat.succ (Nat.succ x))
    else
    (0, 0)).snd
    have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
      rw [odd]
      simp;
    rw [if_neg (not_and_of_not_right (0 < Nat.succ (Nat.succ x)) not_even)]
    rw [if_pos (zero_lt_succ (Nat.succ x))]
    exact zero_lt_succ (Nat.succ x)
| step y_le_x => exact ih y y_le_x;
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
⊢ 0 < (val_bin_nat (Nat.succ (Nat.succ x))).snd
Tactic:
cases mod_two_eq_zero_or_one (Nat.succ (Nat.succ x)) with
| inl even =>
  have h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 :=
  And.intro (zero_lt_succ (Nat.succ x)) even;
  show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
  let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
  (vbn_half.fst + 1, vbn_half.snd)
  else if 0 < Nat.succ (Nat.succ x) then
  (0, Nat.succ (Nat.succ x))
  else
  (0, 0)).snd
  rw [if_pos h, div2_succ_succ_eq_succ_div2]
  exact ih (x / 2) (Nat.div_le_self x 2)
| inr odd =>
  show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
  let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
  (vbn_half.fst + 1, vbn_half.snd)
  else if 0 < Nat.succ (Nat.succ x) then
  (0, Nat.succ (Nat.succ x))
  else
  (0, 0)).snd
  have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
    rw [odd]
    simp;
  rw [if_neg (not_and_of_not_right (0 < Nat.succ (Nat.succ x)) not_even)]
  rw [if_pos (zero_lt_succ (Nat.succ x))]
  exact zero_lt_succ (Nat.succ x)
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 < (val_bin_nat (Nat.succ (Nat.succ x))).snd
Tactic:
have h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 :=
And.intro (zero_lt_succ (Nat.succ x)) even
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 < (val_bin_nat (Nat.succ (Nat.succ x))).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 < (val_bin_nat (Nat.succ (Nat.succ x))).snd
Tactic:
show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
(vbn_half.fst + 1, vbn_half.snd)
else if 0 < Nat.succ (Nat.succ x) then
(0, Nat.succ (Nat.succ x))
else
(0, 0)).snd
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Tactic:
rw [if_pos h, div2_succ_succ_eq_succ_div2]
Proof state after:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 <
    (let vbn_half := val_bin_nat (Nat.succ (x / 2));
      (vbn_half.fst + 1, vbn_half.snd)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inl
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
even : Nat.succ (Nat.succ x) % 2 = 0
h : 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0
⊢ 0 <
    (let vbn_half := val_bin_nat (Nat.succ (x / 2));
      (vbn_half.fst + 1, vbn_half.snd)).snd
Tactic:
exact ih (x / 2) (Nat.div_le_self x 2)
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 0 < (val_bin_nat (Nat.succ (Nat.succ x))).snd
Tactic:
show 0 < (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
(vbn_half.fst + 1, vbn_half.snd)
else if 0 < Nat.succ (Nat.succ x) then
(0, Nat.succ (Nat.succ x))
else
(0, 0)).snd
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Tactic:
have not_even : Nat.succ (Nat.succ x) % 2 ≠ 0 := by
  rw [odd]
  simp;
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 <
    (if 0 < Nat.succ (Nat.succ x) ∧ Nat.succ (Nat.succ x) % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ (Nat.succ x) / 2);
        (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Tactic:
rw [if_neg (not_and_of_not_right (0 < Nat.succ (Nat.succ x)) not_even)]
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 < (if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 < (if 0 < Nat.succ (Nat.succ x) then (0, Nat.succ (Nat.succ x)) else (0, 0)).snd
Tactic:
rw [if_pos (zero_lt_succ (Nat.succ x))]
Proof state after:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 < (0, Nat.succ (Nat.succ x)).snd
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.refl.inr
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
not_even : Nat.succ (Nat.succ x) % 2 ≠ 0
⊢ 0 < (0, Nat.succ (Nat.succ x)).snd
Tactic:
exact zero_lt_succ (Nat.succ x)
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ Nat.succ (Nat.succ x) % 2 ≠ 0
Tactic:
rw [odd]
Proof state after:
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 1 ≠ 0
Theorem: Int.odd_part_succ_pos
Proof state before:
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
odd : Nat.succ (Nat.succ x) % 2 = 1
⊢ 1 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Int.odd_part_succ_pos
Proof state before:
case succ.step
x : ℕ
ih : ∀ (y : ℕ), y ≤ x → 0 < (val_bin_nat (Nat.succ y)).snd
y : ℕ
y_le_x : Nat.le y x
⊢ 0 < (val_bin_nat (Nat.succ y)).snd
Tactic:
exact ih y y_le_x
Proof state after:
no goals