case zero
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
⊢ x • m ^ Nat.zero = (x • m) ^ Nat.zero

case succ
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
ih : x • m ^ n = (x • m) ^ n
⊢ x • m ^ Nat.succ n = (x • m) ^ Nat.succ n
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
⊢ x • m ^ n = (x • m) ^ n
induction' n with n ih
case zero
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
⊢ x • 1 = 1
case zero
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
⊢ x • m ^ Nat.zero = (x • m) ^ Nat.zero
rw [pow_zero, pow_zero]
no goals
case zero
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
⊢ x • 1 = 1
exact smul_one x
case succ
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
ih : x • m ^ n = (x • m) ^ n
⊢ x • (m * m ^ n) = x • m * (x • m) ^ n
case succ
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
ih : x • m ^ n = (x • m) ^ n
⊢ x • m ^ Nat.succ n = (x • m) ^ Nat.succ n
rw [pow_succ, pow_succ]
no goals
case succ
α : Type ?u.75902
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✝³ : Monoid N
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : MulDistribMulAction M N
x : M
m : N
n : ℕ
ih : x • m ^ n = (x • m) ^ n
⊢ x • (m * m ^ n) = x • m * (x • m) ^ n
exact (smul_mul' x m (m ^ n)).trans (congr_arg _ ih)