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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ a ≠ 0 → ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
intro ha
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
⊢ ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
this : ∃ i, UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
cases this with | intro i hi =>
suffices ∀ j, UInt.getBit (UInt.lsb a) j = decide (i = j) from ⟨i, this⟩
intro j
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›
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 := ‹_›
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

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

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

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

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

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

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

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