awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < p

Tactic:
h.left_pos

Premises used: NNReal.HolderTriple.left_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 ≤ p

Tactic:
h.pos.le

Premises used: LT.lt.le, NNReal.HolderTriple.pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ p ≠ 0

Tactic:
h.pos.ne'

Premises used: LT.lt.ne', NNReal.HolderTriple.pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < p⁻¹

Tactic:
inv_pos.2 h.pos

Premises used: Iff.mpr, inv_pos, NNReal.HolderTriple.pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 ≤ p⁻¹

Tactic:
h.inv_pos.le

Premises used: LT.lt.le, NNReal.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ p⁻¹ ≠ 0

Tactic:
h.inv_pos.ne'

Premises used: LT.lt.ne', NNReal.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < 1 / p

Tactic:
_root_.one_div_pos.2 h.pos

Premises used: Iff.mpr, one_div_pos, NNReal.HolderTriple.pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 ≤ 1 / p

Tactic:
le_of_lt h.one_div_pos

Premises used: le_of_lt, NNReal.HolderTriple.one_div_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 1 / p ≠ 0

Tactic:
ne_of_gt h.one_div_pos

Premises used: ne_of_gt, NNReal.HolderTriple.one_div_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < r

Tactic:
inv_pos.mp <| h.inv_add_inv_eq_inv ▸ add_pos h.inv_pos h.symm.inv_pos

Premises used: add_pos, Eq.rec, inv_pos, NNReal.HolderTriple.inv_add_inv_eq_inv, Iff.mp, NNReal.HolderTriple.symm, NNReal.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 ≤ r

Tactic:
h.pos'.le

Premises used: LT.lt.le, NNReal.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r ≠ 0

Tactic:
h.pos'.ne'

Premises used: NNReal.HolderTriple.pos', LT.lt.ne'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < r⁻¹

Tactic:
inv_pos.2 h.pos'

Premises used: Iff.mpr, inv_pos, NNReal.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 ≤ r⁻¹

Tactic:
h.inv_pos'.le

Premises used: LT.lt.le, NNReal.HolderTriple.inv_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r⁻¹ ≠ 0

Tactic:
h.inv_pos'.ne'

Premises used: LT.lt.ne', NNReal.HolderTriple.inv_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < 1 / r

Tactic:
_root_.one_div_pos.2 h.pos'

Premises used: Iff.mpr, NNReal.HolderTriple.pos', one_div_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 ≤ 1 / r

Tactic:
le_of_lt h.one_div_pos'

Premises used: le_of_lt, NNReal.HolderTriple.one_div_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 1 / r ≠ 0

Tactic:
ne_of_gt h.one_div_pos'

Premises used: ne_of_gt, NNReal.HolderTriple.one_div_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < p ∧ 0 < q ∧ 0 < r

Tactic:
⟨h.pos, h.symm.pos, h.pos'⟩

Premises used: NNReal.HolderTriple.pos', And.intro, NNReal.HolderTriple.pos, NNReal.HolderTriple.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r⁻¹ = p⁻¹ + q⁻¹

Tactic:
h.inv_add_inv_eq_inv.symm

Premises used: NNReal.HolderTriple.inv_add_inv_eq_inv, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
exact_mod_cast h.coe.one_div_add_one_div

Premises used: NNReal.HolderTriple.coe, Real.HolderTriple.one_div_add_one_div
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 1 / r = 1 / p + 1 / q

Tactic:
h.one_div_add_one_div.symm

Premises used: NNReal.HolderTriple.one_div_add_one_div, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
exact_mod_cast h.coe.inv_inv_add_inv

Premises used: NNReal.HolderTriple.coe, Real.HolderTriple.inv_inv_add_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ p⁻¹ < r⁻¹

Tactic:
h.coe.inv_lt_inv

Premises used: NNReal.HolderTriple.coe, Real.HolderTriple.inv_lt_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r < p

Tactic:
h.coe.lt

Premises used: NNReal.HolderTriple.coe, Real.HolderTriple.lt, NNReal.toReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ q⁻¹ ≤ r⁻¹

Tactic:
have := h.symm.inv_lt_inv.le
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this : q⁻¹ ≤ r⁻¹
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
exact_mod_cast h.coe.inv_sub_inv_eq_inv

Premises used: NNReal.HolderTriple.coe, Real.HolderTriple.inv_sub_inv_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹

Tactic:
simp [div_eq_mul_inv, ← mul_add, h.inv_add_inv_eq_inv, h.ne_zero']

Premises used: div_eq_mul_inv, NNReal.HolderTriple.ne_zero', NNReal.HolderTriple.inv_add_inv_eq_inv, mul_add
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < p

Tactic:
have := h.left_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this : 0 < p
⊢ 0 < r

Tactic:
have := h.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this_1 : 0 < p
this : 0 < r
⊢ 0 < p / r

Tactic:
positivity
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < q

Tactic:
have := h.right_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this : 0 < q
⊢ 0 < r

Tactic:
have := h.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this_1 : 0 < q
this : 0 < r
⊢ 0 < q / r

Tactic:
positivity
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
⊢ HAdd.hAdd (α := ℝ≥0) 2⁻¹ 2⁻¹ = 1⁻¹

Tactic:
simpa using add_halves (1 : ℝ≥0)

Premises used: add_halves, OfNat.ofNat
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ q.HolderConjugate p

Tactic:
HolderTriple.symm h

Premises used: NNReal.HolderTriple.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
inv_one (G := ℝ≥0) ▸ h.inv_add_inv_eq_inv

Premises used: inv_one, Eq.rec, NNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ 0 < p - 1

Tactic:
tsub_pos_of_lt h.lt

Premises used: NNReal.HolderTriple.lt, tsub_pos_of_lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p - 1 ≠ 0

Tactic:
h.sub_one_pos.ne'

Premises used: LT.lt.ne', NNReal.HolderConjugate.sub_one_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ (↑1 : ℝ) ≤ (↑p : ℝ)

Tactic:
have : ((1 : ℝ≥0) : ℝ) ≤ p := h.coe.lt.le
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
this : (↑1 : ℝ) ≤ (↑p : ℝ)
⊢ q = p / (p - 1)

Tactic:
exact_mod_cast NNReal.coe_sub this ▸ coe_one ▸ h.coe.conjugate_eq
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p.conjExponent = q

Tactic:
h.conjugate_eq.symm

Premises used: NNReal.conjExponent, NNReal.HolderConjugate.conjugate_eq, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ 1 - p⁻¹ = q⁻¹

Tactic:
tsub_eq_of_eq_add h.symm.inv_add_inv_eq_one.symm

Premises used: NNReal.HolderConjugate.symm, NNReal.HolderConjugate.inv_add_inv_eq_one, tsub_eq_of_eq_add, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ (p - 1) * q = p

Tactic:
mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conjugate_eq

Premises used: HSub.hSub, Eq.rec, NNReal.HolderConjugate.conjugate_eq, NNReal.HolderConjugate.sub_one_ne_zero, Iff.mp, mul_comm, OfNat.ofNat, eq_div_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p * q = p + q

Tactic:
simpa [mul_add, add_mul, h.ne_zero, h.symm.ne_zero, add_comm q] using congr(p * $(h.inv_eq) * q)

Premises used: add_mul, NNReal.HolderTriple.inv_eq, NNReal.HolderConjugate.symm, add_comm, mul_add, NNReal.HolderTriple.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
field_simp : p = q * (p - 1)
⊢ p / q = p - 1

Tactic:
field_simp [h.symm.ne_zero]

Premises used: NNReal.HolderConjugate.symm, NNReal.HolderTriple.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p = q * (p - 1)

Tactic:
linear_combination -h.sub_one_mul_conj

Premises used: NNReal.HolderConjugate.sub_one_mul_conj
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
norm_cast : p⁻¹ + q⁻¹ = 1
⊢ (↑p⁻¹ : ℝ≥0∞) + (↑q⁻¹ : ℝ≥0∞) = 1

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
h.inv_add_inv_eq_one

Premises used: NNReal.HolderConjugate.inv_add_inv_eq_one
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
exact h.inv_add_inv_eq_one

Premises used: NNReal.HolderConjugate.inv_add_inv_eq_one
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
rw : (↑1 : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ)⁻¹ + (↑q : ℝ)⁻¹ = (↑1 : ℝ) ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
⊢ p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Tactic:
rw [← holderConjugate_coe_iff, Real.holderConjugate_iff, ← coe_one]

Premises used: Real.holderConjugate_iff, NNReal.holderConjugate_coe_iff, NNReal.coe_one
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
⊢ (↑1 : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ)⁻¹ + (↑q : ℝ)⁻¹ = (↑1 : ℝ) ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Tactic:
exact_mod_cast Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
simpa using hab
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ≥0
ha₀ : 0 < a
ha₁ : a < 1
⊢ a⁻¹⁻¹ + (1 - a)⁻¹⁻¹ = 1

Tactic:
simpa using add_tsub_cancel_of_le ha₁.le

Premises used: LT.lt.le, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ≥0
ha₀ : 0 < a
ha₁ : a < 1
⊢ (1 - a)⁻¹.HolderConjugate a⁻¹

Tactic:
(inv_one_sub_inv ha₀ ha₁).symm

Premises used: NNReal.HolderConjugate.symm, NNReal.HolderConjugate.inv_one_sub_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
⊢ p.HolderConjugate q ↔ q.HolderConjugate p

Tactic:
⟨.symm, .symm⟩

Premises used: NNReal.HolderConjugate.symm, Iff.intro
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
hp : 1 < p
⊢ 1 < (↑p : ℝ)

Tactic:
exact_mod_cast hp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
hp : 1 < p
rw : (↑q : ℝ) = (↑p : ℝ) / (↑(p - 1) : ℝ) ↔ q = p / (p - 1)
⊢ p.HolderConjugate q ↔ q = p / (p - 1)

Tactic:
rw [← holderConjugate_coe_iff, Real.holderConjugate_iff_eq_conjExponent (by exact_mod_cast hp),
    ← coe_one, ← NNReal.coe_sub hp.le]

Premises used: LT.lt.le, NNReal.holderConjugate_coe_iff, NNReal.coe_one, Real.holderConjugate_iff_eq_conjExponent, NNReal.coe_sub
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
hp : 1 < p
⊢ (↑q : ℝ) = (↑p : ℝ) / (↑(p - 1) : ℝ) ↔ q = p / (p - 1)

Tactic:
exact_mod_cast Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0
h : 1 < p
⊢ p.HolderConjugate p.conjExponent

Tactic:
(holderConjugate_iff_eq_conjExponent h).2 rfl

Premises used: Iff.mpr, NNReal.holderConjugate_iff_eq_conjExponent, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (1 / a).HolderConjugate (1 / b)

Tactic:
simpa using HolderConjugate.inv_inv ha hb hab

Premises used: NNReal.HolderConjugate.inv_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ p.toNNReal.HolderTriple q.toNNReal r.toNNReal

Tactic:
simpa [← NNReal.holderTriple_coe_iff, h.nonneg, h.symm.nonneg, h.nonneg']

Premises used: Real.HolderTriple.nonneg', Real.HolderTriple.symm, NNReal.holderTriple_coe_iff, Real.HolderTriple.nonneg
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p.toNNReal.HolderConjugate q.toNNReal

Tactic:
simpa using Real.HolderTriple.toNNReal h

Premises used: Real.HolderTriple.toNNReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0
hp : 1 < p
rw : (↑(p / (p - 1)) : ℝ≥0∞) = 1 + (↑(p - 1)⁻¹ : ℝ≥0∞)
⊢ (↑(p / (p - 1)) : ℝ≥0∞) = 1 + (↑(p - 1) : ℝ≥0∞)⁻¹

Tactic:
rw [← coe_inv (tsub_pos_of_lt hp).ne']

Premises used: ENNReal.coe_inv, LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0
hp : 1 < p
norm_cast : p / (p - 1) = 1 + (p - 1)⁻¹
⊢ (↑(p / (p - 1)) : ℝ≥0∞) = 1 + (↑(p - 1)⁻¹ : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0
hp : 1 < p
field_simp : p = p - 1 + 1
⊢ p / (p - 1) = 1 + (p - 1)⁻¹

Tactic:
field_simp [(tsub_pos_of_lt hp).ne']

Premises used: LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0
hp : 1 < p
rw rw₁ : p = p
⊢ p = p - 1 + 1

Tactic:
rw [tsub_add_cancel_of_le hp.le]

Premises used: tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
⊢ (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞) ↔ p.HolderTriple q r

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
refine_1 : ∀ (h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)), p.HolderTriple q r
refine_2 : ∀ (h : p.HolderTriple q r), (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞) ↔ p.HolderTriple q r

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
refine_1 : p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
⊢ p.HolderTriple q r

Tactic:
rw [NNReal.holderTriple_iff]

Premises used: NNReal.holderTriple_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
left : p ≠ 0
right : q ≠ 0
⊢ p ≠ 0 ∧ q ≠ 0

Tactic:
constructor
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
q r : ℝ≥0
hr : r ≠ 0
h : (↑0 : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
left : r = 0
⊢ False

Tactic:
apply hr
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
q r : ℝ≥0
hr : r ≠ 0
h : (↑0 : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ r = 0

Tactic:
exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑0 : ℝ≥0∞) (↑r : ℝ≥0∞)
right : r = 0
⊢ False

Tactic:
apply hr
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑0 : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ r = 0

Tactic:
exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ p ≠ 0

Tactic:
obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0 := by
      constructor
      all_goals
        rintro rfl
        apply hr
        exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0 := by
      constructor
      all_goals
        rintro rfl
        apply hr
        exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
hp : p ≠ 0
hq : q ≠ 0
⊢ p⁻¹ + q⁻¹ = r⁻¹

Tactic:
exact_mod_cast h.inv_add_inv_eq_inv

Premises used: ENNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
hp : p ≠ 0
hq : q ≠ 0
⊢ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q

Tactic:
exact ⟨by exact_mod_cast h.inv_add_inv_eq_inv, hp.bot_lt, hq.bot_lt⟩
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
refine_2 : (↑p : ℝ≥0∞)⁻¹ + (↑q : ℝ≥0∞)⁻¹ = (↑r : ℝ≥0∞)⁻¹
⊢ (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)

Tactic:
rw [holderTriple_iff]

Premises used: ENNReal.holderTriple_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ p ≠ 0

Tactic:
have hp := h.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
have hq := h.symm.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
hp : p ≠ 0
hq : q ≠ 0
⊢ (↑p : ℝ≥0∞)⁻¹ + (↑q : ℝ≥0∞)⁻¹ = (↑r : ℝ≥0∞)⁻¹

Tactic:
exact_mod_cast h.inv_add_inv_eq_inv

Premises used: NNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
⊢ (↑p : ℝ≥0∞).HolderConjugate (↑q : ℝ≥0∞) ↔ p.HolderConjugate q

Tactic:
holderTriple_coe_iff one_ne_zero

Premises used: ENNReal.holderTriple_coe_iff, one_ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)

Tactic:
simpa [holderTriple_iff, ofReal_inv_of_pos, h.pos, h.symm.pos, h.pos', ofReal_add, h.nonneg,
    h.symm.nonneg] using congr(ENNReal.ofReal $(h.inv_add_inv_eq_inv))

Premises used: ENNReal.holderTriple_iff, Real.HolderTriple.pos, Real.HolderTriple.symm, ENNReal.ofReal_inv_of_pos, ENNReal.ofReal_add, Real.HolderTriple.pos', Real.HolderTriple.nonneg
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)

Tactic:
simpa using Real.HolderTriple.ennrealOfReal h

Premises used: Real.HolderTriple.ennrealOfReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
⊢ 0 < p.toReal

Tactic:
have hp := h.pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
⊢ 0 < q.toReal

Tactic:
have hq := h.symm.pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ 0 < r.toReal

Tactic:
have hr := h.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
⊢ 0 < p ∧ p < ∞

Tactic:
rw [toReal_pos_iff] at hp hq hr

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
hp₁ : 0 < p ∧ p < ∞
⊢ 0 < q ∧ q < ∞

Tactic:
rw [toReal_pos_iff] at hp hq hr

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
hp₁ : 0 < p ∧ p < ∞
hq₁ : 0 < q ∧ q < ∞
⊢ 0 < r ∧ r < ∞

Tactic:
rw [toReal_pos_iff] at hp hq hr

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
hr : 0 < r ∧ r < ∞
⊢ p.HolderTriple q r

Tactic:
simpa [hp.2.ne, hq.2.ne, hr.2.ne] using h.ennrealOfReal

Premises used: And.right, Real.HolderTriple.ennrealOfReal, LT.lt.ne
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r

Tactic:
⟨of_toReal, fun h ↦ ⟨?_, hp, hq⟩⟩

Premises used: Real.HolderTriple.mk, Iff.intro, ENNReal.HolderTriple.of_toReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
refine : ∀ (h : p.HolderTriple q r), p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹
⊢ p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r

Tactic:
refine ⟨of_toReal, fun h ↦ ⟨?_, hp, hq⟩⟩
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
h : p.HolderTriple q r
⊢ 0 < p ∧ p < ∞

Tactic:
rw [toReal_pos_iff] at hp hq

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
h : p.HolderTriple q r
hp₁ : 0 < p ∧ p < ∞
⊢ 0 < q ∧ q < ∞

Tactic:
rw [toReal_pos_iff] at hp hq

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
h : p.HolderTriple q r
hp₁ : 0 < p ∧ p < ∞
hq₁ : 0 < q ∧ q < ∞
⊢ p.HolderTriple q r

Tactic:
rw [toReal_pos_iff] at hp hq

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p ∧ p < ∞
hq : 0 < q ∧ q < ∞
h : p.HolderTriple q r
⊢ p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹

Tactic:
simpa [toReal_add, Finiteness.inv_ne_top, hp.1.ne', hq.1.ne']
    using congr(ENNReal.toReal $(h.inv_add_inv_eq_inv))

Premises used: ENNReal.toReal_add, LT.lt.ne', And.left, ENNReal.Finiteness.inv_ne_top
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
inst : p.HolderTriple q r
⊢ p.toReal.HolderTriple q.toReal r.toReal

Tactic:
toReal_iff r hp hq |>.mpr ‹_›

Premises used: Iff.mpr, ENNReal.HolderTriple.toReal_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
h : p.toNNReal.HolderTriple q.toNNReal r.toNNReal
⊢ p.toReal.HolderTriple q.toReal r.toReal

Tactic:
simpa only [coe_toNNReal_eq_toReal] using h.coe

Premises used: ENNReal.coe_toNNReal_eq_toReal, NNReal.HolderTriple.coe
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
simp_rw : p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r
⊢ p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r

Tactic:
simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]

Premises used: ENNReal.coe_toNNReal_eq_toReal, NNReal.holderTriple_coe_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
apply : 0 < p.toReal
apply₁ : 0 < q.toReal
⊢ p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r

Tactic:
apply toReal_iff r ?_ ?_

Premises used: ENNReal.HolderTriple.toReal_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 0 < p.toReal

Tactic:
simpa [← coe_toNNReal_eq_toReal]

Premises used: ENNReal.coe_toNNReal_eq_toReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 0 < q.toReal

Tactic:
simpa [← coe_toNNReal_eq_toReal]

Premises used: ENNReal.coe_toNNReal_eq_toReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
inst : p.HolderTriple q r
⊢ p.toNNReal.HolderTriple q.toNNReal r.toNNReal

Tactic:
toNNReal_iff r hp hq |>.mpr ‹_›

Premises used: Iff.mpr, ENNReal.HolderTriple.toNNReal_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.toReal.HolderConjugate q.toReal
⊢ p.toReal.HolderTriple q.toReal 1

Tactic:
rw [Real.HolderConjugate] at h

Premises used: Real.HolderConjugate
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal 1
⊢ p.HolderConjugate q

Tactic:
HolderTriple.of_toReal (toReal_one ▸ h)

Premises used: ENNReal.toReal_one, Eq.rec, ENNReal.HolderTriple.of_toReal, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal 1
⊢ p.HolderConjugate q

Tactic:
exact HolderTriple.of_toReal (toReal_one ▸ h)

Premises used: ENNReal.HolderTriple.of_toReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
⊢ p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q

Tactic:
⟨of_toReal, fun h ↦ ?_⟩

Premises used: ENNReal.HolderConjugate.of_toReal, Iff.intro