awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
refine : ∀ (h : p.HolderConjugate q), p.toReal.HolderConjugate q.toReal
⊢ p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q

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

Tactic:
rw [toReal_pos_iff]

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

Tactic:
⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩

Premises used: Iff.mpr, And.intro, ENNReal.HolderConjugate.pos, ENNReal.HolderConjugate.lt_top_iff_one_lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
refine : 1 < p
⊢ 0 < q ∧ q < ∞

Tactic:
refine ⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
contrapose! : ∀ (hp : p ≤ 1), p.toReal ≤ 1
⊢ 1 < p

Tactic:
contrapose! hp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≤ 1
⊢ p.toReal ≤ 1

Tactic:
toReal_mono one_ne_top hp

Premises used: ENNReal.toReal, ENNReal.toReal_mono, NNReal.toReal, ENNReal.one_ne_top
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≤ 1
⊢ p.toReal ≤ 1

Tactic:
exact toReal_mono one_ne_top hp

Premises used: ENNReal.toReal_mono, ENNReal.one_ne_top
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ 0 < q.toReal

Tactic:
have hq : 0 < q.toReal := by
    rw [toReal_pos_iff]
    refine ⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩
    contrapose! hp
    exact toReal_mono one_ne_top hp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
hq : 0 < q.toReal
⊢ p.toReal.HolderConjugate q.toReal

Tactic:
simpa using HolderTriple.toReal 1 (zero_lt_one.trans hp) hq

Premises used: zero_lt_one, LT.lt.trans, OfNat.ofNat, ENNReal.HolderTriple.toReal
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
inst : p.HolderConjugate q
⊢ p.toReal.HolderConjugate q.toReal

Tactic:
toReal_iff hp |>.mpr ‹_›

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

Tactic:
simpa only [coe_toNNReal_eq_toReal] using h.coe

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

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 : ℝ≥0∞
hp : 1 < p.toNNReal
apply : 1 < p.toReal
⊢ p.toReal.HolderTriple q.toReal (↑1 : ℝ) ↔ p.HolderConjugate q

Tactic:
apply toReal_iff ?_

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

Tactic:
simpa [← coe_toNNReal_eq_toReal]

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

Tactic:
all_goals simpa [← coe_toNNReal_eq_toReal]

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

Tactic:
toNNReal_iff hp |>.mpr ‹_›

Premises used: Iff.mpr, ENNReal.HolderConjugate.toNNReal_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p ≠ 0

Tactic:
have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
rw : (1 + (p - 1)⁻¹)⁻¹ + p⁻¹ = 1⁻¹
⊢ p.HolderConjugate p.conjExponent

Tactic:
rw [HolderConjugate, holderTriple_iff, conjExponent, add_comm]

Premises used: ENNReal.holderTriple_iff, ENNReal.conjExponent, add_comm, ENNReal.HolderConjugate
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ AddLECancellable p⁻¹

Tactic:
simpa
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ p⁻¹ ≤ 1⁻¹

Tactic:
simpa
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
refine : (1 + (p - 1)⁻¹)⁻¹ = 1⁻¹ - p⁻¹
⊢ (1 + (p - 1)⁻¹)⁻¹ + p⁻¹ = 1⁻¹

Tactic:
refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (by simpa) (by simpa)).1 ?_

Premises used: AddLECancellable.eq_tsub_iff_add_eq_of_le, Iff.mp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
rw : 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
⊢ (1 + (p - 1)⁻¹)⁻¹ = 1⁻¹ - p⁻¹

Tactic:
rw [inv_eq_iff_eq_inv]

Premises used: inv_eq_iff_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
inl :
  ∀ (hp : LE.le (α := ℝ≥0∞) 1 1) (this : Ne (α := ℝ≥0∞) 1 0),
    1 + (HSub.hSub (α := ℝ≥0∞) 1 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ 1⁻¹)⁻¹
inr : ∀ (hp₁ : 1 < p), 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
obtain rfl | hp₁ := hp.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
hp : LE.le (α := ℝ≥0∞) 1 1
this : Ne (α := ℝ≥0∞) 1 0
⊢ 1 + (HSub.hSub (α := ℝ≥0∞) 1 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ 1⁻¹)⁻¹

Tactic:
simp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
inr :
  ∀ (hp : LE.le (α := ℝ≥0∞) 1 ∞) (this : Ne (α := ℝ≥0∞) ∞ 0) (hp₁ : LT.lt (α := ℝ≥0∞) 1 ∞),
    1 + (HSub.hSub (α := ℝ≥0∞) ∞ 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ ∞⁻¹)⁻¹
inr₁ : ∀ (hp : p ≠ ∞), 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
obtain rfl | hp := eq_or_ne p ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
hp : LE.le (α := ℝ≥0∞) 1 ∞
this : Ne (α := ℝ≥0∞) ∞ 0
hp₁ : LT.lt (α := ℝ≥0∞) 1 ∞
⊢ 1 + (HSub.hSub (α := ℝ≥0∞) ∞ 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ ∞⁻¹)⁻¹

Tactic:
simp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 + (p - 1)⁻¹ = (p - 1) / (p - 1) + 1 / (p - 1)
rw₁ : 1 + (p - 1)⁻¹ = 1 + 1 / (p - 1)
rw₂ rw₃ : 1 + (p - 1)⁻¹ = 1 + (p - 1)⁻¹
⊢ 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)

Tactic:
rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]

Premises used: ENNReal.sub_ne_top, LT.lt.ne', ENNReal.add_div, ENNReal.div_self, one_div, tsub_pos_of_lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 - p⁻¹ = 1⁻¹ - p⁻¹
h0 : p ≠ 0
ht : p ≠ ∞
rw₁ : LT.lt (α := ℝ≥0∞) 0 1 → 1 < p → p⁻¹ ≠ ∞
ha : p ≠ 0 ∨ (p - 1)⁻¹ ≠ ∞
hb : p ≠ ∞ ∨ (p - 1)⁻¹ ≠ 0
rw₂ : 1 ≤ p
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹

Tactic:
rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one]

Premises used: ENNReal.mul_sub, tsub_add_cancel_of_le, div_eq_mul_inv, inv_inv, ENNReal.inv_mul_cancel, mul_one, ENNReal.mul_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 - p⁻¹ = 1⁻¹ - p⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ ∞

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) 0 1 → 1 < p → p⁻¹ ≠ ∞

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ 0 ∨ (p - 1)⁻¹ ≠ ∞

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ ∞ ∨ (p - 1)⁻¹ ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 ≤ p

Tactic:
simp [*]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)
rw₁ : (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
calc
    1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
      rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
    _ = (1⁻¹ - p⁻¹)⁻¹ := by
      rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]

Premises used: HSub.hSub, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a b p_1 q r p : ℝ≥0∞
inst : Fact (1 ≤ p)
⊢ p.HolderConjugate p.conjExponent

Tactic:
.conjExponent Fact.out

Premises used: ENNReal.HolderConjugate.conjExponent, Fact.out
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
⊢ p.conjExponent = q

Tactic:
have : Fact (1 ≤ p) := ⟨one_le p q⟩
  unique p (conjExponent p) q

Premises used: ENNReal.HolderConjugate.unique, ENNReal.conjExponent, ENNReal.HolderConjugate.one_le, Fact.mk
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
⊢ q = 1 + (p - 1)⁻¹

Tactic:
conjExponent_eq.symm

Premises used: ENNReal.conjExponent, Eq.symm, ENNReal.HolderConjugate.conjExponent_eq
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
inl : ∀ [h : HolderConjugate ∞ q], ∞ * q = ∞ + q
inr : ∀ (hp : p ≠ ∞), p * q = p + q
⊢ p * q = p + q

Tactic:
obtain rfl | hp := eq_or_ne p ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
q : ℝ≥0∞
h : HolderConjugate ∞ q
⊢ ∞ * q = ∞ + q

Tactic:
simp [ne_zero q ∞]

Premises used: Top.top, ENNReal.HolderConjugate.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
inr : ∀ [h : p.HolderConjugate ∞], p * ∞ = p + ∞
inr₁ : ∀ (hq : q ≠ ∞), p * q = p + q
⊢ p * q = p + q

Tactic:
obtain rfl | hq := eq_or_ne q ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : p ≠ ∞
h : p.HolderConjugate ∞
⊢ p * ∞ = p + ∞

Tactic:
simp [ne_zero p ∞]

Premises used: Top.top, ENNReal.HolderConjugate.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
hq : q ≠ ∞
⊢ p * q = p + q

Tactic:
simpa [add_comm p, mul_add, add_mul, hp, hq, ne_zero p q, ne_zero q p, ENNReal.mul_inv_cancel,
    ENNReal.inv_mul_cancel_right] using congr(p * $((inv_add_inv_eq_one p q).symm) * q)

Premises used: add_mul, add_comm, ENNReal.mul_inv_cancel, ENNReal.HolderConjugate.inv_add_inv_eq_one, mul_add, Eq.symm, ENNReal.HolderConjugate.ne_zero, ENNReal.inv_mul_cancel_right
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
inl : ∀ [h : p.HolderConjugate ∞], p / ∞ = p - 1
inr : ∀ (hq : q ≠ ∞), p / q = p - 1
⊢ p / q = p - 1

Tactic:
obtain rfl | hq := eq_or_ne q ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
h : p.HolderConjugate ∞
inl : ∀ [h : HolderConjugate 1 ∞], HDiv.hDiv (α := ℝ≥0∞) 1 ∞ = HSub.hSub (α := ℝ≥0∞) 1 1
⊢ p / ∞ = p - 1

Tactic:
obtain rfl := unique ∞ p 1

Premises used: ENNReal.HolderConjugate.unique, Top.top, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
h : HolderConjugate 1 ∞
⊢ HDiv.hDiv (α := ℝ≥0∞) 1 ∞ = HSub.hSub (α := ℝ≥0∞) 1 1

Tactic:
simp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q = p - 1

Tactic:
ENNReal.eq_sub_of_add_eq one_ne_top ?_

Premises used: ENNReal.eq_sub_of_add_eq, ENNReal.one_ne_top
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + 1 = p
⊢ p / q = p - 1

Tactic:
refine ENNReal.eq_sub_of_add_eq one_ne_top ?_

Premises used: ENNReal.eq_sub_of_add_eq, ENNReal.one_ne_top
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + q / q = p
inr₁ : (p + q) / q = p
inr₂ : p * q / q = p
inr₃ : p * (q / q) = p
inr₄ : p * 1 = p
inr₅ inr₆ : p = p
⊢ p / q + 1 = p

Tactic:
rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]

Premises used: mul_div_assoc, ENNReal.add_div, ENNReal.div_self, ENNReal.HolderConjugate.mul_eq_add, mul_one, ENNReal.HolderConjugate.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a b : ℝ≥0∞
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
simpa [inv_inv] using hab

Premises used: inv_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ≥0∞
ha : a ≤ 1
⊢ a⁻¹.HolderConjugate (1 - a)⁻¹

Tactic:
.inv_inv <| add_tsub_cancel_of_le ha

Premises used: ENNReal.HolderConjugate.inv_inv, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ≥0∞
ha : 1 ≤ a
⊢ a.HolderConjugate (1 - a⁻¹)⁻¹

Tactic:
simpa using inv_one_sub_inv (ENNReal.inv_le_one.mpr ha)

Premises used: Iff.mpr, ENNReal.inv_le_one, ENNReal.HolderConjugate.inv_one_sub_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ≥0∞
ha : a ≤ 1
⊢ (1 - a)⁻¹.HolderConjugate a⁻¹

Tactic:
(inv_one_sub_inv ha).symm

Premises used: ENNReal.HolderConjugate.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
⊢ HAdd.hAdd (α := ℝ≥0∞) ∞⁻¹ 1⁻¹ = 1⁻¹

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

Tactic:
simp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0∞
⊢ p.HolderConjugate q ↔ q.HolderConjugate p

Tactic:
⟨(·.symm), (·.symm)⟩

Premises used: ENNReal.HolderConjugate.symm, Iff.intro
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.HolderConjugate (1 + (p - 1)⁻¹)

Tactic:
.conjExponent hp

Premises used: ENNReal.conjExponent, ENNReal.HolderConjugate.conjExponent
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.HolderConjugate (1 + (p - 1)⁻¹)

Tactic:
exact .conjExponent hp
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
⊢ map Nat.cast = toENNReal

Tactic:
rfl

Premises used: ENat.toENNReal, rfl
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
⊢ (↑⊤ : ℝ≥0∞) = ∞

Tactic:
rfl

Premises used: WithTop.map, ENat.toENNReal, ENat.map, rfl
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
n : ℕ
⊢ (↑(↑n : ℕ∞) : ℝ≥0∞) = (↑n : ℝ≥0∞)

Tactic:
rfl

Premises used: WithTop.map, ENat.toENNReal, WithTop.some, ENat.map, rfl
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : ℝ≥0∞) = OfNat.ofNat n

Tactic:
rfl

Premises used: WithTop.map, ENat.toENNReal, WithTop.some, ENat.map, rfl
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑m : ℝ≥0∞) = (↑n : ℝ≥0∞) ↔ m = n

Tactic:
toENNRealOrderEmbedding.eq_iff_eq

Premises used: WithTop.map, ENat.toENNReal, ENat.map, ENat.toENNRealOrderEmbedding, OrderEmbedding.eq_iff_eq
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
n : ℕ∞
⊢ (↑n : ℝ≥0∞) = ∞ ↔ n = ⊤

Tactic:
simp [← toENNReal_inj]

Premises used: ENat.toENNReal_inj
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
n : ℕ∞
⊢ (↑n : ℝ≥0∞) ≠ ∞ ↔ n ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑m : ℝ≥0∞) ≤ (↑n : ℝ≥0∞) ↔ m ≤ n

Tactic:
toENNRealOrderEmbedding.le_iff_le

Premises used: WithTop.map, ENat.toENNReal, ENat.map, ENat.toENNRealOrderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑m : ℝ≥0∞) < (↑n : ℝ≥0∞) ↔ m < n

Tactic:
toENNRealOrderEmbedding.lt_iff_lt

Premises used: WithTop.map, ENat.toENNReal, ENat.map, ENat.toENNRealOrderEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
n : ℕ∞
⊢ (↑n : ℝ≥0∞) < ∞ ↔ n < ⊤

Tactic:
simp [← toENNReal_lt]

Premises used: ENat.toENNReal_lt
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
⊢ Monotone toENNReal

Tactic:
toENNRealOrderEmbedding.monotone

Premises used: OrderEmbedding.monotone, WithTop.map, ENat.toENNReal, ENat.map, ENat.toENNRealOrderEmbedding
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
⊢ StrictMono toENNReal

Tactic:
toENNRealOrderEmbedding.strictMono

Premises used: WithTop.map, OrderEmbedding.strictMono, ENat.toENNReal, ENat.map, ENat.toENNRealOrderEmbedding
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
⊢ (↑0 : ℝ≥0∞) = 0

Tactic:
map_zero toENNRealRingHom

Premises used: WithTop.map, map_zero, ENat.toENNReal, ENat.map, ENat.toENNRealRingHom
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑(m + n) : ℝ≥0∞) = (↑m : ℝ≥0∞) + (↑n : ℝ≥0∞)

Tactic:
map_add toENNRealRingHom m n

Premises used: WithTop.map, map_add, ENat.toENNReal, ENat.map, ENat.toENNRealRingHom
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
⊢ (↑1 : ℝ≥0∞) = 1

Tactic:
map_one toENNRealRingHom

Premises used: WithTop.map, ENat.toENNReal, ENat.map, map_one, ENat.toENNRealRingHom
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑(m * n) : ℝ≥0∞) = (↑m : ℝ≥0∞) * (↑n : ℝ≥0∞)

Tactic:
map_mul toENNRealRingHom m n

Premises used: WithTop.map, ENat.toENNReal, ENat.map, map_mul, ENat.toENNRealRingHom
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
x : ℕ∞
n : ℕ
⊢ (↑(x ^ n) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ n

Tactic:
map_pow toENNRealRingHom x n

Premises used: WithTop.map, ENat.toENNReal, map_pow, ENat.map, ENat.toENNRealRingHom
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑(min m n) : ℝ≥0∞) = min (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)

Tactic:
toENNReal_mono.map_min

Premises used: ENat.toENNReal_mono, Monotone.map_min
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑(max m n) : ℝ≥0∞) = max (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)

Tactic:
toENNReal_mono.map_max

Premises used: Monotone.map_max, ENat.toENNReal_mono
-- Module: Mathlib.Data.Real.ENatENNReal
Goal:
m n : ℕ∞
⊢ (↑(m - n) : ℝ≥0∞) = (↑m : ℝ≥0∞) - (↑n : ℝ≥0∞)

Tactic:
WithTop.map_sub Nat.cast_tsub Nat.cast_zero m n

Premises used: WithTop.map_sub, ENat.toENNReal, ENat.map, ENNReal, Nat.cast_tsub
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
num : ℤ
n den : ℕ
hn : 0 < n
x : M
rw :
  HSMul.hSMul (α := ℤ) (↑n : ℤ) (HSMul.hSMul (β := M) num 1) < HSMul.hSMul (α := ℤ) (↑n : ℤ) (den • x) ↔
    HSMul.hSMul (β := M) num 1 < den • x
⊢ HSMul.hSMul (β := M) (num * (↑n : ℤ)) 1 < HMul.hMul (α := ℤ) (↑n : ℤ) (↑den : ℤ) • x ↔
    HSMul.hSMul (β := M) num 1 < den • x

Tactic:
rw [mul_comm num, mul_smul, mul_smul, natCast_zsmul x den]

Premises used: mul_comm, natCast_zsmul, SemigroupAction.mul_smul
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) (HSMul.hSMul (β := M) num 1) < HSMul.hSMul (α := ℤ) (↑n : ℤ) (den • x) ↔
    HSMul.hSMul (β := M) num 1 < den • x

Tactic:
⟨fun h ↦ lt_of_smul_lt_smul_left h (Int.natCast_nonneg n),
    fun h ↦ zsmul_lt_zsmul_right (Int.natCast_pos.mpr hn) h⟩

Premises used: Iff.mpr, zsmul_lt_zsmul_right, Iff.intro, lt_of_smul_lt_smul_left, Int.natCast_pos, Int.natCast_nonneg
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) (HSMul.hSMul (β := M) num 1) < HSMul.hSMul (α := ℤ) (↑n : ℤ) (den • x) ↔
    HSMul.hSMul (β := M) num 1 < den • x

Tactic:
exact ⟨fun h ↦ lt_of_smul_lt_smul_left h (Int.natCast_nonneg n),
    fun h ↦ zsmul_lt_zsmul_right (Int.natCast_pos.mpr hn) h⟩
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
⊢ HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x

Tactic:
simpa [mul_comm] using (mul_smul_one_lt_iff v.den_pos).mpr hu

Premises used: Iff.mpr, mul_smul_one_lt_iff, mul_comm, Rat.den_pos
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
⊢ HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x

Tactic:
have hu' : (u.num * v.den) • 1 < (u.den * v.den : ℤ) • x := by
    simpa [mul_comm] using (mul_smul_one_lt_iff v.den_pos).mpr hu
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)

Tactic:
(mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_

Premises used: mul_pos, mul_smul_one_lt_iff, Iff.mp, Rat.den_pos
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
refine :
  HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)

Tactic:
refine (mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_

Premises used: mul_pos, mul_smul_one_lt_iff, Iff.mp, Rat.den_pos
-- Module: Mathlib.Data.Real.Embedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
rwa :
  HSMul.hSMul (β := M) ((u + v).num * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
rwa₁ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
rwa₂ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    ((↑(u + v).den : ℤ) * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) • (x + y)
rwa₃ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) • (x + y)
rwa₄ rwa₅ rwa₆ rwa₇ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
⊢ HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)

Tactic:
rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]

Premises used: smul_assoc, mul_assoc, Rat.den, Nat.cast, Nat.cast_mul, HAdd.hAdd, mul_comm, smul_eq_mul