no goals
α : Type ?u.4429
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
split_ifs <;> rfl