awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inr : ∀ (h₂ : LE.le (α := ℝ) 0 0), HPow.hPow (β := ℝ) x 0 ≤ HPow.hPow (β := ℝ) y 0
⊢ x ^ z ≤ y ^ z
have inr₁ : ∀ (h₂' : 0 < z), 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 (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
⊢ y ^ z < x ^ z
have this : 0 < y
Tactic: have := hx.trans hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ y ^ z < x ^ z
have rw : x ^ (-z) < y ^ (-z)
Tactic: rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
rw : x ^ (-z) < y ^ (-z)
⊢ y ^ z < x ^ z
have hx₁ : 0 ≤ y
Tactic: rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
rw : x ^ (-z) < y ^ (-z)
hx₁ : 0 ≤ y
⊢ y ^ z < x ^ z
have hx₂ : 0 ≤ x
Tactic: rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ y ^ z < x ^ z
have ha : 0 < x ^ z
Tactic: rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ y ^ z < x ^ z
have hb : 0 < y ^ z
Tactic: rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)
have refine : 0 ≤ x
Tactic: refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)
have on_goal : 0 ≤ x
Tactic: on_goal 1 => refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
⊢ y ^ z ≤ x ^ z
have this : 0 < y
Tactic: have := hx.trans_le hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ y ^ z ≤ x ^ z
have rw : x ^ (-z) ≤ y ^ (-z)
Tactic: rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
rw : x ^ (-z) ≤ y ^ (-z)
⊢ y ^ z ≤ x ^ z
have hx₁ : 0 ≤ y
Tactic: rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
rw : x ^ (-z) ≤ y ^ (-z)
hx₁ : 0 ≤ y
⊢ y ^ z ≤ x ^ z
have hx₂ : 0 ≤ x
Tactic: rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ y ^ z ≤ x ^ z
have ha : 0 < x ^ z
Tactic: rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ y ^ z ≤ x ^ z
have hb : 0 < y ^ z
Tactic: rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)
have refine : 0 ≤ x
Tactic: refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)
have on_goal : 0 ≤ x
Tactic: on_goal 1 => refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
h : y ≤ x
h₁ : 0 ≤ y
⊢ y ^ z ≤ x ^ z
have h₂ : 0 ≤ z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
hx₁ : 0 ≤ y
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have hy₁ : z ≠ 0
Tactic: rw [← rpow_le_rpow_iff hx _ hz, rpow_inv_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
hx₁ : 0 ≤ y
hy₁ : z ≠ 0
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have rw : 0 ≤ y ^ z⁻¹
Tactic: rw [← rpow_le_rpow_iff hx _ hz, rpow_inv_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
hx₁ : 0 ≤ x
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
have hy₁ : z ≠ 0
Tactic: rw [← rpow_le_rpow_iff _ hy hz, rpow_inv_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
hx₁ : 0 ≤ x
hy₁ : z ≠ 0
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
have rw : 0 ≤ x ^ z⁻¹
Tactic: rw [← rpow_le_rpow_iff _ hy hz, rpow_inv_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
have rw : 0 ≤ y
Tactic: rw [← rpow_le_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ y
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
have rw₁ : 0 < y ^ z⁻¹
Tactic: rw [← rpow_le_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z
have rw : 0 ≤ y
Tactic: rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ y
⊢ x < y ^ z⁻¹ ↔ y < x ^ z
have rw₁ : 0 < y ^ z⁻¹
Tactic: rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ < y ↔ y ^ z < x
have rw : 0 ≤ x
Tactic: rw [← rpow_lt_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ x
⊢ x ^ z⁻¹ < y ↔ y ^ z < x
have rw₁ : 0 < x ^ z⁻¹
Tactic: rw [← rpow_lt_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x
have rw : 0 ≤ x
Tactic: rw [← rpow_le_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
rw : 0 ≤ x
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x
have rw₁ : 0 < x ^ z⁻¹
Tactic: rw [← rpow_le_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z
have rw : rexp (log x * y) < x ^ z
Tactic: rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < x ^ z
have rw : rexp (log x * y) < rexp (log x * z)
Tactic: rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z
have repeat' : rexp (log x * y) < rexp (log x * z)
Tactic: repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ rexp (log x * y) < rexp (log x * z)
have rw : log x * y < log x * z
Tactic: rw [exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
have rw : rexp (log x * y) ≤ x ^ z
Tactic: rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ x ^ z
have rw : rexp (log x * y) ≤ rexp (log x * z)
Tactic: rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
have repeat' : rexp (log x * y) ≤ rexp (log x * z)
Tactic: repeat' rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)
have rw : log x * y ≤ log x * z
Tactic: rw [exp_le_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z
have ha : 0 ≤ log x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x y z : ℝ
hx : 1 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
have x_pos : 0 < x
Tactic: have x_pos : 0 < x := lt_trans zero_lt_one hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
have rw : log (x ^ y) ≤ log (x ^ z) ↔ y ≤ z
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
    log_rpow x_pos, mul_le_mul_iff_left₀ (log_pos hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
rw : log (x ^ y) ≤ log (x ^ z) ↔ y ≤ z
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
have rw₁ : y * log x ≤ log (x ^ z) ↔ y ≤ z
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
    log_rpow x_pos, mul_le_mul_iff_left₀ (log_pos hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
rw : log (x ^ y) ≤ log (x ^ z) ↔ y ≤ z
rw₁ : y * log x ≤ log (x ^ z) ↔ y ≤ z
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
have rw₂ : y * log x ≤ z * log x ↔ y ≤ z
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
    log_rpow x_pos, mul_le_mul_iff_left₀ (log_pos hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
rw : log (x ^ y) ≤ log (x ^ z) ↔ y ≤ z
rw₁ : y * log x ≤ log (x ^ z) ↔ y ≤ z
rw₂ : y * log x ≤ z * log x ↔ y ≤ z
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
have rw₃ : y ≤ z ↔ y ≤ z
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
    log_rpow x_pos, mul_le_mul_iff_left₀ (log_pos hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
⊢ x ^ y < x ^ z ↔ y < z
have rw : ¬x ^ z ≤ x ^ y ↔ y < z
Tactic: rw [lt_iff_not_ge, rpow_le_rpow_left_iff hx, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
rw : ¬x ^ z ≤ x ^ y ↔ y < z
⊢ x ^ y < x ^ z ↔ y < z
have rw₁ : ¬z ≤ y ↔ y < z
Tactic: rw [lt_iff_not_ge, rpow_le_rpow_left_iff hx, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 1 < x
rw : ¬x ^ z ≤ x ^ y ↔ y < z
rw₁ : ¬z ≤ y ↔ y < z
⊢ x ^ y < x ^ z ↔ y < z
have rw₂ : ¬z ≤ y ↔ ¬z ≤ y
Tactic: rw [lt_iff_not_ge, rpow_le_rpow_left_iff hx, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
have rw : rexp (log x * y) < x ^ z
Tactic: rw [rpow_def_of_pos hx0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < x ^ z
have rw : rexp (log x * y) < rexp (log x * z)
Tactic: rw [rpow_def_of_pos hx0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
have repeat' : rexp (log x * y) < rexp (log x * z)
Tactic: repeat' rw [rpow_def_of_pos hx0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)
have rw : log x * y < log x * z
Tactic: rw [exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
have rw : rexp (log x * y) ≤ x ^ z
Tactic: rw [rpow_def_of_pos hx0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ x ^ z
have rw : rexp (log x * y) ≤ rexp (log x * z)
Tactic: rw [rpow_def_of_pos hx0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
have repeat' : rexp (log x * y) ≤ rexp (log x * z)
Tactic: repeat' rw [rpow_def_of_pos hx0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)
have rw : log x * y ≤ log x * z
Tactic: rw [exp_le_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y ≤ x ^ z ↔ z ≤ y
have rw : log (x ^ y) ≤ log (x ^ z) ↔ z ≤ y
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
    mul_le_mul_right_of_neg (log_neg hx0 hx1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
rw : log (x ^ y) ≤ log (x ^ z) ↔ z ≤ y
⊢ x ^ y ≤ x ^ z ↔ z ≤ y
have rw₁ : y * log x ≤ log (x ^ z) ↔ z ≤ y
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
    mul_le_mul_right_of_neg (log_neg hx0 hx1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
rw : log (x ^ y) ≤ log (x ^ z) ↔ z ≤ y
rw₁ : y * log x ≤ log (x ^ z) ↔ z ≤ y
⊢ x ^ y ≤ x ^ z ↔ z ≤ y
have rw₂ : y * log x ≤ z * log x ↔ z ≤ y
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
    mul_le_mul_right_of_neg (log_neg hx0 hx1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
rw : log (x ^ y) ≤ log (x ^ z) ↔ z ≤ y
rw₁ : y * log x ≤ log (x ^ z) ↔ z ≤ y
rw₂ : y * log x ≤ z * log x ↔ z ≤ y
⊢ x ^ y ≤ x ^ z ↔ z ≤ y
have rw₃ : z ≤ y ↔ z ≤ y
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
    mul_le_mul_right_of_neg (log_neg hx0 hx1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y < x ^ z ↔ z < y
have rw : ¬x ^ z ≤ x ^ y ↔ z < y
Tactic: rw [lt_iff_not_ge, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
rw : ¬x ^ z ≤ x ^ y ↔ z < y
⊢ x ^ y < x ^ z ↔ z < y
have rw₁ : ¬y ≤ z ↔ z < y
Tactic: rw [lt_iff_not_ge, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
rw : ¬x ^ z ≤ x ^ y ↔ z < y
rw₁ : ¬y ≤ z ↔ z < y
⊢ x ^ y < x ^ z ↔ z < y
have rw₂ : ¬y ≤ z ↔ ¬y ≤ z
Tactic: rw [lt_iff_not_ge, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1
have rw : x ^ z < HPow.hPow (α := ℝ) 1 z
Tactic: rw [← one_rpow z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1
have rw : x ^ z ≤ HPow.hPow (α := ℝ) 1 z
Tactic: rw [← one_rpow z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1
have h : 1 = HPow.hPow (β := ℝ) x 0
Tactic: convert! rpow_lt_rpow_of_exponent_lt hx hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1
have h : 1 = HPow.hPow (β := ℝ) x 0
Tactic: convert! rpow_le_rpow_of_exponent_le hx hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z
have rw : HPow.hPow (α := ℝ) 1 z < x ^ z
Tactic: rw [← one_rpow z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ≤ x ^ z
have rw : HPow.hPow (α := ℝ) 1 z ≤ x ^ z
Tactic: rw [← one_rpow z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ HPow.hPow (α := ℝ) 1 z ≤ x ^ z
have h : LE.le (α := ℝ) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z
have h : 1 = HPow.hPow (β := ℝ) x 0
Tactic: convert! rpow_lt_rpow_of_exponent_gt hx1 hx2 hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 ≤ x ^ z
have h : 1 = HPow.hPow (β := ℝ) x 0
Tactic: convert! rpow_le_rpow_of_exponent_ge hx1 hx2 hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have rw : rexp (log x * y) < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Tactic: rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x * y) < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have rw₁ : log x * y < 0 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Tactic: rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x * y) < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rw₁ : log x * y < 0 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have rw₂ : 0 < log x ∧ y < 0 ∨ log x < 0 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Tactic: rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x * y) < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rw₁ : log x * y < 0 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rw₂ : 0 < log x ∧ y < 0 ∨ log x < 0 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have rw₃ : 1 < x ∧ y < 0 ∨ log x < 0 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Tactic: rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : rexp (log x * y) < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rw₁ : log x * y < 0 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rw₂ : 0 < log x ∧ y < 0 ∨ log x < 0 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rw₃ : 1 < x ∧ y < 0 ∨ log x < 0 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have rw₄ : 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Tactic: rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have inl : ∀ (hx : LE.le (α := ℝ) 0 0),
  HPow.hPow (α := ℝ) 0 y < 1 ↔ Eq (α := ℝ) 0 0 ∧ y ≠ 0 ∨ LT.lt (α := ℝ) 1 0 ∧ y < 0 ∨ LT.lt (α := ℝ) 0 1 ∧ 0 < y
Tactic: rcases hx.eq_or_lt with (rfl | hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
inl :
  ∀ (hx : LE.le (α := ℝ) 0 0),
    HPow.hPow (α := ℝ) 0 y < 1 ↔ Eq (α := ℝ) 0 0 ∧ y ≠ 0 ∨ LT.lt (α := ℝ) 1 0 ∧ y < 0 ∨ LT.lt (α := ℝ) 0 1 ∧ 0 < y
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
have inr : ∀ (hx : 0 < x), x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Tactic: rcases hx.eq_or_lt with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y : ℝ
hx : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) 0 y < 1 ↔ Eq (α := ℝ) 0 0 ∧ y ≠ 0 ∨ LT.lt (α := ℝ) 1 0 ∧ y < 0 ∨ LT.lt (α := ℝ) 0 1 ∧ 0 < y
have inl : HPow.hPow (α := ℝ) (β := ℝ) 0 0 < 1 ↔
  Eq (α := ℝ) 0 0 ∧ Ne (α := ℝ) 0 0 ∨ LT.lt (α := ℝ) 1 0 ∧ LT.lt (α := ℝ) 0 0 ∨ LT.lt (α := ℝ) 0 1 ∧ LT.lt (α := ℝ) 0 0
Tactic: rcases _root_.em (y = 0) with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y : ℝ
hx : LE.le (α := ℝ) 0 0
inl :
  HPow.hPow (α := ℝ) (β := ℝ) 0 0 < 1 ↔
    Eq (α := ℝ) 0 0 ∧ Ne (α := ℝ) 0 0 ∨
      LT.lt (α := ℝ) 1 0 ∧ LT.lt (α := ℝ) 0 0 ∨ LT.lt (α := ℝ) 0 1 ∧ LT.lt (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) 0 y < 1 ↔ Eq (α := ℝ) 0 0 ∧ y ≠ 0 ∨ LT.lt (α := ℝ) 1 0 ∧ y < 0 ∨ LT.lt (α := ℝ) 0 1 ∧ 0 < y
have inl₁ : ∀ (hy : ¬y = 0),
  HPow.hPow (α := ℝ) 0 y < 1 ↔ Eq (α := ℝ) 0 0 ∧ y ≠ 0 ∨ LT.lt (α := ℝ) 1 0 ∧ y < 0 ∨ LT.lt (α := ℝ) 0 1 ∧ 0 < y
Tactic: rcases _root_.em (y = 0) with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 < y
⊢ x ^ y < 1 ↔ x < 1
have rw : x ^ y < 1 ↔ x ^ y < HPow.hPow (α := ℝ) 1 y
Tactic: rw [← Real.rpow_lt_rpow_iff hx zero_le_one hy, Real.one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 < y
rw : x ^ y < 1 ↔ x ^ y < HPow.hPow (α := ℝ) 1 y
⊢ x ^ y < 1 ↔ x < 1
have rw₁ : x ^ y < 1 ↔ x ^ y < 1
Tactic: rw [← Real.rpow_lt_rpow_iff hx zero_le_one hy, Real.one_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
have rw : 1 < rexp (log x * y) ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
Tactic: rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : 1 < rexp (log x * y) ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
have rw₁ : 0 < log x * y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
Tactic: rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : 1 < rexp (log x * y) ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
rw₁ : 0 < log x * y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
have rw₂ : 0 < log x ∧ 0 < y ∨ log x < 0 ∧ y < 0 ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
Tactic: rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
hx : 0 < x
rw : 1 < rexp (log x * y) ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
rw₁ : 0 < log x * y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
rw₂ : 0 < log x ∧ 0 < y ∨ log x < 0 ∧ y < 0 ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
have rw₃ : 1 < x ∧ 0 < y ∨ log x < 0 ∧ y < 0 ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
Tactic: rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]