[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
have h1 : m - n + n = m := tsub_add_cancel_of_le h
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m
[PROOFSTEP]
rw [← pow_add, h1]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a 0
[GOAL]
case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m✝ n✝ m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹
[PROOFSTEP]
rw [zero_pow (tsub_pos_of_lt h), zero_pow (n.zero_le.trans_lt h), zero_mul]
[GOAL]
case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
exact pow_sub₀ _ ha h.le
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
[PROOFSTEP]
rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
[PROOFSTEP]
rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0
[PROOFSTEP]
rw [zpow_ofNat, zero_pow']
[GOAL]
case a
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : -[n+1] ≠ 0
⊢ 0 ^ -[n+1] = 0
[PROOFSTEP]
simp
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1
[PROOFSTEP]
rw [h, zpow_zero]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
[PROOFSTEP]
rw [zero_zpow _ h]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a
[PROOFSTEP]
simp only [← Int.ofNat_succ, zpow_ofNat, pow_succ']
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a ^ (-[0+1] + 1) = a ^ -[0+1] * a
[PROOFSTEP]
erw [zpow_zero, zpow_negSucc, pow_one, inv_mul_cancel ha]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = a ^ -[n + 1+1] * a
[PROOFSTEP]
rw [Int.negSucc_eq, zpow_neg, neg_add, neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ, zpow_ofNat, zpow_ofNat,
  pow_succ _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel ha, mul_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
[PROOFSTEP]
rw [mul_assoc, mul_inv_cancel ha, mul_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
[PROOFSTEP]
rw [← zpow_add_one₀ ha, sub_add_cancel]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
induction' n using Int.induction_on with n ihn n ihn
[GOAL]
case hz
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
[PROOFSTEP]
simp
[GOAL]
case hp
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)
[PROOFSTEP]
simp only [← add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
[GOAL]
case hn
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
[PROOFSTEP]
rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, add_sub_assoc]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
by_cases hm : m = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
simp [hm]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
subst a
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : 0 ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n
[PROOFSTEP]
simp only [false_or_iff, eq_self_iff_true, not_true, Ne.def, hm, hn, false_and_iff, or_false_iff] at h 
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n
[PROOFSTEP]
rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
exact zpow_add₀ ha m n
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i
[PROOFSTEP]
rw [zpow_add₀ h, zpow_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)
[PROOFSTEP]
simp [h.pow_right n]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ -[n+1]) (y ^ -[n+1])
[PROOFSTEP]
simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ^ bit1 n = a ^ n * a ^ n * a
[PROOFSTEP]
rw [← zpow_bit0, bit1, zpow_add', zpow_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ≠ 0 ∨ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
[PROOFSTEP]
right
[GOAL]
case h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
[PROOFSTEP]
left
[GOAL]
case h.h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0
[PROOFSTEP]
apply bit1_ne_zero
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ ↑a✝ ≠ 0
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ a✝ ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ ha
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ -[a✝+1] ≠ 0
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ (a ^ (a✝ + 1))⁻¹ ≠ 0
[PROOFSTEP]
exact inv_ne_zero (pow_ne_zero _ ha)
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
z1 z2 : ℤ
⊢ a ^ (z1 - z2) = a ^ z1 / a ^ z2
[PROOFSTEP]
rw [sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ^ bit1 n = (a * a) ^ n * a
[PROOFSTEP]
rw [zpow_bit1₀, (Commute.refl a).mul_zpow]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ x ^ (-n) * x ^ n = 1
[PROOFSTEP]
rw [zpow_neg]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ (x ^ n)⁻¹ * x ^ n = 1
[PROOFSTEP]
exact inv_mul_cancel (zpow_ne_zero n h)
[GOAL]
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
⊢ a ^ 2 * b / a = a * b
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a = 0
⊢ a ^ 2 * b / a = a * b
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : ¬a = 0
⊢ a ^ 2 * b / a = a * b
[PROOFSTEP]
rw [sq, mul_assoc, mul_div_cancel_left _ ha]
