awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
rw : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = x ^ y * x ^ n
rw₁ : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₂ : ((↑x : ℂ) ^ ((↑y : ℂ) + (↑(↑n : ℝ) : ℂ))).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₃ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑x : ℂ) ^ (↑(↑n : ℝ) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₄ : ((↑x : ℂ) ^ (↑y : ℂ) * HPow.hPow (β := ℂ) (↑x : ℂ) (↑n : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₅ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑x : ℂ) ^ n).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₆ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑(x ^ n) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₇ : ((↑(x ^ n) : ℂ) * (↑x : ℂ) ^ (↑y : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₈ : x ^ n * ((↑x : ℂ) ^ (↑y : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₉ : ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
Tactic: rw [rpow_def, rpow_def, Complex.ofReal_add,
    Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx), Complex.ofReal_intCast,
    Complex.cpow_intCast, ← Complex.ofReal_zpow, mul_comm, Complex.re_ofReal_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + (↑n : ℝ) ≠ 0
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw : x ^ y * HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y * x ^ n
Tactic: rw [rpow_add' hx h, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + (↑n : ℝ) ≠ 0
rw : x ^ y * HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₁ : x ^ y * x ^ n = x ^ y * x ^ n
Tactic: rw [rpow_add' hx h, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + (↑n : ℝ) ≠ 0
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw : x ^ y * HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y * x ^ n
Tactic: rw [rpow_add' hx h, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + (↑n : ℝ) ≠ 0
rw : x ^ y * HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₁ : x ^ y * x ^ n = x ^ y * x ^ n
Tactic: rw [rpow_add' hx h, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - (↑n : ℝ) ≠ 0
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have rw : x ^ y / HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y / x ^ n
Tactic: rw [rpow_sub' hx h, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - (↑n : ℝ) ≠ 0
rw : x ^ y / HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y / x ^ n
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have rw₁ : x ^ y / x ^ n = x ^ y / x ^ n
Tactic: rw [rpow_sub' hx h, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - (↑n : ℝ) ≠ 0
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have rw : x ^ y / HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y / x ^ n
Tactic: rw [rpow_sub' hx h, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - (↑n : ℝ) ≠ 0
rw : x ^ y / HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y / x ^ n
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n
have rw₁ : x ^ y / x ^ n = x ^ y / x ^ n
Tactic: rw [rpow_sub' hx h, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ (y + 1) = x ^ y * x
have rw : x ^ y * HPow.hPow (β := ℝ) x 1 = x ^ y * x
Tactic: rw [rpow_add' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
rw : x ^ y * HPow.hPow (β := ℝ) x 1 = x ^ y * x
⊢ x ^ (y + 1) = x ^ y * x
have rw₁ : x ^ y * x = x ^ y * x
Tactic: rw [rpow_add' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ (1 + y) = x * x ^ y
have rw : HPow.hPow (β := ℝ) x 1 * x ^ y = x * x ^ y
Tactic: rw [rpow_add' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
rw : HPow.hPow (β := ℝ) x 1 * x ^ y = x * x ^ y
⊢ x ^ (1 + y) = x * x ^ y
have rw₁ : x * x ^ y = x * x ^ y
Tactic: rw [rpow_add' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
⊢ x ^ (y - 1) = x ^ y / x
have rw : x ^ y / HPow.hPow (β := ℝ) x 1 = x ^ y / x
Tactic: rw [rpow_sub' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
rw : x ^ y / HPow.hPow (β := ℝ) x 1 = x ^ y / x
⊢ x ^ (y - 1) = x ^ y / x
have rw₁ : x ^ y / x = x ^ y / x
Tactic: rw [rpow_sub' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
⊢ x ^ (1 - y) = x / x ^ y
have rw : HPow.hPow (β := ℝ) x 1 / x ^ y = x / x ^ y
Tactic: rw [rpow_sub' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
rw : HPow.hPow (β := ℝ) x 1 / x ^ y = x / x ^ y
⊢ x ^ (1 - y) = x / x ^ y
have rw₁ : x / x ^ y = x / x ^ y
Tactic: rw [rpow_sub' hx h, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹
have rw : HPow.hPow (β := ℝ) x⁻¹ 1 = x⁻¹
Tactic: rw [rpow_neg_eq_inv_rpow, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
rw : HPow.hPow (β := ℝ) x⁻¹ 1 = x⁻¹
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹
have rw₁ : x⁻¹ = x⁻¹
Tactic: rw [rpow_neg_eq_inv_rpow, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z
have rw : (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z
Tactic: rw [Real.rpow_def_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
rw : (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z
⊢ (x * y) ^ z = x ^ z * y ^ z
have hx₁ : 0 ≤ x * y
Tactic: rw [Real.rpow_def_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z
have pos : ∀ (h_ifs : x * y = 0), z = 0 → 1 = x ^ z * y ^ z
Tactic: split_ifs with h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
pos : ∀ (h_ifs : x * y = 0), z = 0 → 1 = x ^ z * y ^ z
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z
have neg : ∀ (h_ifs : x * y = 0), ¬z = 0 → 0 = x ^ z * y ^ z
Tactic: split_ifs with h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
pos : ∀ (h_ifs : x * y = 0), z = 0 → 1 = x ^ z * y ^ z
neg : ∀ (h_ifs : x * y = 0), ¬z = 0 → 0 = x ^ z * y ^ z
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z
have neg₁ : ∀ (h_ifs : ¬x * y = 0), rexp (log (x * y) * z) = x ^ z * y ^ z
Tactic: split_ifs with h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x * y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z
have h_ifs₁ : ¬x = 0 ∧ ¬y = 0
Tactic: simp_all
Cleared hypotheses: h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z
have neg : rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z
Tactic: rw [Real.rpow_def_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z
have pos : ∀ (h_ifs : x = 0), z = 0 → rexp (log (x * y) * z) = 1 * y ^ z
Tactic: split_ifs with h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
pos : ∀ (h_ifs : x = 0), z = 0 → rexp (log (x * y) * z) = 1 * y ^ z
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z
have neg : ∀ (h_ifs : x = 0), ¬z = 0 → rexp (log (x * y) * z) = 0 * y ^ z
Tactic: split_ifs with h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
pos : ∀ (h_ifs : x = 0), z = 0 → rexp (log (x * y) * z) = 1 * y ^ z
neg : ∀ (h_ifs : x = 0), ¬z = 0 → rexp (log (x * y) * z) = 0 * y ^ z
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z
have neg₁ : ∀ (h_ifs : ¬x = 0), rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
Tactic: split_ifs with h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬x = 0 ∧ ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
have h_ifs₁ : ¬y = 0
Tactic: simp_all
Cleared hypotheses: h_ifs_1, h_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z
have neg : ∀ (h_ifs : ¬y = 0) (h_ifs : ¬x = 0), rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
Tactic: iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
neg : ∀ (h_ifs : ¬y = 0) (h_ifs : ¬x = 0), rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
⊢ (x * y) ^ z = x ^ z * y ^ z
have neg₁ : ∀ (h_ifs : ¬x = 0 ∧ ¬y = 0), 0 ≤ x
Tactic: iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
neg : ∀ (h_ifs : ¬y = 0) (h_ifs : ¬x = 0), rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
neg₁ : ∀ (h_ifs : ¬x = 0 ∧ ¬y = 0), 0 ≤ x
⊢ (x * y) ^ z = x ^ z * y ^ z
have hx₁ : 0 ≤ x * y
Tactic: iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
have neg : rexp ((log x + log y) * z) = rexp (log x * z) * y ^ z
Tactic: rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬y = 0
h_ifs : ¬x = 0
neg : rexp ((log x + log y) * z) = rexp (log x * z) * y ^ z
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
have neg₁ : rexp (log x * z + log y * z) = rexp (log x * z) * y ^ z
Tactic: rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬y = 0
h_ifs : ¬x = 0
neg : rexp ((log x + log y) * z) = rexp (log x * z) * y ^ z
neg₁ : rexp (log x * z + log y * z) = rexp (log x * z) * y ^ z
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
have neg₂ : rexp (log x * z) * rexp (log y * z) = rexp (log x * z) * y ^ z
Tactic: rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬y = 0
h_ifs : ¬x = 0
neg : rexp ((log x + log y) * z) = rexp (log x * z) * y ^ z
neg₁ : rexp (log x * z + log y * z) = rexp (log x * z) * y ^ z
neg₂ : rexp (log x * z) * rexp (log y * z) = rexp (log x * z) * y ^ z
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
have neg₃ : rexp (log x * z) * rexp (log y * z) = rexp (log x * z) * rexp (log y * z)
Tactic: rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have rw : x ^ (-y) = (x ^ y)⁻¹
Tactic: rw [← rpow_neg_eq_inv_rpow, rpow_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : x ^ (-y) = (x ^ y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
have rw₁ : (x ^ y)⁻¹ = (x ^ y)⁻¹
Tactic: rw [← rpow_neg_eq_inv_rpow, rpow_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
⊢ log (x ^ y) = y * log x
have a : rexp (log (x ^ y)) = rexp (y * log x)
Tactic: apply exp_injective
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
⊢ rexp (log (x ^ y)) = rexp (y * log x)
have a : x ^ y = rexp (y * log x)
Tactic: rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
a : x ^ y = rexp (y * log x)
⊢ rexp (log (x ^ y)) = rexp (y * log x)
have a₁ : rexp (log x) ^ y = rexp (y * log (rexp (log x)))
Tactic: rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
a : x ^ y = rexp (y * log x)
a₁ : rexp (log x) ^ y = rexp (y * log (rexp (log x)))
⊢ rexp (log (x ^ y)) = rexp (y * log x)
have a₂ : rexp (log x) ^ y = rexp (log (rexp (log x)) * y)
Tactic: rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
a : x ^ y = rexp (y * log x)
a₁ : rexp (log x) ^ y = rexp (y * log (rexp (log x)))
a₂ : rexp (log x) ^ y = rexp (log (rexp (log x)) * y)
⊢ rexp (log (x ^ y)) = rexp (y * log x)
have a₃ : rexp (log (rexp (log x)) * y) = rexp (log (rexp (log x)) * y)
Tactic: rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = log (x ^ y)
have rw : y * log x = y * log x
Tactic: rw [log_rpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ (x ^ y) ^ y⁻¹ = x
have rw : x ^ (y * y⁻¹) = x
Tactic: rw [← rpow_mul hx, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
rw : x ^ (y * y⁻¹) = x
⊢ (x ^ y) ^ y⁻¹ = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul hx, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
rw : x ^ (y * y⁻¹) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ y) ^ y⁻¹ = x
have rw₂ : x = x
Tactic: rw [← rpow_mul hx, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ (x ^ y⁻¹) ^ y = x
have rw : x ^ (y⁻¹ * y) = x
Tactic: rw [← rpow_mul hx, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
rw : x ^ (y⁻¹ * y) = x
⊢ (x ^ y⁻¹) ^ y = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul hx, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
rw : x ^ (y⁻¹ * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ y⁻¹) ^ y = x
have rw₂ : x = x
Tactic: rw [← rpow_mul hx, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have hn0 : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw₂ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
rw₂ : HPow.hPow (β := ℝ) x 1 = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw₃ : x = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have hn0 : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw₂ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
rw₂ : HPow.hPow (β := ℝ) x 1 = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw₃ : x = x
Tactic: rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul hx, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw₁ : (x ^ n) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul hx, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
Tactic: rw [rpow_mul hx, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [rpow_mul hx, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul hx, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z
have rw₁ : (x ^ n) ^ z = (x ^ n) ^ z
Tactic: rw [rpow_mul hx, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
Tactic: rw [rpow_mul hx, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [rpow_mul hx, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
have hx₁ : 0 = x ∨ 0 < x
Tactic: rw [le_iff_eq_or_lt] at hx
Cleared hypotheses: hx, hxy, hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
have inl : ∀ (hx : 0 = x), x ^ z < y ^ z
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
inl : ∀ (hx : 0 = x), x ^ z < y ^ z
⊢ x ^ z < y ^ z
have inr : ∀ (hx : 0 < x), x ^ z < y ^ z
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z
have inl : 0 < y ^ z
Tactic: rw [← hx, zero_rpow (ne_of_gt hz)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y
have rwa : ∀ (hxy : 0 < y) (hz : 0 < z) (hx : 0 = x), 0 < y
Tactic: rwa [← hx] at hxy
Cleared hypotheses: hxy, hz, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z
have inr : log x * z < log y * z
Tactic: rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
⊢ x ^ z ≤ y ^ z
have inl : ∀ (h₁ : x ≤ x), x ^ z ≤ x ^ z
Tactic: rcases eq_or_lt_of_le h₁ with (rfl | h₁')
Cleared hypotheses: y, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
inl : ∀ (h₁ : x ≤ x), x ^ z ≤ x ^ z
⊢ x ^ z ≤ y ^ z
have inr : ∀ (h₁' : x < y), x ^ z ≤ y ^ z
Tactic: rcases eq_or_lt_of_le h₁ with (rfl | h₁')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z
have inr : ∀ (h₂ : LE.le (α := ℝ) 0 0), HPow.hPow (β := ℝ) x 0 ≤ HPow.hPow (β := ℝ) y 0
Tactic: rcases eq_or_lt_of_le h₂ with (rfl | h₂')
Cleared hypotheses: z, h₂