awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
cons : (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ Finset.cons i s hi, f i)⁻¹ (∏ i ∈ Finset.cons i s hi, (f i)⁻¹)

Tactic:
simp only [Finset.prod_cons, ← ih (hf.mono <| by simp)]

Premises used: Set.Pairwise.mono, Finset.prod_cons
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹

Tactic:
ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)

Premises used: Iff.mpr, setOf, Finset.prod_ne_zero_iff, ENNReal.prod_ne_top, not_or_of_imp, ENNReal.mul_inv
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
cons : ∀ (hi₀ : f i = 0) (j : ι) (hj : j ∈ s), f j ≠ ∞
cons₁ : ∀ (hi₀ : f i = ∞) (j : ι) (hj : j ∈ s), f j ≠ 0
⊢ (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹

Tactic:
refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, ENNReal.prod_ne_top, not_or_of_imp, ENNReal.mul_inv
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ i ∈ (↑(Finset.cons i s hi) : Set ι)

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ j ∈ (↑(Finset.cons i s hi) : Set ι)

Tactic:
simp [hj]
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ f j ≠ ∞

Tactic:
exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀

Premises used: Iff.mpr, Ne.symm, imp_iff_not_or, ne_of_mem_of_not_mem
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ j ∈ (↑(Finset.cons i s hi) : Set ι)

Tactic:
simp [hj]
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ i ∈ (↑(Finset.cons i s hi) : Set ι)

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ f j ≠ 0

Tactic:
exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

Premises used: Iff.mpr, imp_iff_not_or, ne_of_mem_of_not_mem, Or.symm
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : (↑s : Set ι).Pairwise fun (i j : ι) ↦ g i ≠ 0 ∨ g j ≠ ∞
⊢ ∏ i ∈ s, f i / g i = HDiv.hDiv (α := ℝ≥0∞) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
simp only [div_eq_mul_inv, prod_inv_distrib hg, ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, ENNReal.prod_inv_distrib, div_eq_mul_inv
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ ∞
⊢ (↑s : Set ι).Pairwise fun (i j : ι) ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
grind [Set.Pairwise]

Premises used: Set.Pairwise
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ 0
⊢ (↑s : Set ι).Pairwise fun (i j : ι) ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
grind [Set.Pairwise]

Premises used: Set.Pairwise
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ ∅, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ ∅, f a i)

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
cons : HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ Finset.cons a s ha, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ Finset.cons a s ha, f a i)

Tactic:
simp_rw [Finset.sum_cons, ihs]

Premises used: Finset.sum_cons
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i

Tactic:
iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_

Premises used: ENNReal.iSup_add_iSup, Exists.imp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
cons : ∀ (i j k : ι) (hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k), f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i

Tactic:
refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_

Premises used: ENNReal.iSup_add_iSup, Exists.imp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
cons : f a i ≤ f a k
cons₁ : ∀ i ∈ s, f i j ≤ f i k
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k

Tactic:
gcongr
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i ≤ f a k

Tactic:
(hk a).1

Premises used: And.left
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
i_1 : α
h : i_1 ∈ s
⊢ f i_1 j ≤ f i_1 k

Tactic:
(hk _).2

Premises used: And.right
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i ≤ f a k

Tactic:
exacts [(hk a).1, (hk _).2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
empty : Eq (α := ℝ≥0∞) (∑ a ∈ ∅, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ ∅, f a i)
cons :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ihs : Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)),
    Eq (α := ℝ≥0∞) (∑ a ∈ Finset.cons a s ha, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ Finset.cons a s ha, f a i)
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ihs =>
    simp_rw [Finset.sum_cons, ihs]
    refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_
    gcongr
    exacts [(hk a).1, (hk _).2]

Premises used: Finset.sum_cons, ENNReal.iSup_add_iSup, Exists.imp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder ι
inst_1 : IsDirectedOrder ι
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ s, iSup (f a)) (⨆ (n : ι), ∑ a ∈ s, f a n)

Tactic:
finsetSum_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ a ↦ ⟨hf a hi, hf a hj⟩

Premises used: Exists.imp, exists_ge_ge, ENNReal.finsetSum_iSup
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
⊢ p.HolderConjugate q ↔ p⁻¹ + q⁻¹ = 1

Tactic:
simp [holderTriple_iff]

Premises used: ENNReal.holderTriple_iff
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p : ℝ≥0∞
⊢ p⁻¹ + ∞⁻¹ = p⁻¹

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p : ℝ≥0∞
⊢ p⁻¹ + 0⁻¹ = 0⁻¹

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
⊢ r⁻¹ = p⁻¹ + q⁻¹

Tactic:
(inv_add_inv_eq_inv ..).symm

Premises used: Eq.symm, ENNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
r' : ℝ≥0∞
hr' : p.HolderTriple q r'
rw : r⁻¹ = r'⁻¹
rw₁ : p⁻¹ + q⁻¹ = r'⁻¹
rw₂ rw₃ : p⁻¹ + q⁻¹ = p⁻¹ + q⁻¹
⊢ r = r'

Tactic:
rw [← inv_inj, inv_eq p q r, inv_eq p q r']

Premises used: inv_inj, ENNReal.HolderTriple.inv_eq
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
simpa using inv_add_inv_eq_inv ..

Premises used: ENNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
⊢ 1 / r = 1 / p + 1 / q

Tactic:
one_div_add_one_div p q r |>.symm

Premises used: Eq.symm, ENNReal.HolderTriple.one_div_add_one_div
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
simp [inv_add_inv_eq_inv p q r]

Premises used: ENNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
⊢ r ≤ p

Tactic:
simp [← ENNReal.inv_le_inv, ← @inv_inv_add_inv p q r, inv_inv]

Premises used: ENNReal.inv_le_inv, inv_inv, ENNReal.HolderTriple.inv_inv_add_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
⊢ p⁻¹ ≤ r⁻¹

Tactic:
simp [ENNReal.inv_le_inv, le p q r]

Premises used: ENNReal.inv_le_inv, ENNReal.HolderTriple.le
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr : r ≠ 0
apply : q⁻¹ < ∞
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
apply ENNReal.sub_eq_of_eq_add (ne_of_lt ?_) (inv_eq p q r)

Premises used: ENNReal.sub_eq_of_eq_add, ENNReal.HolderTriple.inv_eq, ne_of_lt
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr : r ≠ 0
⊢ q⁻¹ ≤ r⁻¹

Tactic:
HolderTriple.inv_le_inv q p r

Premises used: ENNReal.HolderTriple.inv_le_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr : r ≠ 0
⊢ r⁻¹ < ∞

Tactic:
simpa using pos_iff_ne_zero.mpr hr

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr : r ≠ 0
q₁ : r⁻¹ < ∞
⊢ q⁻¹ < ∞

Tactic:
calc
    q⁻¹ ≤ r⁻¹ := HolderTriple.inv_le_inv q p r
    _ < ∞ := by simpa using pos_iff_ne_zero.mpr hr

Premises used: ENNReal.HolderTriple.inv_le_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hq : q ≠ 0
inl : ∀ [p.HolderTriple q 0], 0⁻¹ - q⁻¹ = p⁻¹
inr : ∀ (hr : 0 < r), r⁻¹ - q⁻¹ = p⁻¹
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
obtain (rfl | hr) := eq_zero_or_pos r

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
this : p = 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
simpa [this]
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
inl : p = 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
suffices p = 0 by simpa [this]
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
inl : ∀ (hp : p ≠ 0), False
⊢ p = 0

Tactic:
by_contra! hp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
hp : p ≠ 0
⊢ p⁻¹ + q⁻¹ < HAdd.hAdd (α := ℝ≥0∞) ∞ ∞

Tactic:
simp [hp, hq, pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
hp : p ≠ 0
⊢ HAdd.hAdd (α := ℝ≥0∞) ∞ ∞ = ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
hp : p ≠ 0
⊢ LT.lt (α := ℝ≥0∞) 0⁻¹ ∞

Tactic:
have := calc
      0⁻¹ = p⁻¹ + q⁻¹ := inv_eq p q 0
      _ < ⊤ + ⊤ := by simp [hp, hq, pos_iff_ne_zero]
      _ = ⊤ := by simp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
hp : p ≠ 0
this : LT.lt (α := ℝ≥0∞) 0⁻¹ ∞
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hq : q ≠ 0
hr : 0 < r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
inv_sub_inv_eq_inv p q hr.ne'

Premises used: LT.lt.ne', ENNReal.HolderTriple.inv_sub_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hq : q ≠ 0
hr : 0 < r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
exact inv_sub_inv_eq_inv p q hr.ne'

Premises used: LT.lt.ne', ENNReal.HolderTriple.inv_sub_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst_1 : p.HolderTriple q' r
rw : q⁻¹ = q'⁻¹
rw₁ : r⁻¹ - p⁻¹ = q'⁻¹
rw₂ rw₃ : r⁻¹ - p⁻¹ = r⁻¹ - p⁻¹
⊢ q = q'

Tactic:
rw [← inv_inj, ← inv_sub_inv_eq_inv q p hr, ← inv_sub_inv_eq_inv q' p hr]

Premises used: inv_inj, ENNReal.HolderTriple.inv_sub_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr₀ : r ≠ 0
hr : r ≠ ∞
rw : r / p + (q / r)⁻¹ = 1⁻¹
rw₁ : r / p + r / q = 1⁻¹
rw₂ : r * p⁻¹ + r / q = 1⁻¹
rw₃ : r * p⁻¹ + r * q⁻¹ = 1⁻¹
rw₄ : r * (p⁻¹ + q⁻¹) = 1⁻¹
rw₅ : r * r⁻¹ = 1⁻¹
rw₆ : Eq (α := ℝ≥0∞) 1 1⁻¹
rw₇ rw₈ : Eq (α := ℝ≥0∞) 1 1
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹

Tactic:
rw [ENNReal.inv_div (.inl hr) (.inl hr₀), ENNReal.inv_div (.inl hr) (.inl hr₀), div_eq_mul_inv,
      div_eq_mul_inv, ← mul_add, inv_add_inv_eq_inv p q r, ENNReal.mul_inv_cancel hr₀ hr, inv_one]

Premises used: inv_one, div_eq_mul_inv, ENNReal.mul_inv_cancel, mul_add, Or.inl, ENNReal.inv_div, ENNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
hpq : p.HolderConjugate q
⊢ q.HolderConjugate p

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
rw : Eq (α := ℝ≥0∞) 1 1⁻¹
h0 : Ne (α := ℝ≥0∞) 2 0
ht : Ne (α := ℝ≥0∞) 2 ∞
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1⁻¹

Tactic:
rw [← two_mul, ENNReal.mul_inv_cancel]

Premises used: two_mul, ENNReal.mul_inv_cancel
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
⊢ Eq (α := ℝ≥0∞) 1 1⁻¹

Tactic:
norm_num
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
norm_num
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
norm_num
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
⊢ HolderConjugate 1 ∞

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ 1 ≤ p

Tactic:
HolderTriple.le p q 1

Premises used: ENNReal.HolderTriple.le, OfNat.ofNat
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ 0 < p

Tactic:
zero_lt_one.trans_le (one_le p q)

Premises used: ENNReal.HolderConjugate.one_le, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ p ≠ 0

Tactic:
pos p q |>.ne'

Premises used: LT.lt.ne', ENNReal.HolderConjugate.pos
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
@inv_one ℝ≥0∞ _ ▸ HolderTriple.inv_add_inv_eq_inv p q 1

Premises used: inv_one, Eq.rec, OfNat.ofNat, ENNReal.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ 1 - p⁻¹ = q⁻¹

Tactic:
@inv_one ℝ≥0∞ _ ▸ HolderTriple.inv_sub_inv_eq_inv q p one_ne_zero

Premises used: inv_one, Eq.rec, ENNReal.HolderTriple.inv_sub_inv_eq_inv, one_ne_zero
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
q' : ℝ≥0∞
hq' : p.HolderConjugate q'
⊢ q = q'

Tactic:
HolderTriple.unique_of_ne_zero p q q' one_ne_zero

Premises used: one_ne_zero, ENNReal.HolderTriple.unique_of_ne_zero
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
mp : p = ∞ → q = 1
mpr : q = 1 → p = ∞
⊢ p = ∞ ↔ q = 1

Tactic:
constructor
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
q : ℝ≥0∞
inst : HolderConjugate ∞ q
mp : (HSub.hSub (α := ℝ≥0∞) 1 ∞⁻¹)⁻¹ = 1
⊢ q = 1

Tactic:
rw [← inv_inv q, ← one_sub_inv ∞ q]

Premises used: ENNReal.HolderConjugate.one_sub_inv, inv_inv, Top.top
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
q : ℝ≥0∞
inst : HolderConjugate ∞ q
⊢ (HSub.hSub (α := ℝ≥0∞) 1 ∞⁻¹)⁻¹ = 1

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p : ℝ≥0∞
inst : p.HolderConjugate 1
mpr : (HSub.hSub (α := ℝ≥0∞) 1 1⁻¹)⁻¹ = ∞
⊢ p = ∞

Tactic:
rw [← inv_inv p, ← one_sub_inv 1 p]

Premises used: ENNReal.HolderConjugate.one_sub_inv, inv_inv, OfNat.ofNat
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p : ℝ≥0∞
inst : p.HolderConjugate 1
⊢ (HSub.hSub (α := ℝ≥0∞) 1 1⁻¹)⁻¹ = ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
rw : p = ∞ ↔ q = 1
rw₁ rw₂ : q = 1 ↔ q = 1
⊢ p ≠ ∞ ↔ q ≠ 1

Tactic:
rw [not_iff_not, eq_top_iff_eq_one p q]

Premises used: not_iff_not, ENNReal.HolderConjugate.eq_top_iff_eq_one
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
rw : 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q
⊢ p < ∞ ↔ 1 < q

Tactic:
rw [lt_top_iff_ne_top, ne_top_iff_ne_one _ q, ne_comm, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, lt_top_iff_ne_top, ne_comm, ENNReal.HolderConjugate.ne_top_iff_ne_one
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q

Tactic:
simp [one_le q p]

Premises used: ENNReal.HolderConjugate.one_le
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
⊢ p ≠ 0

Tactic:
have := pos p q |>.ne'
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ LT.lt (α := ℝ≥0∞) 0 1 → 1 < p → p⁻¹ ≠ ∞

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ p ≠ ∞

Tactic:
lia
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
rw : 1 - 1 * p⁻¹ = q⁻¹
⊢ (p - 1) * p⁻¹ = q⁻¹

Tactic:
rw [ENNReal.sub_mul (by simp_all), ENNReal.mul_inv_cancel this (by lia)]

Premises used: ENNReal.sub_mul, ENNReal.mul_inv_cancel
-- Module: Mathlib.Data.ENNReal.Holder
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ 1 - 1 * p⁻¹ = q⁻¹

Tactic:
simp [one_sub_inv p q]

Premises used: ENNReal.HolderConjugate.one_sub_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
rw : a * b⁻¹ = b⁻¹ * a
rw₁ rw₂ : b⁻¹ * a = b⁻¹ * a
⊢ a / b = b⁻¹ * a

Tactic:
rw [div_eq_mul_inv, mul_comm]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
⊢ a / b / c = a / c / b

Tactic:
simp only [div_eq_mul_inv, mul_right_comm]

Premises used: div_eq_mul_inv, mul_right_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ Eq (α := ℝ≥0∞) (sInf {b : ℝ≥0∞ | 1 ≤ 0 * b}) ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : 0 < a
⊢ Membership.mem (γ := Set ℝ≥0∞) {b : ℝ≥0∞ | 1 ≤ ∞ * b} a

Tactic:
simp [*, h.ne', top_mul]

Premises used: ENNReal.top_mul, LT.lt.ne'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r b : ℝ≥0
hb : 1 ≤ (↑r : ℝ≥0∞) * (↑b : ℝ≥0∞)
h : 1 ≤ r * b
⊢ r⁻¹ ≤ b

Tactic:
apply NNReal.inv_le_of_le_mul

Premises used: NNReal.inv_le_of_le_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r b : ℝ≥0
hb : 1 ≤ (↑r : ℝ≥0∞) * (↑b : ℝ≥0∞)
h : ∀ (hb : 1 ≤ (↑(r * b) : ℝ≥0∞)), 1 ≤ r * b
h₁ : ∀ (hb : (↑1 : ℝ≥0∞) ≤ (↑(r * b) : ℝ≥0∞)), 1 ≤ r * b
h₂ h₃ h₄ h₅ : ∀ (hb : 1 ≤ r * b), 1 ≤ r * b
⊢ 1 ≤ r * b

Tactic:
rwa [← coe_mul, ← coe_one, coe_le_coe] at hb

Premises used: ENNReal.coe_le_coe, ENNReal.coe_one, ENNReal.coe_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r : ℝ≥0
hr : r ≠ 0
rw : 1 ≤ (↑(r * r⁻¹) : ℝ≥0∞)
rw₁ : 1 ≤ (↑1 : ℝ≥0∞)
rw₂ rw₃ : LE.le (α := ℝ≥0∞) 1 1
⊢ 1 ≤ (↑r : ℝ≥0∞) * (↑r⁻¹ : ℝ≥0∞)

Tactic:
rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]

Premises used: mul_inv_cancel₀, ENNReal.coe_one, ENNReal.coe_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r : ℝ≥0
inst : NeZero r
⊢ (↑r⁻¹ : ℝ≥0∞) = (↑r : ℝ≥0∞)⁻¹

Tactic:
coe_inv (NeZero.ne r)

Premises used: ENNReal.coe_inv, NeZero.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
rw : (↑2 : ℝ≥0∞)⁻¹ = 2⁻¹
rw₁ rw₂ : Eq (α := ℝ≥0∞) 2⁻¹ 2⁻¹
⊢ (↑2⁻¹ : ℝ≥0∞) = 2⁻¹

Tactic:
rw [coe_inv _root_.two_ne_zero, coe_two]

Premises used: ENNReal.coe_inv, ENNReal.coe_two, two_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r p : ℝ≥0
hr : r ≠ 0
rw : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
rw₁ : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
rw₂ : (↑p : ℝ≥0∞) * (↑r⁻¹ : ℝ≥0∞) = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
rw₃ rw₄ : (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹ = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
⊢ (↑(p / r) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]

Premises used: ENNReal.coe_inv, div_eq_mul_inv, ENNReal.coe_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r p : ℝ≥0
inst : NeZero r
⊢ (↑(p / r) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)

Tactic:
coe_div (NeZero.ne r)

Premises used: ENNReal.coe_div, NeZero.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r p : ℝ≥0
⊢ (↑(p / r) : ℝ≥0∞) ≤ (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)

Tactic:
simpa only [div_eq_mul_inv, coe_mul] using _root_.mul_le_mul_right coe_inv_le _

Premises used: mul_le_mul_right, div_eq_mul_inv, ENNReal.coe_mul, ENNReal.coe_inv_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a ≠ 0
⊢ a / 0 = ∞

Tactic:
simp [div_eq_mul_inv, h]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ Eq (α := ℝ≥0∞) 1⁻¹ 1

Tactic:
simpa only [coe_inv one_ne_zero, coe_one] using coe_inj.2 inv_one

Premises used: Iff.mpr, ENNReal.coe_inv, inv_one, ENNReal.coe_inj, ENNReal.coe_one, one_ne_zero