awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ 0 ≤ log x

Tactic:
log_nonneg hx

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

Tactic:
exact log_nonneg hx

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
r : ℝ
hr : r < 0
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r) (Set.Ioi 0)

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

Premises used: StrictAntiOn, Real.rpow_lt_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
r : ℝ
hr : r ≤ 0
⊢ AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r) (Set.Ioi 0)

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

Premises used: Real.rpow_le_rpow_of_nonpos, AntitoneOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
⊢ 0 < x

Tactic:
have x_pos : 0 < x := lt_trans zero_lt_one hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rw₃ rw₄ : y ≤ z ↔ y ≤ z
⊢ x ^ y ≤ 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)]

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, Real.log_pos, Real.log_le_log_iff, mul_le_mul_iff_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 1 < x
rw : ¬x ^ z ≤ x ^ y ↔ y < z
rw₁ : ¬z ≤ y ↔ y < z
rw₂ rw₃ : ¬z ≤ y ↔ ¬z ≤ y
⊢ x ^ y < x ^ z ↔ y < z

Tactic:
rw [lt_iff_not_ge, rpow_le_rpow_left_iff hx, lt_iff_not_ge]

Premises used: lt_iff_not_ge, Real.rpow_le_rpow_left_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
rw : rexp (log x * y) < x ^ z
⊢ x ^ y < x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

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

Tactic:
rw [rpow_def_of_pos hx0]

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

Tactic:
repeat' rw [rpow_def_of_pos hx0]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
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 : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z

Tactic:
mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)

Premises used: Real.log_neg, mul_lt_mul_of_neg_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z

Tactic:
exact mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)

Premises used: Real.log_neg, mul_lt_mul_of_neg_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
rw : rexp (log x * y) ≤ x ^ z
⊢ x ^ y ≤ x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
rw : rexp (log x * y) ≤ rexp (log x * z)
⊢ rexp (log x * y) ≤ x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
repeat' : rexp (log x * y) ≤ rexp (log x * z)
⊢ x ^ y ≤ x ^ z

Tactic:
repeat' rw [rpow_def_of_pos hx0]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
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 : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z

Tactic:
mul_le_mul_of_nonpos_left hyz (log_nonpos (le_of_lt hx0) hx1)

Premises used: mul_le_mul_of_nonpos_left, le_of_lt, Real.log_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z

Tactic:
exact mul_le_mul_of_nonpos_left hyz (log_nonpos (le_of_lt hx0) hx1)

Premises used: mul_le_mul_of_nonpos_left, le_of_lt, Real.log_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rw₃ rw₄ : z ≤ y ↔ z ≤ y
⊢ x ^ y ≤ 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)]

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, mul_le_mul_right_of_neg, Real.log_le_log_iff, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
rw : ¬x ^ z ≤ x ^ y ↔ z < y
rw₁ : ¬y ≤ z ↔ z < y
rw₂ rw₃ : ¬y ≤ z ↔ ¬y ≤ z
⊢ x ^ y < x ^ z ↔ z < y

Tactic:
rw [lt_iff_not_ge, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_ge]

Premises used: lt_iff_not_ge, Real.rpow_le_rpow_left_iff_of_base_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
rw : x ^ z < HPow.hPow (α := ℝ) 1 z
⊢ x ^ z < 1

Tactic:
rw [← one_rpow z]

Premises used: Real.one_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < HPow.hPow (α := ℝ) 1 z

Tactic:
rpow_lt_rpow hx1 hx2 hz

Premises used: Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < HPow.hPow (α := ℝ) 1 z

Tactic:
exact rpow_lt_rpow hx1 hx2 hz

Premises used: Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
rw : x ^ z ≤ HPow.hPow (α := ℝ) 1 z
⊢ x ^ z ≤ 1

Tactic:
rw [← one_rpow z]

Premises used: Real.one_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
h : 0 ≤ x
h₂ : 0 ≤ z
⊢ x ^ z ≤ HPow.hPow (α := ℝ) 1 z

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < HPow.hPow (β := ℝ) x 0

Tactic:
rpow_lt_rpow_of_exponent_lt hx hz

Premises used: Real.rpow_lt_rpow_of_exponent_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : z < 0
h : 1 = HPow.hPow (β := ℝ) x 0
⊢ x ^ z < 1

Tactic:
convert! rpow_lt_rpow_of_exponent_lt hx hz

Premises used: Real.rpow_lt_rpow_of_exponent_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
(rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
exact (rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ HPow.hPow (β := ℝ) x 0

Tactic:
rpow_le_rpow_of_exponent_le hx hz

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
h : 1 = HPow.hPow (β := ℝ) x 0
⊢ x ^ z ≤ 1

Tactic:
convert! rpow_le_rpow_of_exponent_le hx hz

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
(rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
exact (rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : 0 < z
rw : HPow.hPow (α := ℝ) 1 z < x ^ z
⊢ 1 < x ^ z

Tactic:
rw [← one_rpow z]

Premises used: Real.one_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ HPow.hPow (α := ℝ) 1 z < x ^ z

Tactic:
rpow_lt_rpow zero_le_one hx hz

Premises used: zero_le_one, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ HPow.hPow (α := ℝ) 1 z < x ^ z

Tactic:
exact rpow_lt_rpow zero_le_one hx hz

Premises used: zero_le_one, Real.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
rw : HPow.hPow (α := ℝ) 1 z ≤ x ^ z
⊢ 1 ≤ x ^ z

Tactic:
rw [← one_rpow z]

Premises used: Real.one_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
h : LE.le (α := ℝ) 0 1
h₂ : 0 ≤ z
⊢ HPow.hPow (α := ℝ) 1 z ≤ x ^ z

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ HPow.hPow (β := ℝ) x 0 < x ^ z

Tactic:
rpow_lt_rpow_of_exponent_gt hx1 hx2 hz

Premises used: Real.rpow_lt_rpow_of_exponent_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
h : 1 = HPow.hPow (β := ℝ) x 0
⊢ 1 < x ^ z

Tactic:
convert! rpow_lt_rpow_of_exponent_gt hx1 hx2 hz

Premises used: Real.rpow_lt_rpow_of_exponent_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
(rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
exact (rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ HPow.hPow (β := ℝ) x 0 ≤ x ^ z

Tactic:
rpow_le_rpow_of_exponent_ge hx1 hx2 hz

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
h : 1 = HPow.hPow (β := ℝ) x 0
⊢ 1 ≤ x ^ z

Tactic:
convert! rpow_le_rpow_of_exponent_ge hx1 hx2 hz

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
(rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = HPow.hPow (β := ℝ) x 0

Tactic:
exact (rpow_zero x).symm

Premises used: Real.rpow_zero, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rw₄ rw₅ : 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
⊢ 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]

Premises used: Real.rpow_def_of_pos, Real.log_pos_iff, LT.lt.le, mul_neg_iff, Real.exp_lt_one_iff, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inr : ∀ (hx : 0 < x), x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

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

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 < 1 ↔
    Eq (α := ℝ) 0 0 ∧ Ne (α := ℝ) 0 0 ∨
      LT.lt (α := ℝ) 1 0 ∧ LT.lt (α := ℝ) 0 0 ∨ LT.lt (α := ℝ) 0 1 ∧ LT.lt (α := ℝ) 0 0
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
⊢ 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)

Premises used: em, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ 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:
simp [*, zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y : ℝ
hx : LE.le (α := ℝ) 0 0
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:
simp [*, zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm]

Premises used: Real.rpow_lt_one_iff_of_pos, Ne.symm, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 < y
rw : x ^ y < 1 ↔ x ^ y < HPow.hPow (α := ℝ) 1 y
rw₁ rw₂ : x ^ y < 1 ↔ x ^ y < 1
⊢ x ^ y < 1 ↔ x < 1

Tactic:
rw [← Real.rpow_lt_rpow_iff hx zero_le_one hy, Real.one_rpow]

Premises used: Real.one_rpow, zero_le_one, Real.rpow_lt_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rw₄ rw₅ : 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0 ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
⊢ 1 < 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]

Premises used: Real.rpow_def_of_pos, Real.log_pos_iff, LT.lt.le, mul_pos_iff, Real.one_lt_exp_iff, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inr : ∀ (hx : 0 < x), 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
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
⊢ 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)

Premises used: em, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ 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:
simp [*, (zero_lt_one' ℝ).not_gt]

Premises used: Real, zero_lt_one', LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y : ℝ
hx : LE.le (α := ℝ) 0 0
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:
simp [*, (zero_lt_one' ℝ).not_gt]

Premises used: Real, zero_lt_one', LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
simp [one_lt_rpow_iff_of_pos hx, hx]

Premises used: Real.one_lt_rpow_iff_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inr : ∀ (hx0' : 0 < x), x ^ y ≤ x ^ z
⊢ x ^ y ≤ x ^ z

Tactic:
rcases eq_or_lt_of_le hx0 with (rfl | hx0')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inl₁ : ∀ (hy0 : y ≠ 0), HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z
⊢ HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z

Tactic:
rcases eq_or_ne y 0 with rfl | hy0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z : ℝ
hx0 : LE.le (α := ℝ) 0 0
hx1 : LE.le (α := ℝ) 0 1
hyz : z ≤ 0
h : Eq (α := ℝ) 0 0 → Eq (α := ℝ) 0 0 → z = 0
inl inl₁ : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (α := ℝ) (β := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (α := ℝ) 0 z

Tactic:
rw [h rfl rfl]

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
inl : 0 ≤ HPow.hPow (α := ℝ) 0 z
⊢ HPow.hPow (α := ℝ) 0 y ≤ HPow.hPow (α := ℝ) 0 z

Tactic:
rw [zero_rpow hy0]

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
⊢ 0 ≤ HPow.hPow (α := ℝ) 0 z

Tactic:
apply zero_rpow_nonneg

Premises used: Real.zero_rpow_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z

Tactic:
rpow_le_rpow_of_exponent_ge hx0' hx1 hyz

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z

Tactic:
exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hz : 0 ≤ z
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
rpow_le_rpow_of_exponent_ge_of_imp hx0 hx1 hyz fun _ hy ↦ le_antisymm (hyz.trans_eq hy) hz

Premises used: LE.le.trans_eq, le_antisymm, Real.rpow_le_rpow_of_exponent_ge_of_imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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)
inr : ∀ (hxy : y ≤ x), max x y ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rcases le_total x y with hxy | hxy

Premises used: le_total
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
h : 0 ≤ x
h₂ : 0 ≤ p
⊢ x ^ p ≤ y ^ p

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
inl : y ^ p = max (x ^ p) (y ^ p)
inl₁ inl₂ : y ^ p = y ^ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_right hxy, max_eq_right (by gcongr)]

Premises used: max_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
h : 0 ≤ y
h₂ : 0 ≤ p
⊢ y ^ p ≤ x ^ p

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
inr : x ^ p = max (x ^ p) (y ^ p)
inr₁ inr₂ : x ^ p = x ^ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_left hxy, max_eq_left (by gcongr)]

Premises used: max_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 0 ≤ x
h₂ : x ≤ 1
h₃ : y ≤ 1
⊢ x ≤ x ^ y

Tactic:
simpa only [rpow_one]
    using rpow_le_rpow_of_exponent_ge_of_imp h₁ h₂ h₃ fun _ ↦ (absurd · one_ne_zero)

Premises used: Real.rpow_one, absurd, Real.rpow_le_rpow_of_exponent_ge_of_imp, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 1 ≤ x
h₂ : 1 ≤ y
⊢ x ≤ x ^ y

Tactic:
simpa only [rpow_one] using rpow_le_rpow_of_exponent_le h₁ h₂

Premises used: Real.rpow_one, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 0 ≤ x
h₂ : x ≤ 1
h₃ : 1 ≤ y
⊢ x ^ y ≤ x

Tactic:
simpa only [rpow_one]
    using rpow_le_rpow_of_exponent_ge_of_imp h₁ h₂ h₃ fun _ ↦ (absurd · (one_pos.trans_le h₃).ne')

Premises used: Real.rpow_one, LT.lt.ne', absurd, LT.lt.trans_le, Real.rpow_le_rpow_of_exponent_ge_of_imp, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 1 ≤ x
h₂ : y ≤ 1
⊢ x ^ y ≤ x

Tactic:
simpa only [rpow_one] using rpow_le_rpow_of_exponent_le h₁ h₂

Premises used: Real.rpow_one, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 0 < x
h₂ : x < 1
h₃ : y < 1
⊢ x < x ^ y

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_gt h₁ h₂ h₃

Premises used: Real.rpow_one, Real.rpow_lt_rpow_of_exponent_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 1 < x
h₂ : 1 < y
⊢ x < x ^ y

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_lt h₁ h₂

Premises used: Real.rpow_one, Real.rpow_lt_rpow_of_exponent_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 0 < x
h₂ : x < 1
h₃ : 1 < y
⊢ x ^ y < x

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_gt h₁ h₂ h₃

Premises used: Real.rpow_one, Real.rpow_lt_rpow_of_exponent_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
h₁ : 1 < x
h₂ : y < 1
⊢ x ^ y < x

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_lt h₁ h₂

Premises used: Real.rpow_one, Real.rpow_lt_rpow_of_exponent_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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⁻¹
rw₅ rw₆ : (z ^ x) ^ x⁻¹ = (z ^ x) ^ x⁻¹
⊢ y = z

Tactic:
rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]

Premises used: mul_inv_cancel₀, Real.rpow_one, Real.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x ^ z = y ^ z ↔ x = y

Tactic:
(rpow_left_injOn hz).eq_iff hx hy

Premises used: Set.InjOn.eq_iff, Real.rpow_left_injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
rw : 0 ≤ x ^ z⁻¹
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
rw [← rpow_left_inj _ hy hz, rpow_inv_rpow hx hz]

Premises used: Real.rpow_left_inj, Real.rpow_inv_rpow
-- 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 ≤ y ^ z⁻¹
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
rw [← rpow_left_inj hx _ hz, rpow_inv_rpow hy hz]

Premises used: Real.rpow_left_inj, Real.rpow_inv_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ y ^ z⁻¹

Tactic:
positivity