Theorem: getBitRes_apply_two_pow (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ (getBitRes i) ⟨2 ^ ↑i, ⋯⟩ = (true, 0)
Tactic:
ext
State after:
case a
m : ℕ
i : Fin (m + 1)
⊢ ((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).1 = (true, 0).1

case a.h
m : ℕ
i : Fin (m + 1)
⊢ ↑((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).2 = ↑(true, 0).2

State before:
case a
m : ℕ
i : Fin (m + 1)
⊢ ((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).1 = (true, 0).1
Tactic:
simp only [getBitRes_apply, finFunctionFinEquiv, Equiv.ofRightInverseOfCardLE_symm_apply,
gt_iff_lt, zero_lt_two, pow_pos, Nat.div_self, Nat.one_mod, Fin.mk_one, finTwoEquiv_apply,
decide_True, Equiv.ofRightInverseOfCardLE_apply]
State after:
no goals

State before:
case a.h
m : ℕ
i : Fin (m + 1)
⊢ ↑((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).2 = ↑(true, 0).2
Tactic:
simp only [getBitRes_apply, finFunctionFinEquiv_apply_val, finFunctionFinEquiv_symm_apply_val,
Fin.val_zero', Finset.sum_eq_zero_iff, Finset.mem_univ, mul_eq_zero, forall_true_left]
State after:
case a.h
m : ℕ
i : Fin (m + 1)
⊢ ∀ (x : Fin m), 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0 ∨ 2 ^ ↑x = 0

State before:
case a.h
m : ℕ
i : Fin (m + 1)
⊢ ∀ (x : Fin m), 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0 ∨ 2 ^ ↑x = 0
Tactic:
refine' fun x => Or.inl _
State after:
case a.h
m : ℕ
i : Fin (m + 1)
x : Fin m
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0

State before:
case a.h
m : ℕ
i : Fin (m + 1)
x : Fin m
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Tactic:
rcases (Fin.succAbove_ne i x).lt_or_lt with h | h <;> rw [Fin.lt_iff_val_lt_val] at h
State after:
case a.h.inl
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑(i.succAbove x) < ↑i
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0

case a.h.inr
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑i < ↑(i.succAbove x)
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0

State before:
case a.h.inl
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑(i.succAbove x) < ↑i
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Tactic:
rw [Nat.pow_div h.le zero_lt_two, Nat.pow_mod, Nat.mod_self,
  Nat.zero_pow (Nat.sub_pos_of_lt h), Nat.zero_mod]
State after:
no goals

State before:
case a.h.inr
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑i < ↑(i.succAbove x)
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Tactic:
rw [Nat.div_eq_of_lt (pow_lt_pow_right one_lt_two h), Nat.zero_mod]
State after:
no goals