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

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
if ha : a = 0
then intros; rw [ha, UInt.getBit_zero]
else
  have : ∃ i₀, ∀ j, UInt.getBit (UInt.lsb a) j = decide (i₀=j) := UInt.lsb_singleton a ha
  cases this with | intro i₀ hi₀ =>
  have : UInt.getBit (UInt.lsb a) i₀ = true := decide_eq_true (Eq.refl i₀) ▸ (hi₀ i₀)
  have ⟨_, (halow: ∀ j, j < i₀ → UInt.getBit a j = false)⟩ :=
    (UInt.getBit_lsb_iff a).mp this
  suffices UInt.toNat (UInt.ctz a) = i₀ by
    rw [this]; intro hi; exact halow _ hi
  have : decide (i₀ = toNat (UInt.ctz a)) = true :=
    hi₀ _ ▸ UInt.getBit_lsb_ctz a ha
  apply Eq.symm; exact of_decide_eq_true this
State after:
no goals

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : a = 0
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
intros
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : a = 0
a✝ : i < toNat (UInt.ctz a)
⊢ UInt.getBit a i = false

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : a = 0
a✝ : i < toNat (UInt.ctz a)
⊢ UInt.getBit a i = false
Tactic:
rw [ha, UInt.getBit_zero]
State after:
no goals

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
have : ∃ i₀, ∀ j, UInt.getBit (UInt.lsb a) j = decide (i₀=j) := UInt.lsb_singleton a ha
State after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
this : ∃ i₀, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false

State before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
this : ∃ i₀, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
cases this with | intro i₀ hi₀ =>
have : UInt.getBit (UInt.lsb a) i₀ = true := decide_eq_true (Eq.refl i₀) ▸ (hi₀ i₀)
have ⟨_, (halow: ∀ j, j < i₀ → UInt.getBit a j = false)⟩ :=
  (UInt.getBit_lsb_iff a).mp this
suffices UInt.toNat (UInt.ctz a) = i₀ by
  rw [this]; intro hi; exact halow _ hi
have : decide (i₀ = toNat (UInt.ctz a)) = true :=
  hi₀ _ ▸ UInt.getBit_lsb_ctz a ha
apply Eq.symm; exact of_decide_eq_true this
State after:
no goals

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

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

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

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

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

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

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

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

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