G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ≠ 0 ∨ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ^ bit1 n = a ^ n * a ^ n * a
rw [← zpow_bit0, bit1, zpow_add', zpow_one]
case h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ≠ 0 ∨ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
right
case h.h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0
case h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
left
no goals
case h.h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0
apply bit1_ne_zero