awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I
⊢ (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y) * cos (y * π)
have rw : rexp (log x * y) * cos (y * π) + ((↑(rexp (log x * y) * sin (y * π)) : ℂ).re * 0 - 0 * Complex.I.im) =
  rexp (log x * y) * cos (y * π)
Tactic: rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
      Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
      Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im,
      Real.log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬(↑x : ℂ) = 0
have hnc : ¬x = 0
Tactic: rw [Complex.ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)
have pos : ∀ (h : x = 0), y = 0 → x ^ y = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
pos : ∀ (h : x = 0), y = 0 → x ^ y = 1
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)
have neg : ∀ (h : x = 0), ¬y = 0 → x ^ y = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
pos : ∀ (h : x = 0), y = 0 → x ^ y = 1
neg : ∀ (h : x = 0), ¬y = 0 → x ^ y = 0
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)
have neg₁ : ∀ (h : ¬x = 0), x ^ y = rexp (log x * y) * cos (y * π)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < x ^ y
have rw : 0 < rexp (log x * y)
Tactic: rw [rpow_def_of_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
α : Type u_1
f : α → ℝ
⊢ HPow.hPow (β := ℝ) f 0 = 1
have h : ∀ (x : α), HPow.hPow (β := ℝ) f 0 x = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
⊢ HPow.hPow (α := ℝ) 0 x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have mp : HPow.hPow (α := ℝ) 0 x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
mp : HPow.hPow (α := ℝ) 0 x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
⊢ HPow.hPow (α := ℝ) 0 x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have mpr : x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → HPow.hPow (α := ℝ) 0 x = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have pos : ∀ (h : x = 0), x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
pos : ∀ (h : x = 0), x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have neg : ∀ (h : ¬x = 0), x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have pos : ∀ (hyp : (HPow.hPow (α := ℂ) 0 (↑0 : ℂ)).re = a), Ne (α := ℝ) 0 0 ∧ a = 0 ∨ Eq (α := ℝ) 0 0 ∧ a = 1
Tactic: subst h
Cleared hypotheses: x, hyp, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑0 : ℂ)).re = a
⊢ Ne (α := ℝ) 0 0 ∧ a = 0 ∨ Eq (α := ℝ) 0 0 ∧ a = 1
have hyp₁ : 1 = a
Tactic: simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have hyp₁ : Complex.re 0 = a
Tactic: rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp
Cleared hypotheses: hyp, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
⊢ a = HPow.hPow (α := ℝ) 0 x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have rw : a = HPow.hPow (α := ℝ) 0 x ↔ HPow.hPow (α := ℝ) 0 x = a
Tactic: rw [← zero_rpow_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x a : ℝ
rw : a = HPow.hPow (α := ℝ) 0 x ↔ HPow.hPow (α := ℝ) 0 x = a
⊢ a = HPow.hPow (α := ℝ) 0 x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have rw₁ : HPow.hPow (α := ℝ) 0 x = a ↔ HPow.hPow (α := ℝ) 0 x = a
Tactic: rw [← zero_rpow_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
α : Type u_1
f : α → ℝ
⊢ HPow.hPow (β := ℝ) f 1 = f
have h : ∀ (x : α), HPow.hPow (β := ℝ) f 1 x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ HPow.hPow (α := ℝ) 0 x ≤ 1
have pos : ∀ (h : x = 0), HPow.hPow (α := ℝ) 0 x ≤ 1
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
pos : ∀ (h : x = 0), HPow.hPow (α := ℝ) 0 x ≤ 1
⊢ HPow.hPow (α := ℝ) 0 x ≤ 1
have neg : ∀ (h : ¬x = 0), HPow.hPow (α := ℝ) 0 x ≤ 1
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 x
have pos : ∀ (h : x = 0), 0 ≤ HPow.hPow (α := ℝ) 0 x
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
pos : ∀ (h : x = 0), 0 ≤ HPow.hPow (α := ℝ) 0 x
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 x
have neg : ∀ (h : ¬x = 0), 0 ≤ HPow.hPow (α := ℝ) 0 x
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ x ^ y
have rw : 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
Tactic: rw [rpow_def_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have pos : x = 0 → y = 0 → LE.le (α := ℝ) 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 → LE.le (α := ℝ) 0 1
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg : x = 0 → ¬y = 0 → LE.le (α := ℝ) 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 → LE.le (α := ℝ) 0 1
neg : x = 0 → ¬y = 0 → LE.le (α := ℝ) 0 0
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
have neg₁ : ¬x = 0 → 0 ≤ rexp (log x * y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y
have h_rpow_nonneg : 0 ≤ x ^ y
Tactic: have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg hx_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y
have rw : |x ^ y| = x ^ y
Tactic: rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
rw : |x ^ y| = x ^ y
⊢ |x ^ y| = |x| ^ y
have rw₁ : x ^ y = x ^ y
Tactic: rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
⊢ |x ^ y| ≤ |x| ^ y
have inl : ∀ (hx : 0 ≤ x), |x ^ y| ≤ |x| ^ y
Tactic: rcases le_or_gt 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
inl : ∀ (hx : 0 ≤ x), |x ^ y| ≤ |x| ^ y
⊢ |x ^ y| ≤ |x| ^ y
have inr : ∀ (hx : x < 0), |x ^ y| ≤ |x| ^ y
Tactic: rcases le_or_gt 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y
have inl : |x| ^ y ≤ |x| ^ y
Tactic: rw [abs_rpow_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y
have inr : rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)
Tactic: rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
      abs_of_pos (exp_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
⊢ |x ^ y| ≤ rexp (log x * y)
have refine : |x| ^ y ≤ rexp (log x * y)
Tactic: refine (abs_rpow_le_abs_rpow x y).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
⊢ |x| ^ y ≤ rexp (log x * y)
have pos : ∀ (hx : x = 0), |x| ^ y ≤ rexp (log x * y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
pos : ∀ (hx : x = 0), |x| ^ y ≤ rexp (log x * y)
⊢ |x| ^ y ≤ rexp (log x * y)
have neg : ∀ (hx : ¬x = 0), |x| ^ y ≤ rexp (log x * y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : x = 0
⊢ |x| ^ y ≤ rexp (log x * y)
have pos : ∀ (hy : y = 0), |x| ^ y ≤ rexp (log x * y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : x = 0
pos : ∀ (hy : y = 0), |x| ^ y ≤ rexp (log x * y)
⊢ |x| ^ y ≤ rexp (log x * y)
have neg : ∀ (hy : ¬y = 0), |x| ^ y ≤ rexp (log x * y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : ¬x = 0
⊢ |x| ^ y ≤ rexp (log x * y)
have neg : rexp (log |x| * y) ≤ rexp (log x * y)
Tactic: rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : ¬x = 0
neg : rexp (log |x| * y) ≤ rexp (log x * y)
⊢ |x| ^ y ≤ rexp (log x * y)
have neg₁ : rexp (log x * y) ≤ rexp (log x * y)
Tactic: rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ (log x)⁻¹ = rexp 1
have rw : log x ≠ 0
Tactic: rw [rpow_def_of_pos hx₀, mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ x ^ (log x)⁻¹ ≤ rexp 1
have calc : |x| ^ (log x)⁻¹ ≤ rexp 1
Tactic: calc
    _ ≤ |x ^ (log x)⁻¹| := le_abs_self _
    _ ≤ |x| ^ (log x)⁻¹ := abs_rpow_le_abs_rpow ..
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ |x| ^ (log x)⁻¹ ≤ rexp 1
have calc : |x| ^ (log |x|)⁻¹ ≤ rexp 1
Tactic: rw [← log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
have calc : ∀ (hx : |x| = 0), |x| ^ (log |x|)⁻¹ ≤ rexp 1
Tactic: obtain hx | hx := (abs_nonneg x).eq_or_lt'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
calc : ∀ (hx : |x| = 0), |x| ^ (log |x|)⁻¹ ≤ rexp 1
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
have calc₁ : ∀ (hx : 0 < |x|), |x| ^ (log |x|)⁻¹ ≤ rexp 1
Tactic: obtain hx | hx := (abs_nonneg x).eq_or_lt'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
have calc : rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1
Tactic: rw [rpow_def_of_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < |x|
⊢ rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1
have calc : log |x| * (log |x|)⁻¹ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), HPow.hPow (α := ℝ) 0 (y + z) = HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z
Tactic: rcases hx.eq_or_lt with (rfl | pos)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
inl : ∀ (hx : LE.le (α := ℝ) 0 0), HPow.hPow (α := ℝ) 0 (y + z) = HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr : ∀ (pos : 0 < x), x ^ (y + z) = x ^ y * x ^ z
Tactic: rcases hx.eq_or_lt with (rfl | pos)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y z : ℝ
h : y + z ≠ 0
hx : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) 0 (y + z) = HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z
have inl : HPow.hPow (α := ℝ) 0 y = 0 ∨ HPow.hPow (α := ℝ) 0 z = 0
Tactic: rw [zero_rpow h, zero_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
y z : ℝ
h : y + z ≠ 0
hx : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) 0 y = 0 ∨ HPow.hPow (α := ℝ) 0 z = 0
have this : y ≠ 0 ∨ z ≠ 0
Tactic: have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z
have rw : y + z ≠ 0
Tactic: rw [← h, rpow_add' hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inl : ∀ (hy : LE.le (α := ℝ) 0 0), x ^ (0 + z) = HPow.hPow (β := ℝ) x 0 * x ^ z
Tactic: rcases hy.eq_or_lt with (rfl | hy)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 ≤ z
inl : ∀ (hy : LE.le (α := ℝ) 0 0), x ^ (0 + z) = HPow.hPow (β := ℝ) x 0 * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z
have inr : ∀ (hy : 0 < y), x ^ (y + z) = x ^ y * x ^ z
Tactic: rcases hy.eq_or_lt with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : LE.le (α := ℝ) 0 0
⊢ x ^ (0 + z) = HPow.hPow (β := ℝ) x 0 * x ^ z
have inl : x ^ z = HPow.hPow (β := ℝ) x 0 * x ^ z
Tactic: rw [zero_add, rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : LE.le (α := ℝ) 0 0
inl : x ^ z = HPow.hPow (β := ℝ) x 0 * x ^ z
⊢ x ^ (0 + z) = HPow.hPow (β := ℝ) x 0 * x ^ z
have inl₁ : x ^ z = 1 * x ^ z
Tactic: rw [zero_add, rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : LE.le (α := ℝ) 0 0
inl : x ^ z = HPow.hPow (β := ℝ) x 0 * x ^ z
inl₁ : x ^ z = 1 * x ^ z
⊢ x ^ (0 + z) = HPow.hPow (β := ℝ) x 0 * x ^ z
have inl₂ : x ^ z = x ^ z
Tactic: rw [zero_add, rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
have inl : ∀ (H : 0 = x), x ^ y * x ^ z ≤ x ^ (y + z)
Tactic: rcases le_iff_eq_or_lt.1 hx with (H | pos)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
inl : ∀ (H : 0 = x), x ^ y * x ^ z ≤ x ^ (y + z)
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
have inr : ∀ (pos : 0 < x), x ^ y * x ^ z ≤ x ^ (y + z)
Tactic: rcases le_iff_eq_or_lt.1 hx with (H | pos)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
have pos : ∀ (h : y + z = 0), x ^ y * x ^ z ≤ x ^ (y + z)
Tactic: by_cases h : y + z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
pos : ∀ (h : y + z = 0), x ^ y * x ^ z ≤ x ^ (y + z)
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
have neg : ∀ (h : ¬y + z = 0), x ^ y * x ^ z ≤ x ^ (y + z)
Tactic: by_cases h : y + z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
have pos : HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ 1
Tactic: simp only [H.symm, h, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ HMul.hMul (α := ℝ) 1 1
have c0 : 0 ≤ HPow.hPow (α := ℝ) 0 z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
c0 : 0 ≤ HPow.hPow (α := ℝ) 0 z
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ HMul.hMul (α := ℝ) 1 1
have h₁ : HPow.hPow (α := ℝ) 0 y ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
c0 : 0 ≤ HPow.hPow (α := ℝ) 0 z
h₁ : HPow.hPow (α := ℝ) 0 y ≤ 1
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ HMul.hMul (α := ℝ) 1 1
have h₂ : HPow.hPow (α := ℝ) 0 z ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ 1
have y₁ : HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ HMul.hMul (α := ℝ) 1 1
Tactic: calc
        (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 := by
          gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]
        _ = 1 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
y₁ : HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ HMul.hMul (α := ℝ) 1 1
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ 1
have y₂ : HMul.hMul (α := ℝ) 1 1 = 1
Tactic: calc
        (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 := by
          gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]
        _ = 1 := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → 0 ≤ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ ∅, f x) = ∏ x ∈ ∅, a ^ f x
have empty : HPow.hPow (β := ℝ) a 0 = ∏ x ∈ ∅, a ^ f x
Tactic: rw [sum_empty, Finset.prod_empty, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → 0 ≤ f x
empty : HPow.hPow (β := ℝ) a 0 = ∏ x ∈ ∅, a ^ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ ∅, f x) = ∏ x ∈ ∅, a ^ f x
have empty₁ : HPow.hPow (β := ℝ) a 0 = 1
Tactic: rw [sum_empty, Finset.prod_empty, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → 0 ≤ f x
empty : HPow.hPow (β := ℝ) a 0 = ∏ x ∈ ∅, a ^ f x
empty₁ : HPow.hPow (β := ℝ) a 0 = 1
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ ∅, f x) = ∏ x ∈ ∅, a ^ f x
have empty₂ : Eq (α := ℝ) 1 1
Tactic: rw [sum_empty, Finset.prod_empty, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : ∀ (h : ∀ x ∈ s, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ cons i s hi, f x) = ∏ x ∈ cons i s hi, a ^ f x
have h₁ : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
Tactic: rw [forall_mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : ∀ (h : ∀ x ∈ s, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ cons i s hi, f x) = ∏ x ∈ cons i s hi, a ^ f x
have cons : a ^ (f i + ∑ x ∈ s, f x) = ∏ x ∈ cons i s hi, a ^ f x
Tactic: rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : ∀ (h : ∀ x ∈ s, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
cons : a ^ (f i + ∑ x ∈ s, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ Finset.cons i s hi, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
have cons₁ : a ^ (f i + ∑ x ∈ s, f x) = a ^ f i * ∏ x ∈ s, a ^ f x
Tactic: rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : ∀ (h : ∀ x ∈ s, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
cons : a ^ (f i + ∑ x ∈ s, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
cons₁ : a ^ (f i + ∑ x ∈ s, f x) = a ^ f i * ∏ x ∈ s, a ^ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ Finset.cons i s hi, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
have cons₂ : a ^ (f i + ∑ x ∈ s, f x) = a ^ f i * HPow.hPow (β := ℝ) a (∑ x ∈ s, f x)
Tactic: rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : ∀ (h : ∀ x ∈ s, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
cons : a ^ (f i + ∑ x ∈ s, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
cons₁ : a ^ (f i + ∑ x ∈ s, f x) = a ^ f i * ∏ x ∈ s, a ^ f x
cons₂ : a ^ (f i + ∑ x ∈ s, f x) = a ^ f i * HPow.hPow (β := ℝ) a (∑ x ∈ s, f x)
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ Finset.cons i s hi, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
have cons₃ : a ^ f i * HPow.hPow (β := ℝ) a (∑ i ∈ s, f i) = a ^ f i * HPow.hPow (β := ℝ) a (∑ x ∈ s, f x)
Tactic: rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ x ∈ s, 0 ≤ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
have empty : ∀ (h : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ ∅, f x) = ∏ x ∈ ∅, a ^ f x
Tactic: induction s using Finset.cons_induction with
  | empty => rw [sum_empty, Finset.prod_empty, rpow_zero]
  | cons i s hi ihs =>
    rw [forall_mem_cons] at h
    rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ x ∈ s, 0 ≤ f x
empty :
  ∀ (h : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → 0 ≤ f x),
    HPow.hPow (β := ℝ) a (∑ x ∈ ∅, f x) = ∏ x ∈ ∅, a ^ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x
have cons : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ihs : ∀ (h : ∀ x ∈ s, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x)
  (h : ∀ x ∈ cons i s hi, 0 ≤ f x), HPow.hPow (β := ℝ) a (∑ x ∈ cons i s hi, f x) = ∏ x ∈ cons i s hi, a ^ f x
Tactic: induction s using Finset.cons_induction with
  | empty => rw [sum_empty, Finset.prod_empty, rpow_zero]
  | cons i s hi ihs =>
    rw [forall_mem_cons] at h
    rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹
have simp : (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
  (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
Tactic: simp only [rpow_def_of_nonneg hx]
-- 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 rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
have pos : x = 0 → -y = 0 → y = 0 → Eq (α := ℝ) 1 1⁻¹
Tactic: split_ifs