awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
pos : ∀ (h : x = 0), 0 ≤ HPow.hPow (α := ℝ) 0 x
neg : ∀ (h : ¬x = 0), 0 ≤ HPow.hPow (α := ℝ) 0 x
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 x

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x = 0
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 x

Tactic:
simp [h, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : ¬x = 0
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 x

Tactic:
simp [h, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
⊢ 0 ≤ x ^ y

Tactic:
rw [rpow_def_of_nonneg hx]

Premises used: Real.rpow_def_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → y = 0 → LE.le (α := ℝ) 0 1
neg : x = 0 → ¬y = 0 → LE.le (α := ℝ) 0 0
neg₁ : ¬x = 0 → 0 ≤ rexp (log x * y)
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : y = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]

Premises used: le_refl, le_of_lt, zero_le_one, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : ¬y = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]

Premises used: le_refl, le_of_lt, zero_le_one, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : ¬x = 0
⊢ 0 ≤ rexp (log x * y)

Tactic:
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]

Premises used: le_refl, le_of_lt, zero_le_one, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ 0 ≤ x ^ y

Tactic:
have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg hx_nonneg _
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
rw : |x ^ y| = x ^ y
rw₁ rw₂ : x ^ y = x ^ y
⊢ |x ^ y| = |x| ^ y

Tactic:
rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]

Premises used: Iff.mpr, abs_eq_self
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
inl : ∀ (hx : 0 ≤ x), |x ^ y| ≤ |x| ^ y
inr : ∀ (hx : x < 0), |x ^ y| ≤ |x| ^ y
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rcases le_or_gt 0 x with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
inl inl₁ : |x| ^ y ≤ |x| ^ y
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rw [abs_rpow_of_nonneg hx]

Premises used: Real.abs_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : x < 0
inr : rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)
⊢ |x ^ y| ≤ |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 _)]

Premises used: Iff.mpr, Real.rpow_def_of_pos, Real.log_neg_eq_log, neg_pos, abs_of_neg, abs_mul, Real.rpow_def_of_neg, abs_of_pos, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : x < 0
⊢ rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)

Tactic:
mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

Premises used: Real.abs_cos_le_one, mul_le_of_le_one_right, LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : x < 0
⊢ rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)

Tactic:
exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

Premises used: Real.abs_cos_le_one, mul_le_of_le_one_right, LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
⊢ |x ^ y| ≤ rexp (log x * y)

Tactic:
(abs_rpow_le_abs_rpow x y).trans ?_

Premises used: Real.abs_rpow_le_abs_rpow, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
refine : |x| ^ y ≤ rexp (log x * y)
⊢ |x ^ y| ≤ rexp (log x * y)

Tactic:
refine (abs_rpow_le_abs_rpow x y).trans ?_

Premises used: Real.abs_rpow_le_abs_rpow, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
pos : ∀ (hx : x = 0), |x| ^ y ≤ rexp (log x * y)
neg : ∀ (hx : ¬x = 0), |x| ^ y ≤ rexp (log x * y)
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : x = 0
pos : ∀ (hy : y = 0), |x| ^ y ≤ rexp (log x * y)
neg : ∀ (hy : ¬y = 0), |x| ^ y ≤ rexp (log x * y)
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : x = 0
hy : y = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
simp [hx, hy, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : x = 0
hy : ¬y = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
simp [hx, hy, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : ¬x = 0
neg : rexp (log |x| * y) ≤ rexp (log x * y)
neg₁ neg₂ : rexp (log x * y) ≤ rexp (log x * y)
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]

Premises used: Iff.mpr, Real.log_abs, Real.rpow_def_of_pos, abs_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
rw : log x ≠ 0
⊢ x ^ (log x)⁻¹ = rexp 1

Tactic:
rw [rpow_def_of_pos hx₀, mul_inv_cancel₀]

Premises used: Real.rpow_def_of_pos, mul_inv_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ≠ -1

Tactic:
bound
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ log x ≠ 0

Tactic:
exact log_ne_zero.2 ⟨hx₀.ne', hx₁, by bound⟩

Premises used: Iff.mpr, LT.lt.ne', And.intro, Real.log_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ x ^ (log x)⁻¹ ≤ |x ^ (log x)⁻¹|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ |x ^ (log x)⁻¹| ≤ |x| ^ (log x)⁻¹

Tactic:
abs_rpow_le_abs_rpow ..

Premises used: Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
calc : |x| ^ (log x)⁻¹ ≤ rexp 1
⊢ x ^ (log x)⁻¹ ≤ rexp 1

Tactic:
calc
    _ ≤ |x ^ (log x)⁻¹| := le_abs_self _
    _ ≤ |x| ^ (log x)⁻¹ := abs_rpow_le_abs_rpow ..

Premises used: le_abs_self, Real.abs_rpow_le_abs_rpow, Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
calc : |x| ^ (log |x|)⁻¹ ≤ rexp 1
⊢ |x| ^ (log x)⁻¹ ≤ rexp 1

Tactic:
rw [← log_abs]

Premises used: Real.log_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
calc : ∀ (hx : |x| = 0), |x| ^ (log |x|)⁻¹ ≤ rexp 1
calc₁ : ∀ (hx : 0 < |x|), |x| ^ (log |x|)⁻¹ ≤ rexp 1
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
obtain hx | hx := (abs_nonneg x).eq_or_lt'

Premises used: LE.le.eq_or_lt', abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : |x| = 0
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < |x|
calc : rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
rw [rpow_def_of_pos hx]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < |x|
calc : log |x| * (log |x|)⁻¹ ≤ 1
⊢ rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < |x|
⊢ log |x| * (log |x|)⁻¹ ≤ 1

Tactic:
mul_inv_le_one

Premises used: mul_inv_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < |x|
⊢ log |x| * (log |x|)⁻¹ ≤ 1

Tactic:
exact mul_inv_le_one

Premises used: mul_inv_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y

Tactic:
abs_rpow_of_nonneg hx_nonneg

Premises used: Real.abs_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y

Tactic:
exact abs_rpow_of_nonneg hx_nonneg

Premises used: Real.abs_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
simp only [rpow_def_of_pos hx, mul_add, exp_add]

Premises used: Real.rpow_def_of_pos, mul_add, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inr : ∀ (pos : 0 < x), x ^ (y + z) = x ^ y * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rcases hx.eq_or_lt with (rfl | pos)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y z : ℝ
h : y + z ≠ 0
hx : LE.le (α := ℝ) 0 0
inl : HPow.hPow (α := ℝ) 0 y = 0 ∨ HPow.hPow (α := ℝ) 0 z = 0
⊢ HPow.hPow (α := ℝ) 0 (y + z) = HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z

Tactic:
rw [zero_rpow h, zero_eq_mul]

Premises used: zero_eq_mul, Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y z : ℝ
h : y + z ≠ 0
hx : LE.le (α := ℝ) 0 0
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y z : ℝ
h : y + z ≠ 0
hx : LE.le (α := ℝ) 0 0
this : y ≠ 0 ∨ z ≠ 0
⊢ HPow.hPow (α := ℝ) 0 y = 0 ∨ HPow.hPow (α := ℝ) 0 z = 0

Tactic:
this.imp zero_rpow zero_rpow

Premises used: Real.zero_rpow, Or.imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y z : ℝ
h : y + z ≠ 0
hx : LE.le (α := ℝ) 0 0
this : y ≠ 0 ∨ z ≠ 0
⊢ HPow.hPow (α := ℝ) 0 y = 0 ∨ HPow.hPow (α := ℝ) 0 z = 0

Tactic:
exact this.imp zero_rpow zero_rpow

Premises used: Real.zero_rpow, Or.imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rpow_add pos _ _

Premises used: Real.rpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
exact rpow_add pos _ _

Premises used: Real.rpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
rw : y + z ≠ 0
⊢ x ^ w = x ^ y * x ^ z

Tactic:
rw [← h, rpow_add' hx]

Premises used: Real.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
rwa rwa₁ rwa₂ rwa₃ : w ≠ 0
⊢ y + z ≠ 0

Tactic:
rwa [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inr : ∀ (hy : 0 < y), x ^ (y + z) = x ^ y * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rcases hy.eq_or_lt with (rfl | hy)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inl₂ inl₃ : x ^ z = x ^ z
⊢ x ^ (0 + z) = HPow.hPow (β := ℝ) x 0 * x ^ z

Tactic:
rw [zero_add, rpow_zero, one_mul]

Premises used: Real.rpow_zero, zero_add, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy_1 : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)

Premises used: ne_of_gt, Real.rpow_add', add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy_1 : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
exact rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)

Premises used: ne_of_gt, Real.rpow_add', add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
inl : ∀ (H : 0 = x), x ^ y * x ^ z ≤ x ^ (y + z)
inr : ∀ (pos : 0 < x), x ^ y * x ^ z ≤ x ^ (y + z)
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
rcases le_iff_eq_or_lt.1 hx with (H | pos)

Premises used: le_iff_eq_or_lt, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
pos : ∀ (h : y + z = 0), x ^ y * x ^ z ≤ x ^ (y + z)
neg : ∀ (h : ¬y + z = 0), x ^ y * x ^ z ≤ x ^ (y + z)
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
by_cases h : y + z = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
pos : HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ 1
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
simp only [H.symm, h, rpow_zero]

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
h₂ : HPow.hPow (α := ℝ) 0 z ≤ 1
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ HMul.hMul (α := ℝ) 1 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 z

Tactic:
zero_rpow_nonneg z

Premises used: Real.zero_rpow_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ HPow.hPow (α := ℝ) 0 y ≤ 1

Tactic:
zero_rpow_le_one y

Premises used: Real.zero_rpow_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ HPow.hPow (α := ℝ) 0 z ≤ 1

Tactic:
zero_rpow_le_one z

Premises used: Real.zero_rpow_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 z

Tactic:
exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]

Premises used: Real.zero_rpow_nonneg, Real.zero_rpow_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ HMul.hMul (α := ℝ) 1 1 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
y₂ : HMul.hMul (α := ℝ) 1 1 = 1
⊢ HPow.hPow (α := ℝ) 0 y * HPow.hPow (α := ℝ) 0 z ≤ 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

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
simp [rpow_add', ← H, h]

Premises used: Real.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
simp [rpow_add pos]

Premises used: Real.rpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
ι : Type u_1
a : ℝ
ha : 0 < a
f : ι → ℝ
s : Finset ι
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x

Tactic:
map_sum (⟨⟨fun (x : ℝ) => (a ^ x : ℝ), rpow_zero a⟩, rpow_add ha⟩ : ℝ →+ (Additive ℝ)) f s

Premises used: Additive, Multiset.prod, Real.rpow_zero, AddMonoidHom.mk, map_sum, ZeroHom.mk, Finset.prod, HPow.hPow, Real.rpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
empty₂ empty₃ : Eq (α := ℝ) 1 1
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ ∅, f x) = ∏ x ∈ ∅, a ^ f x

Tactic:
rw [sum_empty, Finset.prod_empty, rpow_zero]

Premises used: Finset.prod_empty, Real.rpow_zero, Finset.sum_empty
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
⊢ 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x

Tactic:
rw [forall_mem_cons] at h

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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)
cons₃ cons₄ : a ^ f i * HPow.hPow (β := ℝ) a (∑ i ∈ s, f i) = 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

Tactic:
rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]

Premises used: Real.rpow_add_of_nonneg, Finset.sum_cons, Finset.sum_nonneg, And.right, And.left, Finset.prod_cons
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
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 ∈ Finset.cons i s hi, 0 ≤ f x),
    HPow.hPow (β := ℝ) a (∑ x ∈ Finset.cons i s hi, f x) = ∏ x ∈ Finset.cons i s hi, a ^ f x
⊢ HPow.hPow (β := ℝ) a (∑ x ∈ s, f x) = ∏ x ∈ s, 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)]

Premises used: Finset.prod_empty, Finset.sum_cons, Finset.cons, Real.rpow_zero, Finset.forall_mem_cons, Finset.prod_cons, Finset.sum_empty
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
⊢ x ^ (-y) = x⁻¹ ^ y

Tactic:
simp [rpow_def, Complex.cpow_neg, Complex.inv_cpow_eq_ite, apply_ite]

Premises used: apply_ite, Complex.cpow_neg, Complex.inv_cpow_eq_ite, Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
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))⁻¹
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
simp only [rpow_def_of_nonneg hx]

Premises used: Real.rpow_def_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → -y = 0 → y = 0 → Eq (α := ℝ) 1 1⁻¹
neg : x = 0 → -y = 0 → ¬y = 0 → Eq (α := ℝ) 1 0⁻¹
pos₁ : x = 0 → ¬-y = 0 → y = 0 → Eq (α := ℝ) 0 1⁻¹
neg₁ : x = 0 → ¬-y = 0 → ¬y = 0 → Eq (α := ℝ) 0 0⁻¹
neg₂ : ¬x = 0 → rexp (log x * -y) = (rexp (log 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))⁻¹

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : -y = 0
h_2 : y = 0
⊢ Eq (α := ℝ) 1 1⁻¹

Tactic:
simp_all [exp_neg]

Premises used: Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : -y = 0
h_2 : ¬y = 0
⊢ Eq (α := ℝ) 1 0⁻¹

Tactic:
simp_all [exp_neg]

Premises used: Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : ¬-y = 0
h_2 : y = 0
⊢ Eq (α := ℝ) 0 1⁻¹

Tactic:
simp_all [exp_neg]

Premises used: Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : ¬-y = 0
h_2 : ¬y = 0
⊢ Eq (α := ℝ) 0 0⁻¹

Tactic:
simp_all [exp_neg]

Premises used: Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : ¬x = 0
⊢ rexp (log x * -y) = (rexp (log x * y))⁻¹

Tactic:
simp_all [exp_neg]

Premises used: Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
simp only [sub_eq_add_neg, rpow_add hx, rpow_neg (le_of_lt hx), div_eq_mul_inv]

Premises used: sub_eq_add_neg, le_of_lt, div_eq_mul_inv, Real.rpow_add, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y - z ≠ 0
⊢ y + -z ≠ 0

Tactic:
simp only [sub_eq_add_neg] at h ⊢

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y + -z ≠ 0
⊢ x ^ (y + -z) = x ^ y / x ^ z

Tactic:
simp only [rpow_add' hx h, rpow_neg hx, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Real.rpow_add', Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
hf : HasCompactSupport f
r : ℝ
hr : r ≠ 0
⊢ HasCompactSupport (β := ℝ) fun (x : α) ↦ f x ^ r

Tactic:
hf.comp_left (g := (· ^ r)) (Real.zero_rpow hr)

Premises used: Real.zero_rpow, HasCompactSupport.comp_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
simp :
  (↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) : ℂ) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log (↑x : ℂ) * (↑y : ℂ))
⊢ (↑(x ^ y) : ℂ) = (↑x : ℂ) ^ (↑y : ℂ)

Tactic:
simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]

Premises used: Complex.ofReal_eq_zero, Real.rpow_def_of_nonneg, Complex.cpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → y = 0 → (↑1 : ℂ) = 1
neg : x = 0 → ¬y = 0 → (↑0 : ℂ) = 0
neg₁ : ¬x = 0 → (↑(rexp (Real.log x * y)) : ℂ) = cexp (log (↑x : ℂ) * (↑y : ℂ))
⊢ (↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) : ℂ) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log (↑x : ℂ) * (↑y : ℂ))

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : y = 0
⊢ (↑1 : ℂ) = 1

Tactic:
simp [Complex.ofReal_log hx]

Premises used: Complex.ofReal_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : x = 0
h_1 : ¬y = 0
⊢ (↑0 : ℂ) = 0

Tactic:
simp [Complex.ofReal_log hx]

Premises used: Complex.ofReal_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : ¬x = 0
⊢ (↑(rexp (Real.log x * y)) : ℂ) = cexp (log (↑x : ℂ) * (↑y : ℂ))

Tactic:
simp [Complex.ofReal_log hx]

Premises used: Complex.ofReal_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
inl : ∀ (hx : LE.le (α := ℝ) 0 0), (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
inr : ∀ (hlt : x < 0), (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)

Tactic:
rcases hx.eq_or_lt with (rfl | hlt)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y : ℂ
hx : LE.le (α := ℝ) 0 0
inl : HPow.hPow (β := ℂ) (↑0 : ℂ) 0 = HPow.hPow (β := ℂ) (-(↑0 : ℂ)) 0 * cexp ((↑π : ℂ) * I * 0)
inl₁ : ∀ (hy : y ≠ 0), (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
⊢ (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (β := ℂ) (↑0 : ℂ) 0 = HPow.hPow (β := ℂ) (-(↑0 : ℂ)) 0 * cexp ((↑π : ℂ) * I * 0)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y : ℂ
hx : LE.le (α := ℝ) 0 0
hy : y ≠ 0
⊢ (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ (↑x : ℂ) ≠ 0

Tactic:
have hne : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr hlt.ne