case zero
n m : ℕ
inst✝ : NeZero zero
k : Fin zero
⊢ ↑(bit1 k) = bit1 ↑k % zero

case succ
n m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
k : Fin (Nat.succ n✝)
⊢ ↑(bit1 k) = bit1 ↑k % Nat.succ n✝
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ ↑(bit1 k) = bit1 ↑k % n
cases n
no goals
case succ
n m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
k : Fin (Nat.succ n✝)
⊢ ↑(bit1 k) = bit1 ↑k % Nat.succ n✝
simp [bit1, Fin.val_bit0, Fin.val_add, Fin.val_one]
case zero.mk
n m : ℕ
inst✝ : NeZero zero
k : ℕ
h : k < zero
⊢ ↑(bit1 { val := k, isLt := h }) = bit1 ↑{ val := k, isLt := h } % zero
case zero
n m : ℕ
inst✝ : NeZero zero
k : Fin zero
⊢ ↑(bit1 k) = bit1 ↑k % zero
cases' k with k h
case zero.mk.zero
n m : ℕ
inst✝ : NeZero zero
h : zero < zero
⊢ ↑(bit1 { val := zero, isLt := h }) = bit1 ↑{ val := zero, isLt := h } % zero

case zero.mk.succ
n m : ℕ
inst✝ : NeZero zero
n✝ : ℕ
h : Nat.succ n✝ < zero
⊢ ↑(bit1 { val := Nat.succ n✝, isLt := h }) = bit1 ↑{ val := Nat.succ n✝, isLt := h } % zero
case zero.mk
n m : ℕ
inst✝ : NeZero zero
k : ℕ
h : k < zero
⊢ ↑(bit1 { val := k, isLt := h }) = bit1 ↑{ val := k, isLt := h } % zero
cases k
no goals
case zero.mk.succ
n m : ℕ
inst✝ : NeZero zero
n✝ : ℕ
h : Nat.succ n✝ < zero
⊢ ↑(bit1 { val := Nat.succ n✝, isLt := h }) = bit1 ↑{ val := Nat.succ n✝, isLt := h } % zero
cases' h with _ h
case zero.mk.zero
n m : ℕ
inst✝ : NeZero zero
h : zero < zero
⊢ ((zero + zero) % zero + 1 % zero) % zero = bit1 ↑{ val := zero, isLt := h } % zero
case zero.mk.zero
n m : ℕ
inst✝ : NeZero zero
h : zero < zero
⊢ ↑(bit1 { val := zero, isLt := h }) = bit1 ↑{ val := zero, isLt := h } % zero
show _ % _ = _
no goals
case zero.mk.zero
n m : ℕ
inst✝ : NeZero zero
h : zero < zero
⊢ ((zero + zero) % zero + 1 % zero) % zero = bit1 ↑{ val := zero, isLt := h } % zero
simp