[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a : M
b c : ℕ
⊢ (a ^ if P then b else c) = if P then a ^ b else a ^ c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a : M
b c : ℕ
h✝ : P
⊢ a ^ b = a ^ b
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a : M
b c : ℕ
h✝ : ¬P
⊢ a ^ c = a ^ c
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a b : M
c : ℕ
⊢ (if P then a else b) ^ c = if P then a ^ c else b ^ c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a b : M
c : ℕ
h✝ : P
⊢ a ^ c = a ^ c
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Pow M ℕ
P : Prop
inst✝ : Decidable P
a b : M
c : ℕ
h✝ : ¬P
⊢ b ^ c = b ^ c
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
n : ℕ
⊢ n • 0 = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
⊢ Nat.zero • 0 = 0
[PROOFSTEP]
exact zero_nsmul _
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
n : ℕ
ih : n • 0 = 0
⊢ Nat.succ n • 0 = 0
[PROOFSTEP]
rw [succ_nsmul, ih, add_zero]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
⊢ 1 • a = a
[PROOFSTEP]
rw [succ_nsmul, zero_nsmul, add_zero]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
m n : ℕ
⊢ (m + n) • a = m • a + n • a
[PROOFSTEP]
induction m with
| zero => rw [Nat.zero_add, zero_nsmul, zero_add]
| succ m ih => rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
m n : ℕ
⊢ (m + n) • a = m • a + n • a
[PROOFSTEP]
induction m with
| zero => rw [Nat.zero_add, zero_nsmul, zero_add]
| succ m ih => rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
n : ℕ
⊢ (Nat.zero + n) • a = Nat.zero • a + n • a
[PROOFSTEP]

| zero => rw [Nat.zero_add, zero_nsmul, zero_add]
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
n : ℕ
⊢ (Nat.zero + n) • a = Nat.zero • a + n • a
[PROOFSTEP]
rw [Nat.zero_add, zero_nsmul, zero_add]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
n m : ℕ
ih : (m + n) • a = m • a + n • a
⊢ (Nat.succ m + n) • a = Nat.succ m • a + n • a
[PROOFSTEP]

| succ m ih => rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
n m : ℕ
ih : (m + n) • a = m • a + n • a
⊢ (Nat.succ m + n) • a = Nat.succ m • a + n • a
[PROOFSTEP]
rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
n : ℕ
⊢ 1 ^ n = 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
⊢ 1 ^ Nat.zero = 1
[PROOFSTEP]
exact pow_zero _
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
n : ℕ
ih : 1 ^ n = 1
⊢ 1 ^ Nat.succ n = 1
[PROOFSTEP]
rw [pow_succ, ih, one_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
⊢ a ^ 1 = a
[PROOFSTEP]
rw [pow_succ, pow_zero, mul_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
⊢ a ^ 2 = a * a
[PROOFSTEP]
rw [pow_succ, pow_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
⊢ a ^ 3 = a * a * a
[PROOFSTEP]
rw [pow_succ', pow_two]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
⊢ a ^ 3 = a * (a * a)
[PROOFSTEP]
rw [pow_succ, pow_two]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m : ℕ
⊢ a ^ (m + Nat.zero) = a ^ m * a ^ Nat.zero
[PROOFSTEP]
rw [Nat.add_zero, pow_zero, mul_one]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + Nat.succ n) = a ^ m * a ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', Nat.add_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ m) ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m : ℕ
⊢ a ^ (m * Nat.zero) = (a ^ m) ^ Nat.zero
[PROOFSTEP]
rw [Nat.mul_zero, pow_zero, pow_zero]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
ih : a ^ (m * n) = (a ^ m) ^ n
⊢ a ^ (m * Nat.succ n) = (a ^ m) ^ Nat.succ n
[PROOFSTEP]
rw [Nat.mul_succ, pow_add, pow_succ', ih]
  -- Porting note: we are taking the opportunity to swap the names `mul_nsmul` and `mul_nsmul'`
  -- using #align, so that in mathlib4 they will match the multiplicative ones.
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ n) ^ m
[PROOFSTEP]
rw [Nat.mul_comm, pow_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : Commute a b
n : ℕ
⊢ (a * b) ^ n = a ^ n * b ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : Commute a b
⊢ (a * b) ^ Nat.zero = a ^ Nat.zero * b ^ Nat.zero
[PROOFSTEP]
rw [pow_zero, pow_zero, pow_zero, one_mul]
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : Commute a b
n : ℕ
ih : (a * b) ^ n = a ^ n * b ^ n
⊢ (a * b) ^ Nat.succ n = a ^ Nat.succ n * b ^ Nat.succ n
[PROOFSTEP]
simp only [pow_succ, ih, ← mul_assoc, (h.pow_left n).right_comm]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M
inst✝¹ : AddMonoid A
P : Prop
inst✝ : Decidable P
a : M
⊢ (a ^ if P then 1 else 0) = if P then a else 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
⊢ (a ^ m) ^ n = (a ^ n) ^ m
[PROOFSTEP]
rw [← pow_mul, Nat.mul_comm, pow_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n
[PROOFSTEP]
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n
[PROOFSTEP]
rw [← pow_add, Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_2
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % n)
[PROOFSTEP]
have t : x ^ m = x ^ (n * (m / n) + m % n) :=
  congr_arg (fun a => x ^ a) ((Nat.add_comm _ _).trans (Nat.mod_add_div _ _)).symm
[GOAL]
α : Type u_1
M✝ : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
M : Type u_2
inst✝ : Monoid M
x : M
m n : ℕ
h : x ^ n = 1
t : x ^ m = x ^ (n * (m / n) + m % n)
⊢ x ^ m = x ^ (m % n)
[PROOFSTEP]
rw [t, pow_add, pow_mul, h, one_pow, one_mul]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
n : ℕ
⊢ a ^ bit1 n = a ^ n * a ^ n * a
[PROOFSTEP]
rw [bit1, pow_succ', pow_bit0]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
n : ℕ
⊢ a ^ bit0 n = (a * a) ^ n
[PROOFSTEP]
rw [pow_bit0, (Commute.refl a).mul_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
n : ℕ
⊢ a ^ bit1 n = (a * a) ^ n * a
[PROOFSTEP]
rw [bit1, pow_succ', pow_bit0']
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * b ^ n = 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : a * b = 1
⊢ a ^ Nat.zero * b ^ Nat.zero = 1
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ Nat.succ n * b ^ Nat.succ n = 1
[PROOFSTEP]
calc
  a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n) := by rw [pow_succ', pow_succ]
  _ = a ^ n * (a * b) * b ^ n := by simp only [mul_assoc]
  _ = 1 := by simp [h, hn]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ Nat.succ n * b ^ Nat.succ n = a ^ n * a * (b * b ^ n)
[PROOFSTEP]
rw [pow_succ', pow_succ]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ n * a * (b * b ^ n) = a ^ n * (a * b) * b ^ n
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a b : M
h : a * b = 1
n : ℕ
hn : a ^ n * b ^ n = 1
⊢ a ^ n * (a * b) * b ^ n = 1
[PROOFSTEP]
simp [h, hn]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
x y : M
hxy : x ∣ y
n : ℕ
x✝ : n + 1 ≠ 0
⊢ x ∣ y ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
x y : M
hxy : x ∣ y
n : ℕ
x✝ : n + 1 ≠ 0
⊢ x ∣ y * y ^ n
[PROOFSTEP]
exact hxy.mul_right _
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 1 = a
[PROOFSTEP]
convert pow_one a using 1
[GOAL]
case h.e'_2
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 1 = a ^ 1
[PROOFSTEP]
exact zpow_ofNat a 1
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 2 = a * a
[PROOFSTEP]
convert pow_two a using 1
[GOAL]
case h.e'_2
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 2 = a ^ 2
[PROOFSTEP]
exact zpow_ofNat a 2
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
⊢ a⁻¹ ^ 0 = (a ^ 0)⁻¹
[PROOFSTEP]
rw [pow_zero, pow_zero, inv_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℕ
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹
[PROOFSTEP]
rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a b : α
n : ℕ
⊢ 1 ^ ↑n = 1
[PROOFSTEP]
rw [zpow_ofNat, one_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a b : α
n : ℕ
⊢ 1 ^ Int.negSucc n = 1
[PROOFSTEP]
rw [zpow_negSucc, one_pow, inv_one]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
⊢ a ^ (-0) = (a ^ 0)⁻¹
[PROOFSTEP]
change a ^ (0 : ℤ) = (a ^ (0 : ℤ))⁻¹
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
⊢ a ^ 0 = (a ^ 0)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹
[PROOFSTEP]
rw [zpow_negSucc, inv_inv, ← zpow_ofNat]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = a ^ ↑(n + 1)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b✝ a b : α
⊢ (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
[PROOFSTEP]
simp only [zpow_neg, zpow_one, mul_inv_rev]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℕ
⊢ a⁻¹ ^ ↑n = (a ^ ↑n)⁻¹
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, inv_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℕ
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, inv_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℤ
⊢ a⁻¹ ^ n = a ^ (-n)
[PROOFSTEP]
rw [inv_zpow, zpow_neg]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n
[PROOFSTEP]
simp only [one_div, inv_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b a : α
n : ℤ
⊢ (1 / a) ^ n = 1 / a ^ n
[PROOFSTEP]
simp only [one_div, inv_zpow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a b : α
h : Commute a b
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n
[PROOFSTEP]
simp [zpow_ofNat, h.mul_pow n]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a b : α
h : Commute a b
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
[PROOFSTEP]
simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a / b) ^ n = a ^ n / b ^ n
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_pow, inv_pow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionCommMonoid α
a b : α
n : ℤ
⊢ (a / b) ^ n = a ^ n / b ^ n
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_zpow, inv_zpow]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : AddGroup A
inst✝ : AddGroup B
a : G
m n : ℕ
h : n ≤ m
⊢ a ^ (m - n) * a ^ n = a ^ m
[PROOFSTEP]
rw [← pow_add, Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : AddGroup A
inst✝ : AddGroup B
a : G
m n : ℕ
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
[PROOFSTEP]
rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Monoid R
a : R
m n : ℕ
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)
[PROOFSTEP]
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)
[PROOFSTEP]
simp [zpow_ofNat, h.pow_right n]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)
[PROOFSTEP]
simp only [zpow_negSucc, inv_right_iff]
[GOAL]
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
[PROOFSTEP]
apply pow_right h
