awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have singleton : ∀ (a : α) (Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i),
  LT.lt (α := ℝ≥0∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, g i)
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)
Cleared hypotheses: hs, Hlt
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
singleton :
  ∀ (a : α) (Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i),
    LT.lt (α := ℝ≥0∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, g i)
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have cons : ∀ (a : α) (s : Finset α) (h : a ∉ s),
  s.Nonempty →
    ∀ (ih : ∀ (Hlt : ∀ i ∈ s, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i))
      (Hlt : ∀ i ∈ cons a s h, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ cons a s h, f i) (∑ i ∈ cons a s h, g i)
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)
Cleared hypotheses: hs, Hlt
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : LE.le (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
⊢ ∃ i ∈ s, f i ≤ g i
have contrapose! : ∀ (Hle : ∀ (i : α) (_ : i ∈ s), g i < f i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s, g i) (∑ i ∈ s, f i)
Tactic: contrapose! Hle
Cleared hypotheses: Hle
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
have cons : ∀ (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 ≠ ∞),
  Eq (α := ℝ≥0∞) (∏ i ∈ Finset.cons i s hi, f i)⁻¹ (∏ i ∈ Finset.cons i s hi, (f i)⁻¹)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih => ?_
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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 ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ Finset.cons i s hi, f i)⁻¹ (∏ i ∈ Finset.cons i s hi, (f i)⁻¹)
have cons : (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹
Tactic: simp only [Finset.prod_cons, ← ih (hf.mono <| by simp)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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)⁻¹
have cons : ∀ (hi₀ : f i = 0) (j : ι) (hj : j ∈ s), f j ≠ ∞
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 ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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 ≠ ∞
⊢ (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹
have cons₁ : ∀ (hi₀ : f i = ∞) (j : ι) (hj : j ∈ s), f j ≠ 0
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 ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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)
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ Finset.cons a s ha, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ Finset.cons a s ha, f a i)
have cons : HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i
Tactic: simp_rw [Finset.sum_cons, ihs]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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
have 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
Tactic: refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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 + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
have cons : f a i ≤ f a k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
have cons₁ : ∀ i ∈ s, f i j ≤ f i k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
have empty : Eq (α := ℝ≥0∞) (∑ a ∈ ∅, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
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)
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
have 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)
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
r' : ℝ≥0∞
hr' : p.HolderTriple q r'
⊢ r = r'
have rw : r⁻¹ = r'⁻¹
Tactic: rw [← inv_inj, inv_eq p q r, inv_eq p q r']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
r' : ℝ≥0∞
hr' : p.HolderTriple q r'
rw : r⁻¹ = r'⁻¹
⊢ r = r'
have rw₁ : p⁻¹ + q⁻¹ = r'⁻¹
Tactic: rw [← inv_inj, inv_eq p q r, inv_eq p q r']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
r' : ℝ≥0∞
hr' : p.HolderTriple q r'
rw : r⁻¹ = r'⁻¹
rw₁ : p⁻¹ + q⁻¹ = r'⁻¹
⊢ r = r'
have rw₂ : p⁻¹ + q⁻¹ = p⁻¹ + q⁻¹
Tactic: rw [← inv_inj, inv_eq p q r, inv_eq p q r']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr : r ≠ 0
⊢ r⁻¹ - q⁻¹ = p⁻¹
have apply : q⁻¹ < ∞
Tactic: apply ENNReal.sub_eq_of_eq_add (ne_of_lt ?_) (inv_eq p q r)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr : r ≠ 0
⊢ q⁻¹ < ∞
have q₁ : r⁻¹ < ∞
Tactic: calc
    q⁻¹ ≤ r⁻¹ := HolderTriple.inv_le_inv q p r
    _ < ∞ := by simpa using pos_iff_ne_zero.mpr hr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hq : q ≠ 0
⊢ r⁻¹ - q⁻¹ = p⁻¹
have inl : ∀ [p.HolderTriple q 0], 0⁻¹ - q⁻¹ = p⁻¹
Tactic: obtain (rfl | hr) := eq_zero_or_pos r
Cleared hypotheses: r, inst
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hq : q ≠ 0
inl : ∀ [p.HolderTriple q 0], 0⁻¹ - q⁻¹ = p⁻¹
⊢ r⁻¹ - q⁻¹ = p⁻¹
have inr : ∀ (hr : 0 < r), r⁻¹ - q⁻¹ = p⁻¹
Tactic: obtain (rfl | hr) := eq_zero_or_pos r
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹
have inl : p = 0
Tactic: suffices p = 0 by simpa [this]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
⊢ p = 0
have inl : ∀ (hp : p ≠ 0), False
Tactic: by_contra! hp
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (hypothesis)
Goal:
p q : ℝ≥0∞
hq : q ≠ 0
inst : p.HolderTriple q 0
hp : p ≠ 0
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst_1 : p.HolderTriple q' r
⊢ q = q'
have rw : q⁻¹ = q'⁻¹
Tactic: rw [← inv_inj, ← inv_sub_inv_eq_inv q p hr, ← inv_sub_inv_eq_inv q' p hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst_1 : p.HolderTriple q' r
rw : q⁻¹ = q'⁻¹
⊢ q = q'
have rw₁ : r⁻¹ - p⁻¹ = q'⁻¹
Tactic: rw [← inv_inj, ← inv_sub_inv_eq_inv q p hr, ← inv_sub_inv_eq_inv q' p hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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'⁻¹
⊢ q = q'
have rw₂ : r⁻¹ - p⁻¹ = r⁻¹ - p⁻¹
Tactic: rw [← inv_inj, ← inv_sub_inv_eq_inv q p hr, ← inv_sub_inv_eq_inv q' p hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr₀ : r ≠ 0
hr : r ≠ ∞
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw : r / p + (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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q r : ℝ≥0∞
inst : p.HolderTriple q r
hr₀ : r ≠ 0
hr : r ≠ ∞
rw : r / p + (q / r)⁻¹ = 1⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₁ : r / p + r / q = 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₂ : r * p⁻¹ + r / q = 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₃ : r * p⁻¹ + r * q⁻¹ = 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₄ : r * (p⁻¹ + q⁻¹) = 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₅ : r * 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₆ : Eq (α := ℝ≥0∞) 1 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
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⁻¹
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹
have rw₇ : Eq (α := ℝ≥0∞) 1 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1⁻¹
have rw : Eq (α := ℝ≥0∞) 1 1⁻¹
Tactic: rw [← two_mul, ENNReal.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
rw : Eq (α := ℝ≥0∞) 1 1⁻¹
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1⁻¹
have h0 : Ne (α := ℝ≥0∞) 2 0
Tactic: rw [← two_mul, ENNReal.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
rw : Eq (α := ℝ≥0∞) 1 1⁻¹
h0 : Ne (α := ℝ≥0∞) 2 0
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1⁻¹
have ht : Ne (α := ℝ≥0∞) 2 ∞
Tactic: rw [← two_mul, ENNReal.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ p = ∞ ↔ q = 1
have mp : p = ∞ → q = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
mp : p = ∞ → q = 1
⊢ p = ∞ ↔ q = 1
have mpr : q = 1 → p = ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
q : ℝ≥0∞
inst : HolderConjugate ∞ q
⊢ q = 1
have mp : (HSub.hSub (α := ℝ≥0∞) 1 ∞⁻¹)⁻¹ = 1
Tactic: rw [← inv_inv q, ← one_sub_inv ∞ q]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p : ℝ≥0∞
inst : p.HolderConjugate 1
⊢ p = ∞
have mpr : (HSub.hSub (α := ℝ≥0∞) 1 1⁻¹)⁻¹ = ∞
Tactic: rw [← inv_inv p, ← one_sub_inv 1 p]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ p ≠ ∞ ↔ q ≠ 1
have rw : p = ∞ ↔ q = 1
Tactic: rw [not_iff_not, eq_top_iff_eq_one p q]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
rw : p = ∞ ↔ q = 1
⊢ p ≠ ∞ ↔ q ≠ 1
have rw₁ : q = 1 ↔ q = 1
Tactic: rw [not_iff_not, eq_top_iff_eq_one p q]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
⊢ p < ∞ ↔ 1 < q
have rw : 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q
Tactic: rw [lt_top_iff_ne_top, ne_top_iff_ne_one _ q, ne_comm, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (hypothesis)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
⊢ (p - 1) * p⁻¹ = q⁻¹
have this : p ≠ 0
Tactic: have := pos p q |>.ne'
-- Lean 4 proof step from Mathlib.Data.ENNReal.Holder (goal)
Goal:
p q : ℝ≥0∞
inst : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ (p - 1) * p⁻¹ = q⁻¹
have rw : 1 - 1 * p⁻¹ = q⁻¹
Tactic: rw [ENNReal.sub_mul (by simp_all), ENNReal.mul_inv_cancel this (by lia)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ a / b = b⁻¹ * a
have rw : a * b⁻¹ = b⁻¹ * a
Tactic: rw [div_eq_mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : a * b⁻¹ = b⁻¹ * a
⊢ a / b = b⁻¹ * a
have rw₁ : b⁻¹ * a = b⁻¹ * a
Tactic: rw [div_eq_mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r b : ℝ≥0
hb : 1 ≤ (↑r : ℝ≥0∞) * (↑b : ℝ≥0∞)
⊢ r⁻¹ ≤ b
have h : 1 ≤ r * b
Tactic: apply NNReal.inv_le_of_le_mul
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r b : ℝ≥0
hb : 1 ≤ (↑r : ℝ≥0∞) * (↑b : ℝ≥0∞)
⊢ 1 ≤ r * b
have h : ∀ (hb : 1 ≤ (↑(r * b) : ℝ≥0∞)), 1 ≤ r * b
Tactic: rwa [← coe_mul, ← coe_one, coe_le_coe] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r b : ℝ≥0
hb : 1 ≤ (↑r : ℝ≥0∞) * (↑b : ℝ≥0∞)
h : ∀ (hb : 1 ≤ (↑(r * b) : ℝ≥0∞)), 1 ≤ r * b
⊢ 1 ≤ r * b
have h₁ : ∀ (hb : (↑1 : ℝ≥0∞) ≤ (↑(r * b) : ℝ≥0∞)), 1 ≤ r * b
Tactic: rwa [← coe_mul, ← coe_one, coe_le_coe] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ 1 ≤ r * b
have h₂ : ∀ (hb : 1 ≤ r * b), 1 ≤ r * b
Tactic: rwa [← coe_mul, ← coe_one, coe_le_coe] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r : ℝ≥0
hr : r ≠ 0
⊢ 1 ≤ (↑r : ℝ≥0∞) * (↑r⁻¹ : ℝ≥0∞)
have rw : 1 ≤ (↑(r * r⁻¹) : ℝ≥0∞)
Tactic: rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r : ℝ≥0
hr : r ≠ 0
rw : 1 ≤ (↑(r * r⁻¹) : ℝ≥0∞)
⊢ 1 ≤ (↑r : ℝ≥0∞) * (↑r⁻¹ : ℝ≥0∞)
have rw₁ : 1 ≤ (↑1 : ℝ≥0∞)
Tactic: rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r : ℝ≥0
hr : r ≠ 0
rw : 1 ≤ (↑(r * r⁻¹) : ℝ≥0∞)
rw₁ : 1 ≤ (↑1 : ℝ≥0∞)
⊢ 1 ≤ (↑r : ℝ≥0∞) * (↑r⁻¹ : ℝ≥0∞)
have rw₂ : LE.le (α := ℝ≥0∞) 1 1
Tactic: rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
⊢ (↑2⁻¹ : ℝ≥0∞) = 2⁻¹
have rw : (↑2 : ℝ≥0∞)⁻¹ = 2⁻¹
Tactic: rw [coe_inv _root_.two_ne_zero, coe_two]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
rw : (↑2 : ℝ≥0∞)⁻¹ = 2⁻¹
⊢ (↑2⁻¹ : ℝ≥0∞) = 2⁻¹
have rw₁ : Eq (α := ℝ≥0∞) 2⁻¹ 2⁻¹
Tactic: rw [coe_inv _root_.two_ne_zero, coe_two]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r p : ℝ≥0
hr : r ≠ 0
⊢ (↑(p / r) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
have rw : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r p : ℝ≥0
hr : r ≠ 0
rw : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
⊢ (↑(p / r) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
have rw₁ : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r p : ℝ≥0
hr : r ≠ 0
rw : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
rw₁ : (↑(p * r⁻¹) : ℝ≥0∞) = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
⊢ (↑(p / r) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
have rw₂ : (↑p : ℝ≥0∞) * (↑r⁻¹ : ℝ≥0∞) = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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∞)⁻¹
⊢ (↑(p / r) : ℝ≥0∞) = (↑p : ℝ≥0∞) / (↑r : ℝ≥0∞)
have rw₃ : (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹ = (↑p : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
n : ℕ
⊢ ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)
have inl : ((↑0 : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑0 : ℝ≥0∞)⁻¹ ^ (n + 1)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
n : ℕ
inl : ((↑0 : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑0 : ℝ≥0∞)⁻¹ ^ (n + 1)
⊢ ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)
have inr : ∀ (ha : a ≠ 0), ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)
have this : a ^ (n + 1) ≠ 0
Tactic: have := pow_ne_zero (n + 1) ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)
have inr : (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
have inr : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹
Tactic: rw [inv_pow]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ∞
⊢ a * a⁻¹ = 1
have lift : ∀ (a : ℝ≥0) (h0 : (↑a : ℝ≥0∞) ≠ 0), (↑a : ℝ≥0∞) * (↑a : ℝ≥0∞)⁻¹ = 1
Tactic: lift a to ℝ≥0 using ht
Cleared hypotheses: a, h0, ht
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a : ℝ≥0
h0 : (↑a : ℝ≥0∞) ≠ 0
⊢ (↑a : ℝ≥0∞) * (↑a : ℝ≥0∞)⁻¹ = 1
have h0₁ : ¬a = 0
Tactic: norm_cast at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
h0 : ¬a = 0
⊢ (↑a : ℝ≥0∞) * (↑a : ℝ≥0∞)⁻¹ = 1
have norm_cast : a * a⁻¹ = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a⁻¹ * (a * b) = b
have inl : ∀ (ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0), 0⁻¹ * (0 * b) = b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, ha₀, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
inl : ∀ (ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0), 0⁻¹ * (0 * b) = b
⊢ a⁻¹ * (a * b) = b
have inr : ∀ (ha₀ : a ≠ 0), a⁻¹ * (a * b) = b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀_1 : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
⊢ a⁻¹ * (a * b) = b
have inr : ∀ (ha₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0) (ha : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), ∞⁻¹ * (∞ * b) = b
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a, ha₀_1, ha, ha₀