Theorem: UInt.Mem_bitIndices (Algdata/Classes/UInt.lean)

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⟩
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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⟩
State after:
no goals

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
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

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
State after:
no goals

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
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

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))
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

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⟩
State after:
no goals

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)
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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]
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

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
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

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›
State after:
no goals

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
State after:
no goals

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]
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)

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
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

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)
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

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
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

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
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

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›
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
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

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
hle : i < Nat.succ n
⊢ i < n
Tactic:
exact Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hle) ‹i≠n›
State after:
no goals

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:
simp
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 = true
⊢ i = n ∨ i ∈ bitIndices.aux a n ↔ i < Nat.succ n ∧ UInt.getBit a i = true

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 = n ∨ i ∈ bitIndices.aux a n ↔ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
constructor
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 = true
⊢ i = n ∨ i ∈ bitIndices.aux a n → i < Nat.succ n ∧ UInt.getBit a i = true

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 = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n

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 = true
⊢ i = n ∨ i ∈ bitIndices.aux a n → i < Nat.succ n ∧ UInt.getBit a i = true

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 = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Tactic:
. 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⟩
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 = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n

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 = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Tactic:
. 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
State after:
no goals

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 = true
⊢ i = n ∨ i ∈ bitIndices.aux a n → i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
intro h
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 = true
h : i = n ∨ i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true

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 = true
h : i = n ∨ i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
cases h
State after:
case mp.inl
α : 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
h✝ : i = n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true

case mp.inr
α : 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
h✝ : i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true

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
h : i = n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
State after:
no goals

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
h : i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
State after:
no goals

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
h : i = n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
cases h
State after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
⊢ i < Nat.succ i ∧ UInt.getBit a i = true

State before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
⊢ i < Nat.succ i ∧ UInt.getBit a i = true
Tactic:
exact ⟨i.lt_succ_self, hbit⟩
State after:
no goals

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
h : i ∈ bitIndices.aux a n
⊢ i < Nat.succ n ∧ UInt.getBit a i = true
Tactic:
exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
State after:
no goals

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 = true
⊢ i < Nat.succ n ∧ UInt.getBit a i = true → i = n ∨ i ∈ bitIndices.aux a n
Tactic:
intro h
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 = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
⊢ i = n ∨ i ∈ bitIndices.aux a n

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 = true
h : i < Nat.succ n ∧ UInt.getBit a i = true
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
State after:
case mpr.inl
α : 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
h : i < Nat.succ n ∧ UInt.getBit a i = true
h✝ : i < n
⊢ i = n ∨ i ∈ bitIndices.aux a n

case mpr.inr
α : 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
h : i < Nat.succ n ∧ UInt.getBit a i = true
h✝ : i = n
⊢ i = n ∨ i ∈ bitIndices.aux a n

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
h : i < Nat.succ n ∧ UInt.getBit a i = true
hlt : i < n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
State after:
no goals

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
h : i < Nat.succ n ∧ UInt.getBit a i = true
heq : i = n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
case inr heq => cases heq; exact Or.inl rfl
State after:
no goals

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
h : i < Nat.succ n ∧ UInt.getBit a i = true
hlt : i < n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
State after:
no goals

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
h : i < Nat.succ n ∧ UInt.getBit a i = true
heq : i = n
⊢ i = n ∨ i ∈ bitIndices.aux a n
Tactic:
cases heq
State after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
h : i < Nat.succ i ∧ UInt.getBit a i = true
⊢ i = i ∨ i ∈ bitIndices.aux a i

State before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h_ind : i ∈ bitIndices.aux a i ↔ i < i ∧ UInt.getBit a i = true
hbit : UInt.getBit a i = true
h : i < Nat.succ i ∧ UInt.getBit a i = true
⊢ i = i ∨ i ∈ bitIndices.aux a i
Tactic:
exact Or.inl rfl
State after:
no goals