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 : (0 ^ ↑x).re = 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 [rpow_def, Complex.ofReal_zero] at hyp
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
case mp
x a : ℝ
hyp : (0 ^ ↑x).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
by_cases x = 0
case pos
a : ℝ
hyp : (0 ^ ↑0).re = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = 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 : (0 ^ ↑0).re = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
no goals
case pos
a : ℝ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
exact Or.inr ⟨rfl, hyp.symm⟩
case neg
x a : ℝ
hyp : 0.re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp
no goals
case neg
x a : ℝ
hyp : 0.re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
exact Or.inl ⟨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_rpow h
no goals
case mpr.inr.intro

⊢ 0 ^ 0 = 1
exact rpow_zero _