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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
intro i
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
cases Nat.eq_zero_or_pos (length α)
State after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
h✝ : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
h✝ : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
case inl hzero =>
  simp only [hzero, decide_eq_false, Bool.false_and]
  calc
    UInt.getBit (α:=α) 1 i
      = UInt.getBit (α:=α) 0 i := by rw [UInt.eq_of_length_eq_zero hzero 1 0]
    _ = false := UInt.getBit_zero i
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
case inr hpos =>
  rw [decide_eq_true hpos, Bool.true_and]
  dsimp [UInt.getBit]; rw [UInt.toNat_ofNat]
  have := calc
    1 ≤ length α := hpos
    _ < 2^length α := Nat.exp_lt_pow _ .refl
  rw [Nat.mod_eq_of_lt this]
  calc
    Nat.getBit 1 i = decide (0 = i) := Nat.getBit_two_pow 0 i
    _              = decide (i = 0) := decide_eq_decide.mpr ⟨Eq.symm, Eq.symm⟩
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
simp only [hzero, decide_eq_false, Bool.false_and]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = false

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = false
Tactic:
calc
  UInt.getBit (α:=α) 1 i
    = UInt.getBit (α:=α) 0 i := by rw [UInt.eq_of_length_eq_zero hzero 1 0]
  _ = false := UInt.getBit_zero i
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = UInt.getBit 0 i
Tactic:
rw [UInt.eq_of_length_eq_zero hzero 1 0]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
rw [decide_eq_true hpos, Bool.true_and]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = decide (i = 0)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = decide (i = 0)
Tactic:
dsimp [UInt.getBit]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (toNat 1) i = decide (i = 0)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (toNat 1) i = decide (i = 0)
Tactic:
rw [UInt.toNat_ofNat]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
Tactic:
have := calc
  1 ≤ length α := hpos
  _ < 2^length α := Nat.exp_lt_pow _ .refl
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
Tactic:
rw [Nat.mod_eq_of_lt this]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit 1 i = decide (i = 0)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit 1 i = decide (i = 0)
Tactic:
calc
  Nat.getBit 1 i = decide (0 = i) := Nat.getBit_two_pow 0 i
  _              = decide (i = 0) := decide_eq_decide.mpr ⟨Eq.symm, Eq.symm⟩
State after:
no goals