awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₃ : 1 < 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 ∨ x < 1 ∧ 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
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
have inl : ∀ (hx : LE.le (α := ℝ) 0 0),
  1 < HPow.hPow (α := ℝ) 0 y ↔ LT.lt (α := ℝ) 1 0 ∧ 0 < y ∨ LT.lt (α := ℝ) 0 0 ∧ LT.lt (α := ℝ) 0 1 ∧ y < 0
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),
    1 < HPow.hPow (α := ℝ) 0 y ↔ LT.lt (α := ℝ) 1 0 ∧ 0 < y ∨ LT.lt (α := ℝ) 0 0 ∧ LT.lt (α := ℝ) 0 1 ∧ y < 0
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
have inr : ∀ (hx : 0 < x), 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
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
⊢ 1 < HPow.hPow (α := ℝ) 0 y ↔ LT.lt (α := ℝ) 1 0 ∧ 0 < y ∨ LT.lt (α := ℝ) 0 0 ∧ LT.lt (α := ℝ) 0 1 ∧ y < 0
have inl : 1 < HPow.hPow (α := ℝ) (β := ℝ) 0 0 ↔
  LT.lt (α := ℝ) 1 0 ∧ LT.lt (α := ℝ) 0 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 :
  1 < HPow.hPow (α := ℝ) (β := ℝ) 0 0 ↔
    LT.lt (α := ℝ) 1 0 ∧ LT.lt (α := ℝ) 0 0 ∨ LT.lt (α := ℝ) 0 0 ∧ LT.lt (α := ℝ) 0 1 ∧ LT.lt (α := ℝ) 0 0
⊢ 1 < HPow.hPow (α := ℝ) 0 y ↔ LT.lt (α := ℝ) 1 0 ∧ 0 < y ∨ LT.lt (α := ℝ) 0 0 ∧ LT.lt (α := ℝ) 0 1 ∧ y < 0
have inl₁ : ∀ (hy : ¬y = 0),
  1 < HPow.hPow (α := ℝ) 0 y ↔ LT.lt (α := ℝ) 1 0 ∧ 0 < y ∨ LT.lt (α := ℝ) 0 0 ∧ LT.lt (α := ℝ) 0 1 ∧ y < 0
Tactic: rcases _root_.em (y = 0) with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
⊢ x ^ y ≤ x ^ z
have inl : ∀ (hx0 : LE.le (α := ℝ) 0 0) (hx1 : LE.le (α := ℝ) 0 1) (h : Eq (α := ℝ) 0 0 → y = 0 → z = 0),
  HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
Tactic: rcases eq_or_lt_of_le hx0 with (rfl | hx0')
Cleared hypotheses: x, hx0, hx1, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
inl :
  ∀ (hx0 : LE.le (α := ℝ) 0 0) (hx1 : LE.le (α := ℝ) 0 1) (h : Eq (α := ℝ) 0 0 → y = 0 → z = 0),
    HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
⊢ x ^ y ≤ x ^ z
have inr : ∀ (hx0' : 0 < x), x ^ y ≤ x ^ z
Tactic: rcases eq_or_lt_of_le hx0 with (rfl | hx0')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y z : ℝ
hyz : z ≤ y
hx0 : LE.le (α := ℝ) 0 0
hx1 : LE.le (α := ℝ) 0 1
h : Eq (α := ℝ) 0 0 → y = 0 → z = 0
⊢ HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
have inl : ∀ (hyz : z ≤ 0) (h : Eq (α := ℝ) 0 0 → Eq (α := ℝ) 0 0 → z = 0),
  HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (α := ℝ) 0 z
Tactic: rcases eq_or_ne y 0 with rfl | hy0
Cleared hypotheses: y, hyz, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y z : ℝ
hyz : z ≤ y
hx0 : LE.le (α := ℝ) 0 0
hx1 : LE.le (α := ℝ) 0 1
h : Eq (α := ℝ) 0 0 → y = 0 → z = 0
inl :
  ∀ (hyz : z ≤ 0) (h : Eq (α := ℝ) 0 0 → Eq (α := ℝ) 0 0 → z = 0),
    HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (α := ℝ) 0 z
⊢ HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
have inl₁ : ∀ (hy0 : y ≠ 0), HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
Tactic: rcases eq_or_ne y 0 with rfl | hy0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z : ℝ
hx0 : LE.le (α := ℝ) 0 0
hx1 : LE.le (α := ℝ) 0 1
hyz : z ≤ 0
h : Eq (α := ℝ) 0 0 → Eq (α := ℝ) 0 0 → z = 0
⊢ HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (α := ℝ) 0 z
have inl : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (α := ℝ) (β := ℝ) 0 0
Tactic: rw [h rfl rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y z : ℝ
hyz : z ≤ y
hx0 : LE.le (α := ℝ) 0 0
hx1 : LE.le (α := ℝ) 0 1
h : Eq (α := ℝ) 0 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
have inl : 0 ≤ HPow.hPow (α := ℝ) 0 z
Tactic: rw [zero_rpow hy0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inl : ∀ (hxy : x ≤ y), max x y ^ p = max (x ^ p) (y ^ p)
Tactic: rcases le_total x y with hxy | hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
inl : ∀ (hxy : x ≤ y), max x y ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inr : ∀ (hxy : y ≤ x), max x y ^ p = max (x ^ p) (y ^ p)
Tactic: rcases le_total x y with hxy | hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inl : y ^ p = max (x ^ p) (y ^ p)
Tactic: rw [max_eq_right hxy, max_eq_right (by gcongr)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
inl : y ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inl₁ : y ^ p = y ^ p
Tactic: rw [max_eq_right hxy, max_eq_right (by gcongr)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inr : x ^ p = max (x ^ p) (y ^ p)
Tactic: rw [max_eq_left hxy, max_eq_left (by gcongr)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
inr : x ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)
have inr₁ : x ^ p = x ^ p
Tactic: rw [max_eq_left hxy, max_eq_left (by gcongr)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} y
z : ℝ
hz : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} z
hyz : y ^ x = z ^ x
⊢ y = z
have rw : HPow.hPow (β := ℝ) y 1 = z
Tactic: rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} y
z : ℝ
hz : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} z
hyz : y ^ x = z ^ x
rw : HPow.hPow (β := ℝ) y 1 = z
⊢ y = z
have rw₁ : HPow.hPow (β := ℝ) y 1 = HPow.hPow (β := ℝ) z 1
Tactic: rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} y
z : ℝ
hz : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} z
hyz : y ^ x = z ^ x
rw : HPow.hPow (β := ℝ) y 1 = z
rw₁ : HPow.hPow (β := ℝ) y 1 = HPow.hPow (β := ℝ) z 1
⊢ y = z
have rw₂ : y ^ (x * x⁻¹) = z ^ (x * x⁻¹)
Tactic: rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} y
z : ℝ
hz : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} z
hyz : y ^ x = z ^ x
rw : HPow.hPow (β := ℝ) y 1 = z
rw₁ : HPow.hPow (β := ℝ) y 1 = HPow.hPow (β := ℝ) z 1
rw₂ : y ^ (x * x⁻¹) = z ^ (x * x⁻¹)
⊢ y = z
have rw₃ : (y ^ x) ^ x⁻¹ = z ^ (x * x⁻¹)
Tactic: rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} y
z : ℝ
hz : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} z
hyz : y ^ x = z ^ x
rw : HPow.hPow (β := ℝ) y 1 = z
rw₁ : HPow.hPow (β := ℝ) y 1 = HPow.hPow (β := ℝ) z 1
rw₂ : y ^ (x * x⁻¹) = z ^ (x * x⁻¹)
rw₃ : (y ^ x) ^ x⁻¹ = z ^ (x * x⁻¹)
⊢ y = z
have rw₄ : (y ^ x) ^ x⁻¹ = (z ^ x) ^ x⁻¹
Tactic: rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} y
z : ℝ
hz : Membership.mem (γ := Set ℝ) {y : ℝ | 0 ≤ y} z
hyz : y ^ x = z ^ x
rw : HPow.hPow (β := ℝ) y 1 = z
rw₁ : HPow.hPow (β := ℝ) y 1 = HPow.hPow (β := ℝ) z 1
rw₂ : y ^ (x * x⁻¹) = z ^ (x * x⁻¹)
rw₃ : (y ^ x) ^ x⁻¹ = z ^ (x * x⁻¹)
rw₄ : (y ^ x) ^ x⁻¹ = (z ^ x) ^ x⁻¹
⊢ y = z
have rw₅ : (z ^ x) ^ x⁻¹ = (z ^ x) ^ x⁻¹
Tactic: rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]
-- 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 ↔ x = y ^ z
have rw : 0 ≤ x ^ z⁻¹
Tactic: rw [← rpow_left_inj _ hy hz, rpow_inv_rpow hx hz]
-- 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⁻¹ ↔ x ^ z = y
have rw : 0 ≤ y ^ z⁻¹
Tactic: rw [← rpow_left_inj hx _ hz, rpow_inv_rpow hy hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ≤ y ^ z ↔ log x ≤ z * log y
have rw : log x ≤ log (y ^ z) ↔ log x ≤ z * log y
Tactic: rw [← log_le_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log x ≤ log (y ^ z) ↔ log x ≤ z * log y
⊢ x ≤ y ^ z ↔ log x ≤ z * log y
have rw₁ : log x ≤ z * log y ↔ log x ≤ z * log y
Tactic: rw [← log_le_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
⊢ x ≤ y ^ z
have inl : ∀ (hx : x ≤ 0), x ≤ y ^ z
Tactic: obtain hx | hx := le_or_gt x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
inl : ∀ (hx : x ≤ 0), x ≤ y ^ z
⊢ x ≤ y ^ z
have inr : ∀ (hx : 0 < x), x ≤ y ^ z
Tactic: obtain hx | hx := le_or_gt x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ z ↔ log x < z * log y
have rw : log x < log (y ^ z) ↔ log x < z * log y
Tactic: rw [← log_lt_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log x < log (y ^ z) ↔ log x < z * log y
⊢ x < y ^ z ↔ log x < z * log y
have rw₁ : log x < z * log y ↔ log x < z * log y
Tactic: rw [← log_lt_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
⊢ x < y ^ z
have inl : ∀ (hx : x ≤ 0), x < y ^ z
Tactic: obtain hx | hx := le_or_gt x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
inl : ∀ (hx : x ≤ 0), x < y ^ z
⊢ x < y ^ z
have inr : ∀ (hx : 0 < x), x < y ^ z
Tactic: obtain hx | hx := le_or_gt x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ^ z ≤ y ↔ z * log x ≤ log y
have rw : log (x ^ z) ≤ log y ↔ z * log x ≤ log y
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log (x ^ z) ≤ log y ↔ z * log x ≤ log y
⊢ x ^ z ≤ y ↔ z * log x ≤ log y
have rw₁ : z * log x ≤ log y ↔ z * log x ≤ log y
Tactic: rw [← log_le_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ (↑n : ℝ) * log x ≤ log y
have rw : x ^ n ≤ y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) ≤ y
Tactic: rw [← rpow_le_iff_le_log hx hy, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
rw : x ^ n ≤ y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) ≤ y
⊢ x ^ n ≤ y ↔ (↑n : ℝ) * log x ≤ log y
have rw₁ : x ^ n ≤ y ↔ x ^ n ≤ y
Tactic: rw [← rpow_le_iff_le_log hx hy, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ (↑n : ℝ) * log x ≤ log y
have rw : x ^ n ≤ y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) ≤ y
Tactic: rw [← rpow_le_iff_le_log hx hy, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
rw : x ^ n ≤ y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) ≤ y
⊢ x ^ n ≤ y ↔ (↑n : ℝ) * log x ≤ log y
have rw₁ : x ^ n ≤ y ↔ x ^ n ≤ y
Tactic: rw [← rpow_le_iff_le_log hx hy, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ^ z < y ↔ z * log x < log y
have rw : log (x ^ z) < log y ↔ z * log x < log y
Tactic: rw [← log_lt_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log (x ^ z) < log y ↔ z * log x < log y
⊢ x ^ z < y ↔ z * log x < log y
have rw₁ : z * log x < log y ↔ z * log x < log y
Tactic: rw [← log_lt_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ (↑n : ℝ) * log x < log y
have rw : x ^ n < y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) < y
Tactic: rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
rw : x ^ n < y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) < y
⊢ x ^ n < y ↔ (↑n : ℝ) * log x < log y
have rw₁ : x ^ n < y ↔ x ^ n < y
Tactic: rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ (↑n : ℝ) * log x < log y
have rw : x ^ n < y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) < y
Tactic: rw [← rpow_lt_iff_lt_log hx hy, rpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
rw : x ^ n < y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) < y
⊢ x ^ n < y ↔ (↑n : ℝ) * log x < log y
have rw₁ : x ^ n < y ↔ x ^ n < y
Tactic: rw [← rpow_lt_iff_lt_log hx hy, rpow_intCast]
-- 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_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]
-- 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_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]
-- 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_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]
-- 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_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]
-- 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_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| < 1 / t
have rw : |log x * x ^ t| * t < 1
Tactic: rw [lt_div_iff₀ ht]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| * t < 1
have this : |log (x ^ t) * x ^ t| < 1
Tactic: have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1
have rwa : ∀ (this : |t * log x * x ^ t| < 1), |log x * x ^ t| * t < 1
Tactic: rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
rwa : ∀ (this : |t * log x * x ^ t| < 1), |log x * x ^ t| * t < 1
⊢ |log x * x ^ t| * t < 1
have rwa₁ : ∀ (this : |t * (log x * x ^ t)| < 1), |log x * x ^ t| * t < 1
Tactic: rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
rwa : ∀ (this : |t * log x * x ^ t| < 1), |log x * x ^ t| * t < 1
rwa₁ : ∀ (this : |t * (log x * x ^ t)| < 1), |log x * x ^ t| * t < 1
⊢ |log x * x ^ t| * t < 1
have rwa₂ : ∀ (this : |t| * |log x * x ^ t| < 1), |log x * x ^ t| * t < 1
Tactic: rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
rwa : ∀ (this : |t * log x * x ^ t| < 1), |log x * x ^ t| * t < 1
rwa₁ : ∀ (this : |t * (log x * x ^ t)| < 1), |log x * x ^ t| * t < 1
rwa₂ : ∀ (this : |t| * |log x * x ^ t| < 1), |log x * x ^ t| * t < 1
⊢ |log x * x ^ t| * t < 1
have rwa₃ : ∀ (this : t * |log x * x ^ t| < 1), |log x * x ^ t| * t < 1
Tactic: rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
rwa : ∀ (this : |t * log x * x ^ t| < 1), |log x * x ^ t| * t < 1
rwa₁ : ∀ (this : |t * (log x * x ^ t)| < 1), |log x * x ^ t| * t < 1
rwa₂ : ∀ (this : |t| * |log x * x ^ t| < 1), |log x * x ^ t| * t < 1
rwa₃ : ∀ (this : t * |log x * x ^ t| < 1), |log x * x ^ t| * t < 1
⊢ |log x * x ^ t| * t < 1
have rwa₄ : ∀ (this : |log x * x ^ t| * t < 1), |log x * x ^ t| * t < 1
Tactic: rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
⊢ log x ≤ x ^ ε / ε
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
Tactic: rcases hx.eq_or_lt with rfl | h
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
⊢ log x ≤ x ^ ε / ε
have inr : ∀ (h : 0 < x), log x ≤ x ^ ε / ε
Tactic: rcases hx.eq_or_lt with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
hx : LE.le (α := ℝ) 0 0
⊢ log 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
have inl : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
Tactic: rw [log_zero, zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
ε : ℝ
hε : 0 < ε
hx : LE.le (α := ℝ) 0 0
inl : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
⊢ log 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
have inl₁ : 0 ≤ 0 / ε
Tactic: rw [log_zero, zero_rpow hε.ne', zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε
have inr : ε * log x ≤ x ^ ε
Tactic: rw [le_div_iff₀' hε]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ b ^ x
have simp_rw : StrictMono (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)
Tactic: simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
hb : 1 ≤ b
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x
have rcases : ∀ (hb : 1 < b), Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x
Tactic: rcases lt_or_eq_of_le hb with hb | rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
hb : 1 ≤ b
rcases : ∀ (hb : 1 < b), Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x
have rcases₁ : ∀ (hb : LE.le (α := ℝ) 1 1), Monotone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x
Tactic: rcases lt_or_eq_of_le hb with hb | rfl
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
hb : LE.le (α := ℝ) 1 1
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x
have case : ∀ ⦃a b : ℝ⦄,
  a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)
Tactic: case inr => intro _ _ _; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti (β := ℝ) fun (x : ℝ) ↦ b ^ x
have simp_rw : StrictAnti (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)
Tactic: simp_rw [Real.rpow_def_of_pos hb₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x
have rcases : ∀ (hb₁ : b < 1), Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x
Tactic: rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b ≤ 1
rcases : ∀ (hb₁ : b < 1), Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x
have rcases₁ : ∀ (hb₀ : LT.lt (α := ℝ) 0 1) (hb₁ : LE.le (α := ℝ) 1 1), Antitone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x
Tactic: rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
Cleared hypotheses: b, hb₀, hb₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
hb₀ : LT.lt (α := ℝ) 0 1
hb₁ : LE.le (α := ℝ) 1 1
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x
have case : ∀ ⦃a b : ℝ⦄,
  a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)
Tactic: case inr => intro _ _ _; simp