internlm/Lean-Github huggingface dataset:
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ : ∃ i, i < length α ∧ UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Tactic:
. cases ‹∃ i, i < length α ∧ UInt.getBit (UInt.lsb a) i = true› with
  | intro i hi => exact ⟨i, hi.right⟩
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Tactic:
. have hall := ‹∀ i, i < length α → ¬UInt.getBit (UInt.lsb a) i = true›
  suffices a = 0 from absurd this ha
  suffices UInt.lsb a = 0 from UInt.eq_zero_of_lsb_eq_zero a this
  suffices ∀ i, UInt.getBit (UInt.lsb a) i = false by
    apply UInt.bitext; intros; rw [this, UInt.getBit_zero]
  intro i
  cases Nat.lt_or_ge i (length α)
  case inl hlt => exact Bool.not_eq_true _ ▸ hall i hlt
  case inr hge => exact UInt.getBit_high _ _ hge
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ : ∃ i, i < length α ∧ UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Tactic:
cases ‹∃ i, i < length α ∧ UInt.getBit (UInt.lsb a) i = true› with
| intro i hi => exact ⟨i, hi.right⟩
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
case inl.intro
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : i < length α ∧ UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Tactic:
exact ⟨i, hi.right⟩
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Tactic:
have hall := ‹∀ i, i < length α → ¬UInt.getBit (UInt.lsb a) i = true›
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, UInt.getBit (UInt.lsb a) i = true
Tactic:
suffices a = 0 from absurd this ha
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ a = 0
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ a = 0
Tactic:
suffices UInt.lsb a = 0 from UInt.eq_zero_of_lsb_eq_zero a this
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ UInt.lsb a = 0
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ UInt.lsb a = 0
Tactic:
suffices ∀ i, UInt.getBit (UInt.lsb a) i = false by
  apply UInt.bitext; intros; rw [this, UInt.getBit_zero]
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
⊢ ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
Tactic:
intro i
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
⊢ UInt.getBit (UInt.lsb a) i = false
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
⊢ UInt.getBit (UInt.lsb a) i = false
Tactic:
cases Nat.lt_or_ge i (length α)
Proof state after:
case inr.inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝¹ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
h✝ : i < length α
⊢ UInt.getBit (UInt.lsb a) i = false

case inr.inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝¹ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
h✝ : i ≥ length α
⊢ UInt.getBit (UInt.lsb a) i = false
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
hlt : i < length α
⊢ UInt.getBit (UInt.lsb a) i = false
Tactic:
case inl hlt => exact Bool.not_eq_true _ ▸ hall i hlt
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
hge : i ≥ length α
⊢ UInt.getBit (UInt.lsb a) i = false
Tactic:
case inr hge => exact UInt.getBit_high _ _ hge
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
this : ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
⊢ UInt.lsb a = 0
Tactic:
apply UInt.bitext
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
this : ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
⊢ ∀ (i : Nat), i < length α → UInt.getBit (UInt.lsb a) i = UInt.getBit 0 i
Theorem: UInt.lsb_singleton
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
this : ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
⊢ ∀ (i : Nat), i < length α → UInt.getBit (UInt.lsb a) i = UInt.getBit 0 i
Tactic:
intros
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
this : ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
i✝ : Nat
a✝ : i✝ < length α
⊢ UInt.getBit (UInt.lsb a) i✝ = UInt.getBit 0 i✝
Theorem: UInt.lsb_singleton
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
this : ∀ (i : Nat), UInt.getBit (UInt.lsb a) i = false
i✝ : Nat
a✝ : i✝ < length α
⊢ UInt.getBit (UInt.lsb a) i✝ = UInt.getBit 0 i✝
Tactic:
rw [this, UInt.getBit_zero]
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
hlt : i < length α
⊢ UInt.getBit (UInt.lsb a) i = false
Tactic:
exact Bool.not_eq_true _ ▸ hall i hlt
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
h✝ hall : ∀ (i : Nat), i < length α → ¬UInt.getBit (UInt.lsb a) i = true
i : Nat
hge : i ≥ length α
⊢ UInt.getBit (UInt.lsb a) i = false
Tactic:
exact UInt.getBit_high _ _ hge
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
case intro
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
suffices ∀ j, UInt.getBit (UInt.lsb a) j = decide (i = j) from ⟨i, this⟩
Proof state after:
case intro
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
⊢ ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Theorem: UInt.lsb_singleton
Proof state before:
case intro
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
⊢ ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
intro j
Proof state after:
case intro
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
⊢ UInt.getBit (UInt.lsb a) j = decide (i = j)
Theorem: UInt.lsb_singleton
Proof state before:
case intro
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
⊢ UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
if hij : i = j
then exact Eq.trans (hij ▸ hi) (decide_eq_true hij).symm
else
  suffices UInt.getBit (UInt.lsb a) j ≠ true
    by rw [decide_eq_false hij]; exact eq_false_of_ne_true this
  intro hcontra
  cases Nat.lt_or_ge i j
  . have : i < j := ‹_›
    have : UInt.getBit a i = false :=
      ((UInt.getBit_lsb_iff a).mp hcontra).right i this
    have : UInt.getBit a i = true :=
      ((UInt.getBit_lsb_iff a).mp hi).left
    cases Eq.trans ‹UInt.getBit a i = false›.symm ‹UInt.getBit a i = true›
  . have : i > j := Nat.lt_of_le_of_ne ‹i ≥ j› (hij ∘ Eq.symm)
    have : UInt.getBit a j = false :=
      And.right ((UInt.getBit_lsb_iff a).mp hi) j this
    have : UInt.getBit a j = true :=
      ((UInt.getBit_lsb_iff a).mp hcontra).left
    cases Eq.trans ‹UInt.getBit a j = false›.symm ‹UInt.getBit a j = true›
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : i = j
⊢ UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
exact Eq.trans (hij ▸ hi) (decide_eq_true hij).symm
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
⊢ UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
suffices UInt.getBit (UInt.lsb a) j ≠ true
  by rw [decide_eq_false hij]; exact eq_false_of_ne_true this
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
⊢ UInt.getBit (UInt.lsb a) j ≠ true
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
⊢ UInt.getBit (UInt.lsb a) j ≠ true
Tactic:
intro hcontra
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
⊢ False
Tactic:
cases Nat.lt_or_ge i j
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i < j
⊢ False

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i < j
⊢ False

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
⊢ False
Tactic:
. have : i < j := ‹_›
  have : UInt.getBit a i = false :=
    ((UInt.getBit_lsb_iff a).mp hcontra).right i this
  have : UInt.getBit a i = true :=
    ((UInt.getBit_lsb_iff a).mp hi).left
  cases Eq.trans ‹UInt.getBit a i = false›.symm ‹UInt.getBit a i = true›
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
⊢ False
Tactic:
. have : i > j := Nat.lt_of_le_of_ne ‹i ≥ j› (hij ∘ Eq.symm)
  have : UInt.getBit a j = false :=
    And.right ((UInt.getBit_lsb_iff a).mp hi) j this
  have : UInt.getBit a j = true :=
    ((UInt.getBit_lsb_iff a).mp hcontra).left
  cases Eq.trans ‹UInt.getBit a j = false›.symm ‹UInt.getBit a j = true›
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
this : UInt.getBit (UInt.lsb a) j ≠ true
⊢ UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
rw [decide_eq_false hij]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
this : UInt.getBit (UInt.lsb a) j ≠ true
⊢ UInt.getBit (UInt.lsb a) j = false
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
this : UInt.getBit (UInt.lsb a) j ≠ true
⊢ UInt.getBit (UInt.lsb a) j = false
Tactic:
exact eq_false_of_ne_true this
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i < j
⊢ False
Tactic:
have : i < j := ‹_›
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ this : i < j
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ this : i < j
⊢ False
Tactic:
have : UInt.getBit a i = false :=
  ((UInt.getBit_lsb_iff a).mp hcontra).right i this
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ this✝ : i < j
this : UInt.getBit a i = false
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ this✝ : i < j
this : UInt.getBit a i = false
⊢ False
Tactic:
have : UInt.getBit a i = true :=
  ((UInt.getBit_lsb_iff a).mp hi).left
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ this✝¹ : i < j
this✝ : UInt.getBit a i = false
this : UInt.getBit a i = true
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ this✝¹ : i < j
this✝ : UInt.getBit a i = false
this : UInt.getBit a i = true
⊢ False
Tactic:
cases Eq.trans ‹UInt.getBit a i = false›.symm ‹UInt.getBit a i = true›
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
⊢ False
Tactic:
have : i > j := Nat.lt_of_le_of_ne ‹i ≥ j› (hij ∘ Eq.symm)
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
this : i > j
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
this : i > j
⊢ False
Tactic:
have : UInt.getBit a j = false :=
  And.right ((UInt.getBit_lsb_iff a).mp hi) j this
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
this✝ : i > j
this : UInt.getBit a j = false
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
this✝ : i > j
this : UInt.getBit a j = false
⊢ False
Tactic:
have : UInt.getBit a j = true :=
  ((UInt.getBit_lsb_iff a).mp hcontra).left
Proof state after:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
this✝¹ : i > j
this✝ : UInt.getBit a j = false
this : UInt.getBit a j = true
⊢ False
Theorem: UInt.lsb_singleton
Proof state before:
case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
i : Nat
hi : UInt.getBit (UInt.lsb a) i = true
j : Nat
hij : ¬i = j
hcontra : UInt.getBit (UInt.lsb a) j = true
h✝ : i ≥ j
this✝¹ : i > j
this✝ : UInt.getBit a j = false
this : UInt.getBit a j = true
⊢ False
Tactic:
cases Eq.trans ‹UInt.getBit a j = false›.symm ‹UInt.getBit a j = true›
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
Tactic:
let f : α → α × α → α → α × α :=
  λ a₁ z m => (UInt.when ((a₁ &&& m) ≠ 0) z.2 ||| z.1, z.2 <<< 1)
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
Tactic:
let f' : α → Nat → α → α :=
  λ a₁ n x => UInt.when ((a₁ &&& bitmask (OfNat.ofNat n)) ≠ 0) (1 <<< OfNat.ofNat (α:=α) n) ||| x
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
Tactic:
suffices ∀ (a x : α), (maskTable.foldl (f a) (x,1)).1 = Nat.fold (f' a) (Nat.log2RU $ length α) x
  from λ a => this (UInt.lsb a) ..
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a x : α),
    (Array.foldl (f a) (x, 1) maskTable 0 (Array.size maskTable)).fst = Nat.fold (f' a) (Nat.log2RU (length α)) x
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a x : α),
    (Array.foldl (f a) (x, 1) maskTable 0 (Array.size maskTable)).fst = Nat.fold (f' a) (Nat.log2RU (length α)) x
Tactic:
intro a x
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
a x : α
⊢ (Array.foldl (f a) (x, 1) maskTable 0 (Array.size maskTable)).fst = Nat.fold (f' a) (Nat.log2RU (length α)) x
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
a x : α
⊢ (Array.foldl (f a) (x, 1) maskTable 0 (Array.size maskTable)).fst = Nat.fold (f' a) (Nat.log2RU (length α)) x
Tactic:
conv =>
  lhs; unfold maskTable; zeta; rw [Array.foldl_ofFn_eq]; dsimp [flip, Function.comp]
  change (Fin.foldAll ((λ (n : Nat) (z : α × α) => (UInt.when (a &&& bitmask (OfNat.ofNat (α:=α) n) ≠ 0) z.2 ||| z.1, z.2 <<< 1)) ∘ Fin.val (n:=Nat.log2RU $ length α)) (x, 1)).1
  rw [Fin.foldAll_comp_val]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
a x : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (f' a) (Nat.log2RU (length α)) x