case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)

case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)
induction' n with n ih
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (x ^ Nat.zero) (y ^ Nat.zero)
rw [pow_zero, pow_zero]
no goals
case zero
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1
exact SemiconjBy.one_right _
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x * x ^ n) (y * y ^ n)
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ Nat.succ n) (y ^ Nat.succ n)
rw [pow_succ, pow_succ]
no goals
case succ
M : Type u_1
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x * x ^ n) (y * y ^ n)
exact h.mul_right ih