awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
⊢ c ^ (n + 1) ≤ a
have zero : ∀ (hc : 0 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H), HPow.hPow (α := ℕ) 0 (n + 1) ≤ a
Tactic: cases c with
  | zero => simp
  | succ k => simpa using Nat.find_min H hc.le
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
zero : ∀ (hc : 0 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H), HPow.hPow (α := ℕ) 0 (n + 1) ≤ a
⊢ c ^ (n + 1) ≤ a
have succ : ∀ (k : ℕ) (hc : k + 1 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H), (k + 1) ^ (n + 1) ≤ a
Tactic: cases c with
  | zero => simp
  | succ k => simpa using Nat.find_min H hc.le
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
have have : ∀ (c : ℕ) (hc1 : c ^ (n + 1) ≤ a) (hc2 : a < (c + 1) ^ (n + 1)), a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
Tactic: have ⟨c, hc1, hc2⟩ := nthRoot.always_exists n a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ (c + 1) ^ (n + 1) ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
have hab : c ≤ (c ^ (n + 1) / b ^ n + n * b) / (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
have calc : (c + 1) ^ (n + 1) ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
Tactic: calc a < (c + 1) ^ (n + 1) := hc2
    _ ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
      exact nthRoot.lt_pow_go_succ_aux0 hb
    _ ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
calc : (c + 1) ^ (n + 1) ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
have calc₁ : ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
Tactic: calc a < (c + 1) ^ (n + 1) := hc2
    _ ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
      exact nthRoot.lt_pow_go_succ_aux0 hb
    _ ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)
have split_ifs : ∀ (h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess),
  a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
split_ifs :
  ∀ (h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess),
    a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)
have split_ifs₁ : ∀ (h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess), a < (guess + 1) ^ (n + 2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
have inl : ∀ (hlt : a < HAdd.hAdd (α := ℕ) 0 1 ^ (n + 2)) (h : (a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2) < 0),
  a < (go n a fuel ((a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2)) + 1) ^ (n + 2)
Tactic: rcases eq_or_ne guess 0 with rfl | hguess
Cleared hypotheses: guess, hlt, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
inl :
  ∀ (hlt : a < HAdd.hAdd (α := ℕ) 0 1 ^ (n + 2)) (h : (a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2) < 0),
    a < (go n a fuel ((a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2)) + 1) ^ (n + 2)
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
have inr : ∀ (hguess : guess ≠ 0), a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
Tactic: rcases eq_or_ne guess 0 with rfl | hguess
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a guess fuel : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a < (go n a fuel guess + 1) ^ (n + 2)
have zero : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a 0 guess + 1) ^ (n + 2)
Tactic: induction fuel generalizing guess with
  | zero => simpa [go]
  | succ fuel ih =>
    rw [go]
    split_ifs with h
    case pos =>
      rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess
    case neg =>
      assumption
Cleared hypotheses: guess, fuel, hlt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a guess fuel : ℕ
hlt : a < (guess + 1) ^ (n + 2)
zero : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a 0 guess + 1) ^ (n + 2)
⊢ a < (go n a fuel guess + 1) ^ (n + 2)
have succ : ∀ (fuel : ℕ) (ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)) {guess : ℕ}
  (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a (fuel + 1) guess + 1) ^ (n + 2)
Tactic: induction fuel generalizing guess with
  | zero => simpa [go]
  | succ fuel ih =>
    rw [go]
    split_ifs with h
    case pos =>
      rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess
    case neg =>
      assumption
Cleared hypotheses: guess, fuel, hlt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n_1 : ℕ
hn_1 : n_1 ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
⊢ a < (nthRoot.go n a a a + 1) ^ (n + 2)
have hlt : a < (a + 1) ^ (n + 2)
Tactic: apply nthRoot.lt_pow_go_succ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b
have inl : a ^ n ≤ b
Tactic: simp only [hle, true_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
⊢ a ^ n ≤ b
have inl : a ^ n ≤ n.nthRoot b ^ n
Tactic: refine le_trans ?_ (pow_nthRoot_le (.inl hn))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b
have inr : b < a ^ n
Tactic: simp only [hlt.not_ge, false_iff, not_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ b < a ^ n
have inr : (n.nthRoot b + 1) ^ n ≤ a ^ n
Tactic: refine (lt_pow_nthRoot_add_one hn b).trans_le ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ (n.nthRoot b + 1) ^ n ≤ a ^ n
have inr : n.nthRoot b + 1 ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
Goal:
n a b : ℕ
hn : n ≠ 0
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b
have x : a ≤ n.nthRoot b ∨ n.nthRoot b < a
Tactic: cases le_or_gt a (nthRoot n b) with
  | inl hle =>
    simp only [hle, true_iff]
    refine le_trans ?_ (pow_nthRoot_le (.inl hn))
    gcongr
  | inr hlt =>
    simp only [hlt.not_ge, false_iff, not_le]
    refine (lt_pow_nthRoot_add_one hn b).trans_le ?_
    gcongr
    assumption
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.nthRoot (a ^ n) = a
have refine : ∀ (b : ℕ), b ≤ n.nthRoot (a ^ n) ↔ b ≤ a
Tactic: refine eq_of_forall_le_iff fun b ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ≤ n.nthRoot (a ^ n) ↔ b ≤ a
have rw : b ^ n ≤ a ^ n ↔ b ≤ a
Tactic: rw [le_nthRoot_iff hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
⊢ n.nthRoot b = a
have inl : ∀ (h₁ : HPow.hPow (β := ℕ) a 0 ≤ b) (h₂ : b < HPow.hPow (β := ℕ) (a + 1) 0), nthRoot 0 b = a
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
inl : ∀ (h₁ : HPow.hPow (β := ℕ) a 0 ≤ b) (h₂ : b < HPow.hPow (β := ℕ) (a + 1) 0), nthRoot 0 b = a
⊢ n.nthRoot b = a
have inr : ∀ (hn : n ≠ 0), n.nthRoot b = a
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
hn : n ≠ 0
⊢ n.nthRoot b = a
have h₃ : a ≤ n.nthRoot b
Tactic: simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
hn : n ≠ 0
h₃ : a ≤ n.nthRoot b
⊢ n.nthRoot b = a
have h₄ : n.nthRoot b < a + 1
Tactic: simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
hn : n ≠ 0
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n.nthRoot a ^ n = a
have mp : (∃ (x : ℕ), x ^ n = a) → n.nthRoot a ^ n = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
hn : n ≠ 0
mp : (∃ (x : ℕ), x ^ n = a) → n.nthRoot a ^ n = a
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n.nthRoot a ^ n = a
have mpr : n.nthRoot a ^ n = a → ∃ (x : ℕ), x ^ n = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
⊢ n.nthRoot (x ^ n) ^ n = x ^ n
have mp : x ^ n = x ^ n
Tactic: rw [nthRoot_pow hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a
have inl : (∃ (x : ℕ), HPow.hPow (β := ℕ) x 0 = a) ↔
  Eq (α := ℕ) 0 0 ∧ a = 1 ∨ Ne (α := ℕ) 0 0 ∧ HPow.hPow (β := ℕ) (nthRoot 0 a) 0 = a
Tactic: rcases eq_or_ne n 0 with rfl | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
inl :
  (∃ (x : ℕ), HPow.hPow (β := ℕ) x 0 = a) ↔
    Eq (α := ℕ) 0 0 ∧ a = 1 ∨ Ne (α := ℕ) 0 0 ∧ HPow.hPow (β := ℕ) (nthRoot 0 a) 0 = a
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a
have inr : n ≠ 0 → ((∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a)
Tactic: rcases eq_or_ne n 0 with rfl | _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg₂ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
neg₂ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 0 = 0
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg₃ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → ¬x = 0 → Complex.re 0 = rexp (log x * y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
neg₂ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 0 = 0
neg₃ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → ¬x = 0 → Complex.re 0 = rexp (log x * y)
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have pos₂ : ¬(↑x : ℂ) = 0 → x = 0 → y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
neg₂ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 0 = 0
neg₃ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → ¬x = 0 → Complex.re 0 = rexp (log x * y)
pos₂ : ¬(↑x : ℂ) = 0 → x = 0 → y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 1
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg₄ : ¬(↑x : ℂ) = 0 → x = 0 → ¬y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
neg₂ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 0 = 0
neg₃ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → ¬x = 0 → Complex.re 0 = rexp (log x * y)
pos₂ : ¬(↑x : ℂ) = 0 → x = 0 → y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 1
neg₄ : ¬(↑x : ℂ) = 0 → x = 0 → ¬y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 0
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg₅ : ¬(↑x : ℂ) = 0 → ¬x = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
⊢ x ^ y = rexp (log x * y)
have rw : (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = rexp (log x * y)
Tactic: rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
rw : (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = rexp (log x * y)
⊢ x ^ y = rexp (log x * y)
have rw₁ : rexp (log x * y) = rexp (log x * y)
Tactic: rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
⊢ rexp (x * y) = rexp x ^ y
have rw : rexp (x * y) = rexp (log (rexp x) * y)
Tactic: rw [rpow_def_of_pos (exp_pos _), log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
rw : rexp (x * y) = rexp (log (rexp x) * y)
⊢ rexp (x * y) = rexp x ^ y
have rw₁ : rexp (x * y) = rexp (x * y)
Tactic: rw [rpow_def_of_pos (exp_pos _), log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
⊢ HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℤ) x (-(↑n : ℤ))
have rw : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (↑(-(↑n : ℤ)) : ℝ)
Tactic: rw [← rpow_intCast, Int.cast_neg, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (↑(-(↑n : ℤ)) : ℝ)
⊢ HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℤ) x (-(↑n : ℤ))
have rw₁ : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (-(↑(↑n : ℤ) : ℝ))
Tactic: rw [← rpow_intCast, Int.cast_neg, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (↑(-(↑n : ℤ)) : ℝ)
rw₁ : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (-(↑(↑n : ℤ) : ℝ))
⊢ HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℤ) x (-(↑n : ℤ))
have rw₂ : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (-(↑n : ℝ))
Tactic: rw [← rpow_intCast, Int.cast_neg, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ rexp 1 ^ x = rexp x
have rw : rexp (1 * x) = rexp x
Tactic: rw [← exp_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
rw : rexp (1 * x) = rexp x
⊢ rexp 1 ^ x = rexp x
have rw₁ : rexp x = rexp x
Tactic: rw [← exp_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
⊢ rexp 1 ^ n = rexp (↑n : ℝ)
have rw : HPow.hPow (β := ℝ) (rexp 1) (↑n : ℝ) = rexp (↑n : ℝ)
Tactic: rw [← rpow_natCast, exp_one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
rw : HPow.hPow (β := ℝ) (rexp 1) (↑n : ℝ) = rexp (↑n : ℝ)
⊢ rexp 1 ^ n = rexp (↑n : ℝ)
have rw₁ : rexp (↑n : ℝ) = rexp (↑n : ℝ)
Tactic: rw [← rpow_natCast, exp_one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
have simp : (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
Tactic: simp only [rpow_def_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
have pos : x = 0 → y = 0 → (Eq (α := ℝ) 1 0 ↔ x = 0 ∧ y ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
pos : x = 0 → y = 0 → (Eq (α := ℝ) 1 0 ↔ x = 0 ∧ y ≠ 0)
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
have neg : x = 0 → ¬y = 0 → (Eq (α := ℝ) 0 0 ↔ x = 0 ∧ y ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
pos : x = 0 → y = 0 → (Eq (α := ℝ) 1 0 ↔ x = 0 ∧ y ≠ 0)
neg : x = 0 → ¬y = 0 → (Eq (α := ℝ) 0 0 ↔ x = 0 ∧ y ≠ 0)
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
have neg₁ : ¬x = 0 → (rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ x ^ y = rexp (log x * y) * cos (y * π)
have rw : (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y) * cos (y * π)
Tactic: rw [rpow_def, Complex.cpow_def, if_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
rw : (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y) * cos (y * π)
⊢ x ^ y = rexp (log x * y) * cos (y * π)
have hnc : ¬(↑x : ℂ) = 0
Tactic: rw [rpow_def, Complex.cpow_def, if_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I
have simp : ((↑(log x) : ℂ) + (↑π : ℂ) * Complex.I) * (↑y : ℂ) = (↑(log x) : ℂ) * (↑y : ℂ) + (↑y : ℂ) * (↑π : ℂ) * Complex.I
Tactic: simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
        Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y) * cos (y * π)
have this : Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I
Tactic: have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I := by
      simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
        Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]
      ring