awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log x ≤ log (y ^ z) ↔ log x ≤ z * log y
rw₁ rw₂ : log x ≤ z * log y ↔ log x ≤ z * log y
⊢ x ≤ y ^ z ↔ log x ≤ z * log y

Tactic:
rw [← log_le_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, Real.log_le_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ≤ y ^ n ↔ log x ≤ (↑n : ℝ) * log y

Tactic:
rpow_natCast _ _ ▸ le_rpow_iff_log_le hx hy

Premises used: Eq.rec, Real.le_rpow_iff_log_le, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ≤ y ^ n ↔ log x ≤ (↑n : ℝ) * log y

Tactic:
rpow_intCast _ _ ▸ le_rpow_iff_log_le hx hy

Premises used: Eq.rec, Real.le_rpow_iff_log_le, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
inl : ∀ (hx : x ≤ 0), x ≤ y ^ z
inr : ∀ (hx : 0 < x), x ≤ y ^ z
⊢ x ≤ y ^ z

Tactic:
obtain hx | hx := le_or_gt x 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

Tactic:
hx.trans (rpow_pos_of_pos hy _).le

Premises used: Real.rpow_pos_of_pos, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

Tactic:
exact hx.trans (rpow_pos_of_pos hy _).le

Premises used: Real.rpow_pos_of_pos, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Tactic:
(le_rpow_iff_log_le hx hy).2 h

Premises used: Iff.mpr, Real.le_rpow_iff_log_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Tactic:
exact (le_rpow_iff_log_le hx hy).2 h

Premises used: Iff.mpr, Real.le_rpow_iff_log_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hy : 0 < y
h : log x ≤ (↑n : ℝ) * log y
⊢ x ≤ y ^ n

Tactic:
rpow_natCast _ _ ▸ le_rpow_of_log_le hy h

Premises used: Eq.rec, Real.rpow_natCast, Real.le_rpow_of_log_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hy : 0 < y
h : log x ≤ (↑n : ℝ) * log y
⊢ x ≤ y ^ n

Tactic:
rpow_intCast _ _ ▸ le_rpow_of_log_le hy h

Premises used: Eq.rec, Real.rpow_intCast, Real.le_rpow_of_log_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log x < log (y ^ z) ↔ log x < z * log y
rw₁ rw₂ : log x < z * log y ↔ log x < z * log y
⊢ x < y ^ z ↔ log x < z * log y

Tactic:
rw [← log_lt_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ n ↔ log x < (↑n : ℝ) * log y

Tactic:
rpow_natCast _ _ ▸ lt_rpow_iff_log_lt hx hy

Premises used: Eq.rec, Real.rpow_natCast, Real.lt_rpow_iff_log_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ n ↔ log x < (↑n : ℝ) * log y

Tactic:
rpow_intCast _ _ ▸ lt_rpow_iff_log_lt hx hy

Premises used: Eq.rec, Real.rpow_intCast, Real.lt_rpow_iff_log_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
inl : ∀ (hx : x ≤ 0), x < y ^ z
inr : ∀ (hx : 0 < x), x < y ^ z
⊢ x < y ^ z

Tactic:
obtain hx | hx := le_or_gt x 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

Tactic:
hx.trans_lt (rpow_pos_of_pos hy _)

Premises used: Real.rpow_pos_of_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

Tactic:
exact hx.trans_lt (rpow_pos_of_pos hy _)

Premises used: Real.rpow_pos_of_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Tactic:
(lt_rpow_iff_log_lt hx hy).2 h

Premises used: Iff.mpr, Real.lt_rpow_iff_log_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Tactic:
exact (lt_rpow_iff_log_lt hx hy).2 h

Premises used: Iff.mpr, Real.lt_rpow_iff_log_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hy : 0 < y
h : log x < (↑n : ℝ) * log y
⊢ x < y ^ n

Tactic:
rpow_natCast _ _ ▸ lt_rpow_of_log_lt hy h

Premises used: Eq.rec, Real.lt_rpow_of_log_lt, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hy : 0 < y
h : log x < (↑n : ℝ) * log y
⊢ x < y ^ n

Tactic:
rpow_intCast _ _ ▸ lt_rpow_of_log_lt hy h

Premises used: Eq.rec, Real.lt_rpow_of_log_lt, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log (x ^ z) ≤ log y ↔ z * log x ≤ log y
rw₁ rw₂ : z * log x ≤ log y ↔ z * log x ≤ log y
⊢ x ^ z ≤ y ↔ z * log x ≤ log y

Tactic:
rw [← log_le_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, Real.log_le_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
rw : x ^ n ≤ y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) ≤ y
rw₁ rw₂ : x ^ n ≤ y ↔ x ^ n ≤ y
⊢ x ^ n ≤ y ↔ (↑n : ℝ) * log x ≤ log y

Tactic:
rw [← rpow_le_iff_le_log hx hy, rpow_natCast]

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

Tactic:
rw [← rpow_le_iff_le_log hx hy, rpow_intCast]

Premises used: Real.rpow_le_iff_le_log, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
h : x ^ z ≤ y
⊢ 0 < x ^ z

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
h : x ^ n ≤ y
⊢ (↑n : ℝ) * log x ≤ log y

Tactic:
le_log_of_rpow_le hx (rpow_natCast _ _ ▸ h)

Premises used: Eq.rec, Real.le_log_of_rpow_le, Eq.symm, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
h : x ^ n ≤ y
⊢ (↑n : ℝ) * log x ≤ log y

Tactic:
le_log_of_rpow_le hx (rpow_intCast _ _ ▸ h)

Premises used: Eq.rec, Real.le_log_of_rpow_le, Eq.symm, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hy : 0 < y
h : log x ≤ (↑n : ℝ) * log y
⊢ x ≤ y ^ n

Tactic:
rpow_natCast _ _ ▸ rpow_le_of_le_log hy h

Premises used: Eq.rec, Real.rpow_le_of_le_log, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hy : 0 < y
h : log x ≤ (↑n : ℝ) * log y
⊢ x ≤ y ^ n

Tactic:
rpow_intCast _ _ ▸ rpow_le_of_le_log hy h

Premises used: Eq.rec, Real.rpow_le_of_le_log, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
hy : 0 < y
rw : log (x ^ z) < log y ↔ z * log x < log y
rw₁ rw₂ : z * log x < log y ↔ z * log x < log y
⊢ x ^ z < y ↔ z * log x < log y

Tactic:
rw [← log_lt_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, Real.log_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
rw : x ^ n < y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) < y
rw₁ rw₂ : x ^ n < y ↔ x ^ n < y
⊢ x ^ n < y ↔ (↑n : ℝ) * log x < log y

Tactic:
rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast]

Premises used: Real.rpow_lt_iff_lt_log, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
rw : x ^ n < y ↔ HPow.hPow (β := ℝ) x (↑n : ℝ) < y
rw₁ rw₂ : x ^ n < y ↔ x ^ n < y
⊢ x ^ n < y ↔ (↑n : ℝ) * log x < log y

Tactic:
rw [← rpow_lt_iff_lt_log hx hy, rpow_intCast]

Premises used: Real.rpow_lt_iff_lt_log, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx : 0 < x
h : x ^ z < y
⊢ 0 < x ^ z

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 < x
h : x ^ n < y
⊢ (↑n : ℝ) * log x < log y

Tactic:
lt_log_of_rpow_lt hx (rpow_natCast _ _ ▸ h)

Premises used: Eq.rec, Real.lt_log_of_rpow_lt, Eq.symm, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hx : 0 < x
h : x ^ n < y
⊢ (↑n : ℝ) * log x < log y

Tactic:
lt_log_of_rpow_lt hx (rpow_intCast _ _ ▸ h)

Premises used: Eq.rec, Real.lt_log_of_rpow_lt, Eq.symm, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hy : 0 < y
h : log x < (↑n : ℝ) * log y
⊢ x < y ^ n

Tactic:
rpow_natCast _ _ ▸ rpow_lt_of_lt_log hy h

Premises used: Eq.rec, Real.rpow_natCast, Real.rpow_lt_of_lt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℤ
hy : 0 < y
h : log x < (↑n : ℝ) * log y
⊢ x < y ^ n

Tactic:
rpow_intCast _ _ ▸ rpow_lt_of_lt_log hy h

Premises used: Eq.rec, Real.rpow_intCast, Real.rpow_lt_of_lt_log
-- 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_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]

Premises used: Real.rpow_def_of_pos, LT.lt.le, mul_nonpos_iff, Real.exp_le_one_iff, Real.log_nonpos_iff, Real.log_nonneg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
rw : |log x * x ^ t| * t < 1
⊢ |log x * x ^ t| < 1 / t

Tactic:
rw [lt_div_iff₀ ht]

Premises used: lt_div_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |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)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : |log x * x ^ t| * t < 1), |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

Premises used: Real.log_rpow, mul_assoc, abs_mul, mul_comm, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
inl : ∀ (hx : LE.le (α := ℝ) 0 0), log 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inr : ∀ (h : 0 < x), log x ≤ x ^ ε / ε
⊢ log x ≤ x ^ ε / ε

Tactic:
rcases hx.eq_or_lt with rfl | h

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
ε : ℝ
hε : 0 < ε
hx : LE.le (α := ℝ) 0 0
inl : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₁ : 0 ≤ 0 / ε
inl₂ inl₃ : LE.le (α := ℝ) 0 0
⊢ log 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε

Tactic:
rw [log_zero, zero_rpow hε.ne', zero_div]

Premises used: zero_div, Real.zero_rpow, LT.lt.ne', Real.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
inr : ε * log x ≤ x ^ ε
⊢ log x ≤ x ^ ε / ε

Tactic:
rw [le_div_iff₀' hε]

Premises used: le_div_iff₀'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε

Tactic:
(log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
    (sub_one_lt _).le

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, LT.lt.le, Eq.trans_le, sub_one_lt, LE.le.trans, Eq.symm, Real.log_le_sub_one_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε

Tactic:
exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
    (sub_one_lt _).le

Premises used: Real.rpow_pos_of_pos, Real.log_rpow, LT.lt.le, Eq.trans_le, sub_one_lt, LE.le.trans, Eq.symm, Real.log_le_sub_one_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
⊢ log (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε

Tactic:
log_le_rpow_div n.cast_nonneg hε

Premises used: Nat.cast_nonneg, Real.log_le_rpow_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb : 1 < b
simp_rw : StrictMono (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]

Premises used: Real.rpow_def_of_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb : 1 < b
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)

Tactic:
exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb

Premises used: StrictMono.const_mul, Real.log_pos, Real.exp_strictMono, Real.exp, strictMono_id, StrictMono.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb : 1 < b
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)

Tactic:
exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb

Premises used: StrictMono.const_mul, Real.log_pos, Real.exp_strictMono, strictMono_id, StrictMono.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb : 1 ≤ b
rcases : ∀ (hb : 1 < b), Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x
rcases₁ : ∀ (hb : LE.le (α := ℝ) 1 1), Monotone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
rcases lt_or_eq_of_le hb with hb | rfl

Premises used: lt_or_eq_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb_1 : 1 ≤ b
hb : 1 < b
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
(strictMono_rpow_of_base_gt_one hb).monotone

Premises used: StrictMono.monotone, Real.strictMono_rpow_of_base_gt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb_1 : 1 ≤ b
hb : 1 < b
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
exact (strictMono_rpow_of_base_gt_one hb).monotone

Premises used: StrictMono.monotone, Real.strictMono_rpow_of_base_gt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb_1 : 1 ≤ b
hb : 1 < b
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone

Premises used: StrictMono.monotone, Real.strictMono_rpow_of_base_gt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb : LE.le (α := ℝ) 1 1
a : ℝ
_ :
  ∀ ⦃b : ℝ⦄,
    a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)
⊢ ∀ ⦃b : ℝ⦄,
    a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb : LE.le (α := ℝ) 1 1
a b : ℝ
_ : a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)
⊢ a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb : LE.le (α := ℝ) 1 1
a b : ℝ
h : a ≤ b
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb : LE.le (α := ℝ) 1 1
case case₁ case₂ case₃ :
  ∀ ⦃a b : ℝ⦄,
    a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b)
⊢ Monotone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x

Tactic:
case inr => intro _ _ _; simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
simp_rw : StrictAnti (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)
⊢ StrictAnti (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
simp_rw [Real.rpow_def_of_pos hb₀]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)

Tactic:
exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
      <| Real.log_neg hb₀ hb₁

Premises used: StrictMono.const_mul_of_neg, Real.exp_strictMono, Real.exp, strictMono_id, StrictMono.comp_strictAnti, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti (β := ℝ) fun (x : ℝ) ↦ rexp (log b * x)

Tactic:
exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
      <| Real.log_neg hb₀ hb₁

Premises used: StrictMono.const_mul_of_neg, Real.exp_strictMono, strictMono_id, StrictMono.comp_strictAnti, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b ≤ 1
rcases : ∀ (hb₁ : b < 1), Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x
rcases₁ :
  ∀ (hb₀ : LT.lt (α := ℝ) 0 1) (hb₁ : LE.le (α := ℝ) 1 1), Antitone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
rcases lt_or_eq_of_le hb₁ with hb₁ | rfl

Premises used: lt_or_eq_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁_1 : b ≤ 1
hb₁ : b < 1
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
(strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone

Premises used: Real.strictAnti_rpow_of_base_lt_one, StrictAnti.antitone
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁_1 : b ≤ 1
hb₁ : b < 1
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone

Premises used: Real.strictAnti_rpow_of_base_lt_one, StrictAnti.antitone
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
hb₀ : 0 < b
hb₁_1 : b ≤ 1
hb₁ : b < 1
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ b ^ x

Tactic:
case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone

Premises used: Real.strictAnti_rpow_of_base_lt_one, StrictAnti.antitone
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb₀ : LT.lt (α := ℝ) 0 1
hb₁ : LE.le (α := ℝ) 1 1
a : ℝ
_ :
  ∀ ⦃b : ℝ⦄,
    a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)
⊢ ∀ ⦃b : ℝ⦄,
    a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb₀ : LT.lt (α := ℝ) 0 1
hb₁ : LE.le (α := ℝ) 1 1
a b : ℝ
_ : a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)
⊢ a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb₀ : LT.lt (α := ℝ) 0 1
hb₁ : LE.le (α := ℝ) 1 1
a b : ℝ
h : a ≤ b
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
hb₀ : LT.lt (α := ℝ) 0 1
hb₁ : LE.le (α := ℝ) 1 1
case case₁ case₂ case₃ :
  ∀ ⦃a b : ℝ⦄,
    a ≤ b → LE.le (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) b) ((fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x) a)
⊢ Antitone (β := ℝ) fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 1 x

Tactic:
case inr => intro _ _ _; simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : y = z
rw rw₁ : x ^ z = x ^ z
⊢ x ^ y = x ^ z

Tactic:
rw [H]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
refine : ∀ (H : x ^ y = x ^ z), y = z
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ by rw [H]⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
inl : ∀ (h : x < 1), y = z
inr : ∀ (h : 1 < x), y = z
⊢ y = z

Tactic:
rcases hx₁.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : x < 1
⊢ y = z

Tactic:
(strictAnti_rpow_of_base_lt_one hx₀ h).injective H

Premises used: Real.strictAnti_rpow_of_base_lt_one, StrictAnti.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : x < 1
⊢ y = z

Tactic:
exact (strictAnti_rpow_of_base_lt_one hx₀ h).injective H

Premises used: Real.strictAnti_rpow_of_base_lt_one, StrictAnti.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : 1 < x
⊢ y = z

Tactic:
(strictMono_rpow_of_base_gt_one h).injective H

Premises used: Real.strictMono_rpow_of_base_gt_one, StrictMono.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : 1 < x
⊢ y = z

Tactic:
exact (strictMono_rpow_of_base_gt_one h).injective H

Premises used: Real.strictMono_rpow_of_base_gt_one, StrictMono.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y
inl : ∀ (x1 : 1 ≤ x) (yz : y ≤ z), x ^ y ≤ x ^ z
inr : ∀ (x0 : 0 < x) (x1 : x ≤ 1) (zy : z ≤ y), x ^ y ≤ x ^ z
⊢ x ^ y ≤ x ^ z

Tactic:
rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
Real.rpow_le_rpow_of_exponent_le x1 yz

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
exact Real.rpow_le_rpow_of_exponent_le x1 yz

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
Real.rpow_le_rpow_of_exponent_ge x0 x1 zy

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
exact Real.rpow_le_rpow_of_exponent_ge x0 x1 zy

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
linarith : -s.re = 0 → -1 + -(-s.re - 0) + (1 - s.re) = 0
⊢ -s.re ≠ 0

Tactic:
linarith only [hs]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
rw : HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re ≤ 1 / 2
⊢ ‖HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)‖ ≤ 1 / 2

Tactic:
rw [norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]]

Premises used: Subtype.val, Complex.norm_natCast_cpow_of_re_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
linarith : 0 < -s.re → -1 + (0 - -s.re) + (1 - s.re) = 0
⊢ -s.re ≤ 0

Tactic:
linarith only [hs]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
refine : HPow.hPow (α := ℝ) 2 (-s).re ≤ 1 / 2
⊢ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re ≤ 1 / 2

Tactic:
refine (Real.rpow_le_rpow_of_nonpos zero_lt_two (Nat.cast_le.mpr p.prop.two_le) <|
    by rw [neg_re]; linarith only [hs]).trans ?_

Premises used: Iff.mpr, Real.rpow_le_rpow_of_nonpos, Subtype.prop, Nat.Prime.two_le, Nat.cast_le, LE.le.trans, zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
rw : HPow.hPow (α := ℝ) 2 (-s).re ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 (-1)
⊢ HPow.hPow (α := ℝ) 2 (-s).re ≤ 1 / 2

Tactic:
rw [one_div, ← Real.rpow_neg_one]

Premises used: Real.rpow_neg_one, one_div