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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ UInt.lsb a = 0 → a = 0
Tactic:
intro h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ a = 0

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ a = 0
Tactic:
suffices UInt.toNat a = 0 by
  apply UInt.toNat_inj; rw [UInt.toNat_ofNat, Nat.zero_mod]; exact this
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ toNat a = 0

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ toNat a = 0
Tactic:
have : (UInt.toNat a).lsb = 0 := by
  rw [←UInt.toNat_lsb, h, UInt.toNat_ofNat, Nat.zero_mod]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : Nat.lsb (toNat a) = 0
⊢ toNat a = 0

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : Nat.lsb (toNat a) = 0
⊢ toNat a = 0
Tactic:
exact Nat.eq_zero_of_lsb_eq_zero this
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ a = 0
Tactic:
apply UInt.toNat_inj
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = toNat 0

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = toNat 0
Tactic:
rw [UInt.toNat_ofNat, Nat.zero_mod]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = 0

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = 0
Tactic:
exact this
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ Nat.lsb (toNat a) = 0
Tactic:
rw [←UInt.toNat_lsb, h, UInt.toNat_ofNat, Nat.zero_mod]
State after:
no goals