awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
pos : ∀ (h_top : a + b = ∞), a ^ p + b ^ p ≤ (a + b) ^ p
neg : ∀ (h_top : ¬a + b = ∞), a ^ p + b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
by_cases h_top : a + b = ⊤
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ∞
⊢ (a + b) ^ p = ∞

Tactic:
rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top

Premises used: ENNReal.rpow_eq_top_iff_of_pos
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ∞
pos : a ^ p + b ^ p ≤ ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
rw [h_top]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ∞
⊢ a ^ p + b ^ p ≤ ∞

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ∞
⊢ a ^ p + b ^ p ≤ ∞

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
⊢ a ≠ ∞

Tactic:
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top

Premises used: Iff.mp, ENNReal.add_ne_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
ha_top : a ≠ ∞
⊢ b ≠ ∞

Tactic:
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top

Premises used: Iff.mp, ENNReal.add_ne_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
ha_top : a ≠ ∞
hb_top : b ≠ ∞
⊢ a ≠ ∞

Tactic:
ha_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
ha_top : a ≠ ∞
hb_top : b ≠ ∞
neg : ∀ (a : ℝ≥0) (h_top : ¬(↑a : ℝ≥0∞) + b = ∞), (↑a : ℝ≥0∞) ^ p + b ^ p ≤ ((↑a : ℝ≥0∞) + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
lift a to ℝ≥0 using ha_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ∞
a : ℝ≥0
h_top : ¬(↑a : ℝ≥0∞) + b = ∞
⊢ b ≠ ∞

Tactic:
hb_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ∞
a : ℝ≥0
h_top : ¬(↑a : ℝ≥0∞) + b = ∞
neg :
  ∀ (b : ℝ≥0) (h_top : ¬(↑a : ℝ≥0∞) + (↑b : ℝ≥0∞) = ∞),
    (↑a : ℝ≥0∞) ^ p + (↑b : ℝ≥0∞) ^ p ≤ ((↑a : ℝ≥0∞) + (↑b : ℝ≥0∞)) ^ p
⊢ (↑a : ℝ≥0∞) ^ p + b ^ p ≤ ((↑a : ℝ≥0∞) + b) ^ p

Tactic:
lift b to ℝ≥0 using hb_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬(↑a : ℝ≥0∞) + (↑b : ℝ≥0∞) = ∞
⊢ (↑a : ℝ≥0∞) ^ p + (↑b : ℝ≥0∞) ^ p ≤ ((↑a : ℝ≥0∞) + (↑b : ℝ≥0∞)) ^ p

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg _ hp_pos.le] using
    ENNReal.coe_le_coe.2 (NNReal.add_rpow_le_rpow_add a b hp1)

Premises used: Iff.mpr, ENNReal.coe_rpow_of_nonneg, ENNReal.coe_le_coe, LT.lt.le, NNReal.add_rpow_le_rpow_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p⁻¹

Tactic:
simp [lt_of_lt_of_le zero_lt_one hp1]

Premises used: zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
rw : a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
rw [one_div, ← @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1])]

Premises used: ENNReal.le_rpow_inv_iff, one_div
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
rw : a ^ p + b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
add_rpow_le_rpow_add _ _ hp1

Premises used: ENNReal.add_rpow_le_rpow_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
exact add_rpow_le_rpow_add _ _ hp1

Premises used: ENNReal.add_rpow_le_rpow_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a_1 b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
rw : a ^ q = a ^ (p * (q / p))
rw₁ rw₂ : a ^ q = a ^ q
⊢ a ^ q = (a ^ p) ^ (q / p)

Tactic:
rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']

Premises used: ENNReal.rpow_mul, mul_div_cancel₀, LT.lt.ne'
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
⊢ ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)

Tactic:
have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
    rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Premises used: HPow.hPow, ENNReal.rpow_add_rpow_le_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
refine : 1 ≤ q / p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Premises used: HPow.hPow, ENNReal.rpow_add_rpow_le_add
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
rwa rwa₁ rwa₂ rwa₃ : p ≤ q
⊢ 1 ≤ q / p

Tactic:
rwa [one_le_div hp_pos]

Premises used: one_le_div
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
have h_rpow_add_rpow_le_add :
    ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p := by
    refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
    rwa [one_le_div hp_pos]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
rw : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
rw [h_rpow a, h_rpow b, one_div p, ENNReal.le_rpow_inv_iff hp_pos, ← ENNReal.rpow_mul, mul_comm,
    mul_one_div]

Premises used: ENNReal.rpow_mul, ENNReal.le_rpow_inv_iff, mul_one_div, one_div, mul_comm
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p),
    ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p

Tactic:
rwa [one_div_div] at h_rpow_add_rpow_le_add

Premises used: one_div_div
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
inl :
  ∀ (hp : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
    HPow.hPow (β := ℝ) (a + b) 0 ≤ HPow.hPow (β := ℝ) a 0 + HPow.hPow (β := ℝ) b 0
inr : ∀ (hp_pos : 0 < p), (a + b) ^ p ≤ a ^ p + b ^ p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rcases hp.eq_or_lt with (rfl | hp_pos)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
a b : ℝ≥0∞
hp : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
⊢ HPow.hPow (β := ℝ) (a + b) 0 ≤ HPow.hPow (β := ℝ) a 0 + HPow.hPow (β := ℝ) b 0

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
have h := rpow_add_rpow_le a b hp_pos hp1
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [one_div_one, one_div] at h

Premises used: one_div, one_div_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [ENNReal.rpow_one] at h

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ a + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [ENNReal.rpow_one] at h

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ a + b ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
rw [ENNReal.rpow_one] at h

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ a + b ≤ (a ^ p + b ^ p) ^ p⁻¹

Tactic:
repeat' rw [ENNReal.rpow_one] at h

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
(ENNReal.le_rpow_inv_iff hp_pos).mp h

Premises used: ENNReal.le_rpow_inv_iff, Iff.mp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
exact (ENNReal.le_rpow_inv_iff hp_pos).mp h

Premises used: ENNReal.le_rpow_inv_iff, Iff.mp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
hnc : p ∉ Set.Ioo 0 1
⊢ p.LpAddConst = 1

Tactic:
rw [LpAddConst, if_neg]

Premises used: ENNReal.LpAddConst, if_neg
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ False

Tactic:
lt_irrefl _ (h.2.trans_le hp)

Premises used: lt_irrefl, And.right, LT.lt.trans_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ False

Tactic:
exact lt_irrefl _ (h.2.trans_le hp)

Premises used: lt_irrefl, And.right, LT.lt.trans_le
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
hnc : 0 ∉ Set.Ioo 0 1
⊢ LpAddConst 0 = 1

Tactic:
rw [LpAddConst, if_neg]

Premises used: ENNReal.LpAddConst, if_neg
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) 0
⊢ False

Tactic:
lt_irrefl _ h.1

Premises used: lt_irrefl, And.left
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) 0
⊢ False

Tactic:
exact lt_irrefl _ h.1

Premises used: lt_irrefl, And.left
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
pos : ∀ (h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p), HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) < ∞
neg : ∀ (h : p ∉ Set.Ioo 0 1), LT.lt (α := ℝ≥0∞) 1 ∞
⊢ (if Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p then HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) else 1) < ∞

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
apply : 0 ≤ 1 / p.toReal - 1
⊢ HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) < ∞

Tactic:
apply ENNReal.rpow_lt_top_of_nonneg _ ENNReal.ofNat_ne_top

Premises used: ENNReal.ofNat_ne_top, ENNReal.rpow_lt_top_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
rw : ENNReal.toReal 1 ≤ p⁻¹.toReal
⊢ 0 ≤ 1 / p.toReal - 1

Tactic:
rw [one_div, sub_nonneg, ← ENNReal.toReal_inv, ← ENNReal.toReal_one]

Premises used: ENNReal.toReal_one, ENNReal.toReal_inv, one_div, sub_nonneg
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ p⁻¹ ≠ ∞

Tactic:
simpa using h.1.ne'

Premises used: LT.lt.ne', And.left
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ ENNReal.toReal 1 ≤ p⁻¹.toReal

Tactic:
exact ENNReal.toReal_mono (by simpa using h.1.ne') (ENNReal.one_le_inv.2 h.2.le)

Premises used: Iff.mpr, ENNReal.one_le_inv, LT.lt.le, And.right, ENNReal.toReal_mono
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ LT.lt (α := ℝ≥0∞) 1 ∞

Tactic:
ENNReal.one_lt_top

Premises used: ENNReal.one_lt_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ LT.lt (α := ℝ≥0∞) 1 ∞

Tactic:
exact ENNReal.one_lt_top

Premises used: ENNReal.one_lt_top
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
pos : ∀ (h : 1 < p), (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
neg : ∀ (h : ¬1 < p), (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
by_cases h : 1 < p
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
left : 0 < (ENNReal.ofReal p)⁻¹
right : (ENNReal.ofReal p)⁻¹ < 1
⊢ Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹

Tactic:
constructor
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ 0 < (ENNReal.ofReal p)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
right : 1 < ENNReal.ofReal p
right₁ right₂ right₃ right₄ : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1

Tactic:
rwa [ENNReal.inv_lt_one, one_lt_ofReal]

Premises used: ENNReal.inv_lt_one, ENNReal.one_lt_ofReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹

Tactic:
have hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo (0 : ℝ≥0∞) 1 := by
      constructor
      · simp
      · rwa [ENNReal.inv_lt_one, one_lt_ofReal]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
rw :
  (if Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹ then
      HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
    else 1) =
    HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
rw₁ rw₂ :
  HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) =
    HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
⊢ (ENNReal.ofReal p)⁻¹.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)

Tactic:
rw [LpAddConst, if_pos hmem]

Premises used: if_pos, ENNReal.LpAddConst
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
pos : (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) * (z₁ ^ p + z₂ ^ p)
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
rw [show LpAddConst (ENNReal.ofReal p)⁻¹ =
        (2 : ℝ≥0∞) ^ (1 / ((ENNReal.ofReal p)⁻¹).toReal - 1) from by
      rw [LpAddConst, if_pos hmem]]
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
pos : (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 ((ENNReal.ofReal p).toReal - 1) * (z₁ ^ p + z₂ ^ p)
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
simp only [ENNReal.toReal_inv, div_inv_eq_mul, one_mul]

Premises used: ENNReal.toReal_inv, div_inv_eq_mul, one_mul
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
pos : (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 ((ENNReal.ofReal p).toReal - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
rw [ENNReal.toReal_ofReal hp]

Premises used: ENNReal.toReal_ofReal
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
rpow_add_le_mul_rpow_add_rpow _ _ h.le

Premises used: LT.lt.le, ENNReal.rpow_add_le_mul_rpow_add_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
exact rpow_add_le_mul_rpow_add_rpow _ _ h.le

Premises used: LT.lt.le, ENNReal.rpow_add_le_mul_rpow_add_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ p ≤ 1

Tactic:
have hp1 : p ≤ 1 := not_lt.mp h
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
hp1 : p ≤ 1
neg : (z₁ + z₂) ^ p ≤ z₁ ^ p + z₂ ^ p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
rw [LpAddConst_of_one_le (ENNReal.one_le_inv.mpr (ENNReal.ofReal_le_one.mpr hp1)), one_mul]

Premises used: Iff.mpr, ENNReal.one_le_inv, ENNReal.LpAddConst_of_one_le, ENNReal.ofReal_le_one, one_mul
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
hp1 : p ≤ 1
⊢ (z₁ + z₂) ^ p ≤ z₁ ^ p + z₂ ^ p

Tactic:
rpow_add_le_add_rpow _ _ hp hp1

Premises used: ENNReal.rpow_add_le_add_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
hp1 : p ≤ 1
⊢ (z₁ + z₂) ^ p ≤ z₁ ^ p + z₂ ^ p

Tactic:
exact rpow_add_le_add_rpow _ _ hp hp1

Premises used: ENNReal.rpow_add_le_add_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ p : ℝ≥0∞
pos : ∀ (p_zero : p = 0), (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
neg : ∀ (p_zero : ¬p = 0), (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

Tactic:
by_cases p_zero : p = 0
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : p = 0
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

Tactic:
simp [p_zero, LpAddConst_zero]

Premises used: ENNReal.LpAddConst_zero
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ 0 ≤ p.toReal⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
h :
  p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹) =
    (ENNReal.ofReal p.toReal⁻¹)⁻¹.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

Tactic:
convert! rpow_add_le_mul_rpow_add_rpow' z₁ z₂ (p := p.toReal⁻¹) (by positivity) using 1

Premises used: ENNReal.rpow_add_le_mul_rpow_add_rpow'
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ p⁻¹ ≠ ∞

Tactic:
simpa
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
h :
  p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) =
    (ENNReal.ofReal p⁻¹.toReal)⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
h₁ : p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) = p⁻¹⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
h₂ h₃ : p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) = p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
⊢ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹) =
    (ENNReal.ofReal p.toReal⁻¹)⁻¹.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)

Tactic:
rw [← ENNReal.toReal_inv, ENNReal.ofReal_toReal (by simpa), inv_inv]

Premises used: ENNReal.toReal_inv, ENNReal.ofReal_toReal, inv_inv
-- Module: Mathlib.Analysis.MellinInversion
Goal:
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) univ x → HasDerivWithinAt (rexp ∘ Neg.neg) (-rexp (-x)) univ x

Tactic:
fun x _ ↦ mul_neg_one (rexp (-x)) ▸
    ((Real.hasDerivAt_exp (-x)).comp x (hasDerivAt_neg x)).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivAt.comp, Eq.rec, Real.exp, hasDerivAt_neg, Real.hasDerivAt_exp, mul_neg_one, Neg.neg
-- Module: Mathlib.Analysis.MellinInversion
Goal:
rw : rexp '' Neg.neg '' univ = Ioi 0
rw₁ : rexp '' univ = Ioi 0
rw₂ : range rexp = Ioi 0
rw₃ rw₄ : Eq (α := Set ℝ) (Ioi 0) (Ioi 0)
⊢ rexp ∘ Neg.neg '' univ = Ioi 0

Tactic:
rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]

Premises used: Set.image_univ, Real.range_exp, neg_surjective, Set.image_univ_of_surjective, Set.image_comp
-- Module: Mathlib.Analysis.MellinInversion
Goal:
⊢ InjOn (rexp ∘ Neg.neg) univ

Tactic:
Real.exp_injective.injOn.comp neg_injective.injOn (univ.mapsTo_univ _)

Premises used: Set.mapsTo_univ, Function.Injective.injOn, Set.InjOn.comp, Set.univ, neg_injective, Real.exp_injective
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
change : (↑(rexp (-x)) : ℂ) • cexp (-(↑x : ℂ)) ^ (s - 1) • f = cexp (-s * (↑x : ℂ)) • f
⊢ rexp (-x) • cexp (-(↑x : ℂ)) ^ (s - 1) • f = cexp (-s * (↑x : ℂ)) • f

Tactic:
change (rexp (-x) : ℂ) • _ = _ • f

Premises used: Real.exp, Complex.ofReal, Neg.neg
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
rw : ((↑(rexp (-x)) : ℂ) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
⊢ (↑(rexp (-x)) : ℂ) • cexp (-(↑x : ℂ)) ^ (s - 1) • f = cexp (-s * (↑x : ℂ)) • f

Tactic:
rw [← smul_assoc, smul_eq_mul]

Premises used: smul_assoc, smul_eq_mul
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
push_cast : (cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
⊢ ((↑(rexp (-x)) : ℂ) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f

Tactic:
push_cast
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
lhs : cexp (-(↑x : ℂ))
| cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)

Tactic:
lhs
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
rw : HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1
| cexp (-(↑x : ℂ))

Tactic:
rw [← cpow_one (cexp _)]

Premises used: Complex.cpow_one, Complex.exp
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
rw : HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1
| cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)

Tactic:
lhs; rw [← cpow_one (cexp _)]

Premises used: Complex.cpow_one, Complex.exp
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
conv : (HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1 * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
⊢ (cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f

Tactic:
conv in cexp _ * _ => lhs; rw [← cpow_one (cexp _)]

Premises used: Complex.cpow_one, Complex.exp
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ -π < (-(↑x : ℂ)).im

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (-(↑x : ℂ)).im ≤ π

Tactic:
simpa using pi_nonneg

Premises used: Real.pi_nonneg