case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
x a : ℂ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
constructor
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
intro hyp
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
simp only [cpow_def, eq_self_iff_true, if_true] at hyp
case pos
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case neg
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
by_cases x = 0
case pos
a : ℂ
hyp : (if 0 = 0 then 1 else 0) = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
case pos
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
subst h
case pos
a : ℂ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
case pos
a : ℂ
hyp : (if 0 = 0 then 1 else 0) = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
simp only [if_true, eq_self_iff_true] at hyp
case pos.h
a : ℂ
hyp : 1 = a
⊢ 0 = 0 ∧ a = 1
case pos
a : ℂ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
right
no goals
case pos.h
a : ℂ
hyp : 1 = a
⊢ 0 = 0 ∧ a = 1
exact ⟨rfl, hyp.symm⟩
case neg
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
case neg
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
rw [if_neg h] at hyp
case neg.h
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0
case neg
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
left
no goals
case neg.h
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0
exact ⟨h, hyp.symm⟩
case mpr.inl.intro
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

case mpr.inr.intro

⊢ 0 ^ 0 = 1
case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
no goals
case mpr.inl.intro
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0
exact zero_cpow h
no goals
case mpr.inr.intro

⊢ 0 ^ 0 = 1
exact cpow_zero _