case zero
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
⊢ a ^ Nat.zero ~ᵤ b ^ Nat.zero

case succ
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ Nat.succ n ~ᵤ b ^ Nat.succ n
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
n : ℕ
h : a ~ᵤ b
⊢ a ^ n ~ᵤ b ^ n
induction' n with n ih
no goals
case succ
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ Nat.succ n ~ᵤ b ^ Nat.succ n
convert h.mul_mul ih <;> rw [pow_succ]
case zero
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
⊢ 1 ~ᵤ 1
case zero
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
⊢ a ^ Nat.zero ~ᵤ b ^ Nat.zero
simp [h]
no goals
case zero
α : Type u_1
β : Type ?u.188347
γ : Type ?u.188350
δ : Type ?u.188353
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
⊢ 1 ~ᵤ 1
rfl