awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
rw : HPow.hPow (β := ℝ) x 1 / x ^ y = x / x ^ y
rw₁ rw₂ : x / x ^ y = x / x ^ y
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
rw [rpow_sub' hx h, rpow_one]

Premises used: Real.rpow_sub', Real.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ HPow.hPow (β := ℝ) x 2 = HPow.hPow (β := ℕ) x 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
rw : HPow.hPow (β := ℝ) x⁻¹ 1 = x⁻¹
rw₁ rw₂ : x⁻¹ = x⁻¹
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹

Tactic:
rw [rpow_neg_eq_inv_rpow, rpow_one]

Premises used: Real.rpow_one, Real.rpow_neg_eq_inv_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
hx₁ : 0 ≤ x * y
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
rw [Real.rpow_def_of_nonneg]

Premises used: Real.rpow_def_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
neg₁ : ∀ (h_ifs : ¬x * y = 0), rexp (log (x * y) * z) = 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

Tactic:
split_ifs with h_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h : z = 0
⊢ 1 = x ^ z * y ^ z

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h : ¬z = 0
⊢ 0 = x ^ z * y ^ z

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x * y = 0
⊢ ¬x = 0 ∧ ¬y = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
neg : rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z
neg₁ : 0 ≤ x
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z

Tactic:
rw [Real.rpow_def_of_nonneg]

Premises used: Real.rpow_def_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
neg₁ : ∀ (h_ifs : ¬x = 0), rexp (log (x * y) * z) = rexp (log x * z) * 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

Tactic:
split_ifs with h_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h : z = 0
⊢ rexp (log (x * y) * z) = 1 * y ^ z

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h : ¬z = 0
⊢ rexp (log (x * y) * z) = 0 * y ^ z

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬x = 0 ∧ ¬y = 0
h_ifs : ¬x = 0
⊢ ¬y = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs_1 : ¬x = 0 ∧ ¬y = 0
h_ifs : ¬x = 0
h_ifs₁ : ¬y = 0
⊢ ¬x = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
hx₁ : 0 ≤ x * y
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all

Premises used: Real.rpow_def_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
neg₃ neg₄ : rexp (log x * z) * rexp (log y * z) = rexp (log x * z) * rexp (log y * z)
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

Tactic:
rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]

Premises used: add_mul, Real.rpow_def_of_pos, Real.log_mul, Real.exp_add, LE.le.lt_of_ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
rw : x ^ (-y) = (x ^ y)⁻¹
rw₁ rw₂ : (x ^ y)⁻¹ = (x ^ y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rw [← rpow_neg_eq_inv_rpow, rpow_neg hx]

Premises used: Real.rpow_neg_eq_inv_rpow, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
z : ℝ
⊢ (x / y) ^ z = x ^ z / y ^ z

Tactic:
simp only [div_eq_mul_inv, mul_rpow hx (inv_nonneg.2 hy), inv_rpow hy]

Premises used: Iff.mpr, Real.inv_rpow, Real.mul_rpow, div_eq_mul_inv, inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y : ℝ
a : rexp (log (x ^ y)) = rexp (y * log x)
⊢ log (x ^ y) = y * log x

Tactic:
apply exp_injective

Premises used: Real.exp_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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)
a₃ a₄ : rexp (log (rexp (log x)) * y) = rexp (log (rexp (log x)) * y)
⊢ rexp (log (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]

Premises used: Real.rpow_pos_of_pos, Real.rpow_def_of_pos, Real.exp_log, Real.log, mul_comm, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
rw rw₁ : y * log x = y * log x
⊢ y * log x = log (x ^ y)

Tactic:
rw [log_rpow hx]

Premises used: Real.log_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
rw : x ^ (y * y⁻¹) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
rw₂ rw₃ : x = x
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
rw [← rpow_mul hx, mul_inv_cancel₀ hy, rpow_one]

Premises used: mul_inv_cancel₀, Real.rpow_one, Real.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
rw : x ^ (y⁻¹ * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
rw₂ rw₃ : x = x
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
rw [← rpow_mul hx, inv_mul_cancel₀ hy, rpow_one]

Premises used: Real.rpow_one, Real.rpow_mul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rw₃ rw₄ : x = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x

Tactic:
rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]

Premises used: mul_inv_cancel₀, Real.rpow_one, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rw₃ rw₄ : x = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x

Tactic:
rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]

Premises used: Real.rpow_one, Real.rpow_mul, inv_mul_cancel₀, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
rw₁ rw₂ : (x ^ n) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul hx, rpow_natCast]

Premises used: Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
rw₁ rw₂ : (x ^ y) ^ n = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n

Tactic:
rw [rpow_mul hx, rpow_natCast]

Premises used: Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
rw₁ rw₂ : (x ^ n) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul hx, rpow_intCast]

Premises used: Real.rpow_mul, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
rw₁ rw₂ : (x ^ y) ^ n = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n

Tactic:
rw [rpow_mul hx, rpow_intCast]

Premises used: Real.rpow_mul, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
⊢ 0 = x ∨ 0 < x

Tactic:
rw [le_iff_eq_or_lt] at hx

Premises used: le_iff_eq_or_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
hx₁ : 0 = x ∨ 0 < x
⊢ x < y

Tactic:
rw [le_iff_eq_or_lt] at hx

Premises used: le_iff_eq_or_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
hx₁ : 0 = x ∨ 0 < x
hxy₁ : x < y
⊢ 0 < z

Tactic:
rw [le_iff_eq_or_lt] at hx

Premises used: le_iff_eq_or_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
inl : ∀ (hx : 0 = x), x ^ z < y ^ z
inr : ∀ (hx : 0 < x), x ^ z < y ^ z
⊢ x ^ z < y ^ z

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
inl : 0 < y ^ z
⊢ x ^ z < y ^ z

Tactic:
rw [← hx, zero_rpow (ne_of_gt hz)]

Premises used: ne_of_gt, Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hxy : 0 < y) (hz : 0 < z) (hx : 0 = x), 0 < y
⊢ 0 < y

Tactic:
rwa [← hx] at hxy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z

Tactic:
exact rpow_pos_of_pos (by rwa [← hx] at hxy) _

Premises used: Real.rpow_pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
inr : log x * z < log y * z
⊢ x ^ z < y ^ z

Tactic:
rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]

Premises used: Real.rpow_def_of_pos, lt_trans, Real.exp_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z

Tactic:
mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

Premises used: Real.log_lt_log, mul_lt_mul_of_pos_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z

Tactic:
exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

Premises used: Real.log_lt_log, mul_lt_mul_of_pos_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
r : ℝ
hr : 0 < r
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r) (Set.Ici 0)

Tactic:
fun _ ha _ _ hab => rpow_lt_rpow ha hab hr

Premises used: Real.rpow_lt_rpow, StrictMonoOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
inl : ∀ (h₁ : x ≤ x), x ^ z ≤ x ^ z
inr : ∀ (h₁' : x < y), x ^ z ≤ y ^ z
⊢ x ^ z ≤ y ^ z

Tactic:
rcases eq_or_lt_of_le h₁ with (rfl | h₁')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
inr : ∀ (h₂ : LE.le (α := ℝ) 0 0), HPow.hPow (β := ℝ) x 0 ≤ HPow.hPow (β := ℝ) y 0
inr₁ : ∀ (h₂' : 0 < z), x ^ z ≤ y ^ z
⊢ x ^ z ≤ y ^ z

Tactic:
rcases eq_or_lt_of_le h₂ with (rfl | h₂')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (β := ℝ) x 0 ≤ HPow.hPow (β := ℝ) y 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z

Tactic:
le_of_lt (rpow_lt_rpow h h₁' h₂')

Premises used: le_of_lt, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z

Tactic:
exact le_of_lt (rpow_lt_rpow h h₁' h₂')

Premises used: le_of_lt, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
r : ℝ
hr : 0 ≤ r
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r) (Set.Ici 0)

Tactic:
fun _ ha _ _ hab => rpow_le_rpow ha hab hr

Premises used: MonotoneOn, Real.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
⊢ 0 < y

Tactic:
have := hx.trans hxy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
rw : x ^ (-z) < y ^ (-z)
hx₁ : 0 ≤ y
hx₂ : 0 ≤ x
ha : 0 < x ^ z
hb : 0 < y ^ z
⊢ y ^ z < x ^ z

Tactic:
rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]

Premises used: Real.rpow_neg, inv_lt_inv₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)

Tactic:
rpow_lt_rpow ?_ hxy (neg_pos.2 hz)

Premises used: Iff.mpr, neg_pos, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
refine : 0 ≤ x
⊢ x ^ (-z) < y ^ (-z)

Tactic:
refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)

Premises used: Iff.mpr, neg_pos, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
on_goal : 0 ≤ x
⊢ x ^ (-z) < y ^ (-z)

Tactic:
on_goal 1 => refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)

Premises used: Iff.mpr, neg_pos, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
⊢ 0 < y

Tactic:
have := hx.trans_le hxy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
rw : x ^ (-z) ≤ y ^ (-z)
hx₁ : 0 ≤ y
hx₂ : 0 ≤ x
ha : 0 < x ^ z
hb : 0 < y ^ z
⊢ y ^ z ≤ x ^ z

Tactic:
rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]

Premises used: Real.rpow_neg, inv_le_inv₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

Tactic:
rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Premises used: Iff.mpr, neg_nonneg, Real.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
refine : 0 ≤ x
⊢ x ^ (-z) ≤ y ^ (-z)

Tactic:
refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Premises used: Iff.mpr, neg_nonneg, Real.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
on_goal : 0 ≤ x
⊢ x ^ (-z) ≤ y ^ (-z)

Tactic:
on_goal 1 => refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Premises used: Iff.mpr, neg_nonneg, Real.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
h : y ≤ x
h₁ : 0 ≤ y
h₂ : 0 ≤ z
⊢ y ^ z ≤ x ^ z

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
h : x < y
hx₁ : 0 ≤ x
hz₁ : 0 < z
⊢ x ^ z < y ^ z

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ x ^ z ≤ y ^ z ↔ x ≤ y

Tactic:
le_iff_le_iff_lt_iff_lt.2 <| rpow_lt_rpow_iff hy hx hz

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Real.rpow_lt_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z < y ^ z ↔ y < x

Tactic:
⟨lt_imp_lt_of_le_imp_le fun h ↦ rpow_le_rpow_of_nonpos hx h hz.le,
    fun h ↦ rpow_lt_rpow_of_neg hy h hz⟩

Premises used: Real.rpow_lt_rpow_of_neg, Real.rpow_le_rpow_of_nonpos, LT.lt.le, Iff.intro, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z ≤ y ^ z ↔ y ≤ x

Tactic:
le_iff_le_iff_lt_iff_lt.2 <| rpow_lt_rpow_iff_of_neg hy hx hz

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Real.rpow_lt_rpow_iff_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
hx₁ : 0 ≤ y
hy₁ : z ≠ 0
rw : 0 ≤ y ^ z⁻¹
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [← rpow_le_rpow_iff hx _ hz, rpow_inv_rpow]

Premises used: Real.rpow_le_rpow_iff, Real.rpow_inv_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ z ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y ^ z⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
hx₁ : 0 ≤ x
hy₁ : z ≠ 0
rw : 0 ≤ x ^ z⁻¹
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
rw [← rpow_le_rpow_iff _ hy hz, rpow_inv_rpow]

Premises used: Real.rpow_le_rpow_iff, Real.rpow_inv_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x ^ z⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
lt_iff_lt_of_le_iff_le <| rpow_inv_le_iff_of_pos hy hx hz

Premises used: Real.rpow_inv_le_iff_of_pos, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ x ^ z⁻¹ < y ↔ x < y ^ z

Tactic:
lt_iff_lt_of_le_iff_le <| le_rpow_inv_iff_of_pos hy hx hz

Premises used: Real.le_rpow_inv_iff_of_pos, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ y
rw₁ : 0 < y ^ z⁻¹
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

Tactic:
rw [← rpow_le_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]

Premises used: Real.rpow_le_rpow_iff_of_neg, Real.rpow_inv_rpow, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ y
rw₁ : 0 < y ^ z⁻¹
⊢ x < y ^ z⁻¹ ↔ y < x ^ z

Tactic:
rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]

Premises used: Real.rpow_lt_rpow_iff_of_neg, Real.rpow_inv_rpow, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ x
rw₁ : 0 < x ^ z⁻¹
⊢ x ^ z⁻¹ < y ↔ y ^ z < x

Tactic:
rw [← rpow_lt_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]

Premises used: Real.rpow_lt_rpow_iff_of_neg, Real.rpow_inv_rpow, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ z⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ x
rw₁ : 0 < x ^ z⁻¹
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

Tactic:
rw [← rpow_le_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]

Premises used: Real.rpow_le_rpow_iff_of_neg, Real.rpow_inv_rpow, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
rw : rexp (log x * y) < x ^ z
⊢ x ^ y < x ^ z

Tactic:
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Premises used: Real.rpow_def_of_pos, lt_trans, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
rw : rexp (log x * y) < rexp (log x * z)
⊢ rexp (log x * y) < x ^ z

Tactic:
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Premises used: Real.rpow_def_of_pos, lt_trans, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
repeat' : rexp (log x * y) < rexp (log x * z)
⊢ x ^ y < x ^ z

Tactic:
repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]

Premises used: Real.rpow_def_of_pos, lt_trans, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
rw : log x * y < log x * z
⊢ rexp (log x * y) < rexp (log x * z)

Tactic:
rw [exp_lt_exp]

Premises used: Real.exp_lt_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z

Tactic:
mul_lt_mul_of_pos_left hyz (log_pos hx)

Premises used: mul_lt_mul_of_pos_left, Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z

Tactic:
exact mul_lt_mul_of_pos_left hyz (log_pos hx)

Premises used: mul_lt_mul_of_pos_left, Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
rw : rexp (log x * y) ≤ x ^ z
⊢ x ^ y ≤ x ^ z

Tactic:
rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]

Premises used: Real.rpow_def_of_pos, zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
rw : rexp (log x * y) ≤ rexp (log x * z)
⊢ rexp (log x * y) ≤ x ^ z

Tactic:
rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]

Premises used: Real.rpow_def_of_pos, zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
repeat' : rexp (log x * y) ≤ rexp (log x * z)
⊢ x ^ y ≤ x ^ z

Tactic:
repeat' rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]

Premises used: Real.rpow_def_of_pos, zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
rw : log x * y ≤ log x * z
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rw [exp_le_exp]

Premises used: Real.exp_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
ha : 0 ≤ log x
⊢ log x * y ≤ log x * z

Tactic:
gcongr