internlm/Lean-Github huggingface dataset:
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
have : UInt.getBit (UInt.lsb a) i₀ = true := decide_eq_true (Eq.refl i₀) ▸ (hi₀ i₀)
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this : UInt.getBit (UInt.lsb a) i₀ = true
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this : UInt.getBit (UInt.lsb a) i₀ = true
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
have ⟨_, (halow: ∀ j, j < i₀ → UInt.getBit a j = false)⟩ :=
  (UInt.getBit_lsb_iff a).mp this
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
suffices UInt.toNat (UInt.ctz a) = i₀ by
  rw [this]; intro hi; exact halow _ hi
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
⊢ toNat (UInt.ctz a) = i₀
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
⊢ toNat (UInt.ctz a) = i₀
Tactic:
have : decide (i₀ = toNat (UInt.ctz a)) = true :=
  hi₀ _ ▸ UInt.getBit_lsb_ctz a ha
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : decide (i₀ = toNat (UInt.ctz a)) = true
⊢ toNat (UInt.ctz a) = i₀
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : decide (i₀ = toNat (UInt.ctz a)) = true
⊢ toNat (UInt.ctz a) = i₀
Tactic:
apply Eq.symm
Proof state after:
case intro.h
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : decide (i₀ = toNat (UInt.ctz a)) = true
⊢ i₀ = toNat (UInt.ctz a)
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
case intro.h
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : decide (i₀ = toNat (UInt.ctz a)) = true
⊢ i₀ = toNat (UInt.ctz a)
Tactic:
exact of_decide_eq_true this
Proof state after:
no goals
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : toNat (UInt.ctz a) = i₀
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
rw [this]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : toNat (UInt.ctz a) = i₀
⊢ i < i₀ → UInt.getBit a i = false
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : toNat (UInt.ctz a) = i₀
⊢ i < i₀ → UInt.getBit a i = false
Tactic:
intro hi
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : toNat (UInt.ctz a) = i₀
hi : i < i₀
⊢ UInt.getBit a i = false
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
i₀ : Nat
hi₀ : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
this✝ : UInt.getBit (UInt.lsb a) i₀ = true
left✝ : UInt.getBit a i₀ = true
halow : ∀ (j : Nat), j < i₀ → UInt.getBit a j = false
this : toNat (UInt.ctz a) = i₀
hi : i < i₀
⊢ UInt.getBit a i = false
Tactic:
exact halow _ hi
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ UInt.bitIndices a ↔ UInt.getBit a i = true
Tactic:
suffices ∀ (n : Nat), i ∈ UInt.bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true by 
  constructor
  case mp => intro h; exact ((this (length α)).mp h).right
  case mpr =>
    intro h
    have hi : i < length α :=
      (Nat.lt_or_ge i (length α)).elim id (λ hi => by cases (UInt.getBit_high a i hi ▸ h))
    exact (this (length α)).mpr ⟨hi, h⟩
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
Tactic:
intro n
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
⊢ i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
⊢ i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
Tactic:
induction n
Proof state after:
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero ↔ i < Nat.zero ∧ UInt.getBit a i = true

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n✝ : Nat
n_ih✝ : i ∈ bitIndices.aux a n✝ ↔ i < n✝ ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a (Nat.succ n✝) ↔ i < Nat.succ n✝ ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero ↔ i < Nat.zero ∧ UInt.getBit a i = true
Tactic:
case zero =>
  constructor
  . intro h; cases h
  . intro h; cases h.left
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a (Nat.succ n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case succ n h_ind =>
  dsimp [bitIndices.aux]
  cases hbit : UInt.getBit a n
  case false =>
    simp [h_ind]
    intro h
    have : i ≠ n := λ hcontra => by cases (hbit ▸ hcontra ▸ h)
    constructor
    . exact Nat.lt_succ_of_lt
    . intro hle; exact Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hle) ‹i≠n›
  case true =>
    simp
    constructor
    . intro h
      cases h
      case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
      case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
    . intro h
      cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
      case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
      case inr heq => cases heq; exact Or.inl rfl
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ UInt.bitIndices a ↔ UInt.getBit a i = true
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ UInt.bitIndices a → UInt.getBit a i = true

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ UInt.getBit a i = true → i ∈ UInt.bitIndices a
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ UInt.bitIndices a → UInt.getBit a i = true
Tactic:
case mp => intro h; exact ((this (length α)).mp h).right
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ UInt.getBit a i = true → i ∈ UInt.bitIndices a
Tactic:
case mpr =>
  intro h
  have hi : i < length α :=
    (Nat.lt_or_ge i (length α)).elim id (λ hi => by cases (UInt.getBit_high a i hi ▸ h))
  exact (this (length α)).mpr ⟨hi, h⟩
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ UInt.bitIndices a → UInt.getBit a i = true
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : i ∈ UInt.bitIndices a
⊢ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : i ∈ UInt.bitIndices a
⊢ UInt.getBit a i = true
Tactic:
exact ((this (length α)).mp h).right
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ UInt.getBit a i = true → i ∈ UInt.bitIndices a
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : UInt.getBit a i = true
⊢ i ∈ UInt.bitIndices a
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : UInt.getBit a i = true
⊢ i ∈ UInt.bitIndices a
Tactic:
have hi : i < length α :=
  (Nat.lt_or_ge i (length α)).elim id (λ hi => by cases (UInt.getBit_high a i hi ▸ h))
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : UInt.getBit a i = true
hi : i < length α
⊢ i ∈ UInt.bitIndices a
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : UInt.getBit a i = true
hi : i < length α
⊢ i ∈ UInt.bitIndices a
Tactic:
exact (this (length α)).mpr ⟨hi, h⟩
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
this : ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
h : UInt.getBit a i = true
hi : i ≥ length α
⊢ i < length α
Tactic:
cases (UInt.getBit_high a i hi ▸ h)
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero ↔ i < Nat.zero ∧ UInt.getBit a i = true
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero → i < Nat.zero ∧ UInt.getBit a i = true

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i < Nat.zero ∧ UInt.getBit a i = true → i ∈ bitIndices.aux a Nat.zero
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero → i < Nat.zero ∧ UInt.getBit a i = true

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i < Nat.zero ∧ UInt.getBit a i = true → i ∈ bitIndices.aux a Nat.zero
Tactic:
. intro h; cases h
Proof state after:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i < Nat.zero ∧ UInt.getBit a i = true → i ∈ bitIndices.aux a Nat.zero
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i < Nat.zero ∧ UInt.getBit a i = true → i ∈ bitIndices.aux a Nat.zero
Tactic:
. intro h; cases h.left
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero → i < Nat.zero ∧ UInt.getBit a i = true
Tactic:
intro h
Proof state after:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : i ∈ bitIndices.aux a Nat.zero
⊢ i < Nat.zero ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : i ∈ bitIndices.aux a Nat.zero
⊢ i < Nat.zero ∧ UInt.getBit a i = true
Tactic:
cases h
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i < Nat.zero ∧ UInt.getBit a i = true → i ∈ bitIndices.aux a Nat.zero
Tactic:
intro h
Proof state after:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : i < Nat.zero ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a Nat.zero
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : i < Nat.zero ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a Nat.zero
Tactic:
cases h.left
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a (Nat.succ n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
dsimp [bitIndices.aux]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ (i ∈ if UInt.getBit a n = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔
    i < Nat.succ n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
⊢ (i ∈ if UInt.getBit a n = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔
    i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
cases hbit : UInt.getBit a n
Proof state after:
case false
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
⊢ (i ∈ if false = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true

case true
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ (i ∈ if true = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
⊢ (i ∈ if false = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case false =>
  simp [h_ind]
  intro h
  have : i ≠ n := λ hcontra => by cases (hbit ▸ hcontra ▸ h)
  constructor
  . exact Nat.lt_succ_of_lt
  . intro hle; exact Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hle) ‹i≠n›
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ (i ∈ if true = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case true =>
  simp
  constructor
  . intro h
    cases h
    case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
    case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
  . intro h
    cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
    case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
    case inr heq => cases heq; exact Or.inl rfl
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
⊢ (i ∈ if false = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
simp [h_ind]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
⊢ UInt.getBit a i = true → (i < n ↔ i < Nat.succ n)
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
⊢ UInt.getBit a i = true → (i < n ↔ i < Nat.succ n)
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
⊢ i < n ↔ i < Nat.succ n
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
⊢ i < n ↔ i < Nat.succ n
Tactic:
have : i ≠ n := λ hcontra => by cases (hbit ▸ hcontra ▸ h)
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < n ↔ i < Nat.succ n
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < n ↔ i < Nat.succ n
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < n → i < Nat.succ n

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < Nat.succ n → i < n
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < n → i < Nat.succ n

case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < Nat.succ n → i < n
Tactic:
. exact Nat.lt_succ_of_lt
Proof state after:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < Nat.succ n → i < n
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < Nat.succ n → i < n
Tactic:
. intro hle; exact Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hle) ‹i≠n›
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
hcontra : i = n
⊢ False
Tactic:
cases (hbit ▸ hcontra ▸ h)
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
case mp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < n → i < Nat.succ n
Tactic:
exact Nat.lt_succ_of_lt
Proof state after:
no goals
Theorem: UInt.Mem_bitIndices
Proof state before:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
⊢ i < Nat.succ n → i < n
Tactic:
intro hle
Proof state after:
case mpr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = false
h : UInt.getBit a i = true
this : i ≠ n
hle : i < Nat.succ n
⊢ i < n