awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
simp [edist_eq_sum h, ENNReal.zero_rpow_of_pos h, ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, PiLp.edist_eq_sum, inv_pos
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
inl : ∀ (f g : PiLp 0 β), edist f g = edist g f
inr : ∀ (f g : PiLp ∞ β), edist f g = edist g f
inr₁ : ∀ (h : 0 < p.toReal), edist f g = edist g f
⊢ edist f g = edist g f

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_card, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, PiLp.edist_eq_card
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ∞ β
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_iSup, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, PiLp.edist_eq_iSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_sum h, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, PiLp.edist_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → Dist (α i)
f g : PiLp 0 α
⊢ dist f g = (↑(Finset.card.{u_2} (α := ι) (Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯)) : ℝ)

Tactic:
if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → Dist (α i)
p : ℝ≥0∞
hp : 0 < p.toReal
f g : PiLp p α
⊢ dist f g = HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

Premises used: ENNReal.toReal_pos_iff, LT.lt.ne', And.right, And.left, Iff.mp, if_neg, Eq.trans, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → Dist (α i)
f g : PiLp ∞ α
⊢ dist f g = ⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)

Tactic:
rfl

Premises used: iSup, dite, rfl, ite
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → Norm (β i)
f : PiLp 0 β
⊢ ‖f‖ = (↑(Finset.card.{u_2} (α := ι) (Finite.toFinset (s := {i : ι | ‖f.ofLp i‖ ≠ 0}) ⋯)) : ℝ)

Tactic:
if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → Norm (β i)
f : PiLp ∞ β
⊢ ‖f‖ = ⨆ (i : ι), ‖f.ofLp i‖

Tactic:
rfl

Premises used: iSup, dite, rfl, ite
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → Norm (β i)
hp : 0 < p.toReal
f : PiLp p β
⊢ ‖f‖ = HPow.hPow (α := ℝ) (∑ i : ι, ‖f.ofLp i‖ ^ p.toReal) (1 / p.toReal)

Tactic:
let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

Premises used: ENNReal.toReal_pos_iff, LT.lt.ne', And.right, And.left, Iff.mp, if_neg, Eq.trans, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g h : PiLp p β
inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g h : PiLp ∞ β), edist f h ≤ edist f g + edist g h
inr : ∀ (hp : 1 ≤ p.toReal), edist f h ≤ edist f g + edist g h
⊢ edist f h ≤ edist f g + edist g h

Tactic:
rcases p.dichotomy with (rfl | hp)

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g h : PiLp ∞ β
inl :
  ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))
⊢ edist f h ≤ edist f g + edist g h

Tactic:
simp only [edist_eq_iSup]

Premises used: PiLp.edist_eq_iSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g h : PiLp ∞ β
inl :
  IsEmpty ι →
    ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
      HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))
inl₁ :
  Nonempty ι →
    ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
      HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))
⊢ ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g h : PiLp ∞ β
h_1 : IsEmpty ι
⊢ ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))

Tactic:
simp only [ciSup_of_empty, ENNReal.bot_eq_zero, add_zero, nonpos_iff_eq_zero]

Premises used: ENNReal.bot_eq_zero, ciSup_of_empty, add_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g h : PiLp ∞ β
h_1 : Nonempty ι
⊢ ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))

Tactic:
iSup_le fun i => (edist_triangle _ (g i) _).trans <| add_le_add
            (le_iSup (fun k => edist (f k) (g k)) i) (le_iSup (fun k => edist (g k) (h k)) i)

Premises used: add_le_add, le_iSup, iSup_le, LE.le.trans, EDist.edist, WithLp.ofLp, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g h : PiLp ∞ β
h_1 : Nonempty ι
⊢ ⨆ (i : ι), edist (f.ofLp i) (h.ofLp i) ≤
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) (⨆ (i : ι), edist (g.ofLp i) (h.ofLp i))

Tactic:
refine
        iSup_le fun i => (edist_triangle _ (g i) _).trans <| add_le_add
            (le_iSup (fun k => edist (f k) (g k)) i) (le_iSup (fun k => edist (g k) (h k)) i)

Premises used: add_le_add, le_iSup, iSup_le, LE.le.trans, EDist.edist, WithLp.ofLp, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
inr :
  HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (f.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal) +
      HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (g.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal)
⊢ edist f h ≤ edist f g + edist g h

Tactic:
simp only [edist_eq_sum (zero_lt_one.trans_le hp)]

Premises used: PiLp.edist_eq_sum, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      edist (f.ofLp i) (h.ofLp i) ≤ edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (f.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, (edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)) ^ p.toReal)
      (1 / p.toReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ edist (f.ofLp i) (h.ofLp i) ≤ edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)

Tactic:
apply edist_triangle

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, (edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)) ^ p.toReal)
      (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal) +
      HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (g.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
ENNReal.Lp_add_le _ _ _ hp

Premises used: ENNReal.Lp_add_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
edist :
  HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (f.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, (EDist.edist (f.ofLp i) (g.ofLp i) + EDist.edist (g.ofLp i) (h.ofLp i)) ^ p.toReal)
      (1 / p.toReal)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (f.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal) +
      HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (g.ofLp i) (h.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
calc
        (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
            (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          apply edist_triangle
        _ ≤
            (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
              (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
          ENNReal.Lp_add_le _ _ _ hp

Premises used: Finset.univ, HDiv.hDiv, ENNReal.Lp_add_le, ENNReal.toReal, HPow.hPow, HAdd.hAdd, EDist.edist, OfNat.ofNat, WithLp.ofLp, Finset.sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
intro : ∀ (val : Fintype ι), Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞
⊢ Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
intro :
  ∀ (M : { r : ℝ // 0 ≤ r }) (hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) ⋯ ≤ M),
    Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞
⊢ Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)

Premises used: Finite.exists_le, dist_nonneg, Subtype.mk, Dist.dist, WithLp.ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
M : { r : ℝ // 0 ≤ r }
hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) ⋯ ≤ M
⊢ Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞

Tactic:
ne_of_lt ((iSup_le fun i => ?_).trans_lt (@ENNReal.coe_lt_top M))

Premises used: iSup_le, LE.le.trans_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
M : { r : ℝ // 0 ≤ r }
hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) ⋯ ≤ M
intro : ∀ (i : ι), edist (f.ofLp i) (g.ofLp i) ≤ (↑M : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞

Tactic:
refine ne_of_lt ((iSup_le fun i => ?_).trans_lt (@ENNReal.coe_lt_top M))

Premises used: iSup_le, LE.le.trans_lt, ne_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
M : { r : ℝ // 0 ≤ r }
hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) ⋯ ≤ M
i : ι
intro : (↑(NNReal.mk (dist (f.ofLp i) (g.ofLp i)) ⋯) : ℝ≥0∞) ≤ (↑M : ℝ≥0∞)
⊢ edist (f.ofLp i) (g.ofLp i) ≤ (↑M : ℝ≥0∞)

Tactic:
simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]

Premises used: dist_nonneg, ENNReal.ofReal_eq_coe_nnreal, EDist.edist, PseudoMetricSpace.edist_dist
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
M : { r : ℝ // 0 ≤ r }
hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) ⋯ ≤ M
i : ι
⊢ (↑(NNReal.mk (dist (f.ofLp i) (g.ofLp i)) ⋯) : ℝ≥0∞) ≤ (↑M : ℝ≥0∞)

Tactic:
mod_cast hM i

Premises used: cast, ENNReal.coe_le_coe._simp_1, Eq.symm
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
M : { r : ℝ // 0 ≤ r }
hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) ⋯ ≤ M
i : ι
⊢ (↑(NNReal.mk (dist (f.ofLp i) (g.ofLp i)) ⋯) : ℝ≥0∞) ≤ (↑M : ℝ≥0∞)

Tactic:
exact mod_cast hM i
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : PiLp ∞ α), 0 ≤ dist f g
inr : ∀ (h : 1 ≤ p.toReal), 0 ≤ dist f g
⊢ 0 ≤ dist f g

Tactic:
rcases p.dichotomy with (rfl | h)

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
Real.iSup_nonneg fun i ↦ dist_nonneg

Premises used: dist_nonneg, Real.iSup_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
exact Real.iSup_nonneg fun i ↦ dist_nonneg

Premises used: dist_nonneg, Real.iSup_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
pos : ∀ (hp : p = 0), LE.le (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
pos₁ : ∀ (hp : ¬p = 0), p = ∞ → LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
neg : ∀ (hp : ¬p = 0), ¬p = ∞ → 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)
⊢ 0 ≤
    if p = 0 then (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
    else
      if p = ∞ then ⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)
      else HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
split_ifs with hp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : p = 0
linarith :
  LT.lt (α := ℝ) (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ) 0 →
    HSub.hSub (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ) +
        HSub.hSub (α := ℝ) (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ) 0 =
      0
⊢ LE.le (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : ¬p = 0
h_1 : p = ∞
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
Real.iSup_nonneg fun i ↦ dist_nonneg

Premises used: dist_nonneg, Real.iSup_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : ¬p = 0
h_1 : p = ∞
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
exact Real.iSup_nonneg fun i ↦ dist_nonneg

Premises used: dist_nonneg, Real.iSup_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : ¬p = 0
h_1 : ¬p = ∞
i : ι
⊢ 0 i ≤ dist (f.ofLp i) (g.ofLp i) ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : ¬p = 0
h_1 : ¬p = ∞
⊢ 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
exact rpow_nonneg (Fintype.sum_nonneg fun i ↦ by positivity) (1 / p.toReal)

Premises used: HDiv.hDiv, Fintype.sum_nonneg, ENNReal.toReal, Real.rpow_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
inl : ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : PiLp ∞ α), edist f g = ENNReal.ofReal (dist f g)
inr : ∀ (h : 1 ≤ p.toReal), edist f g = ENNReal.ofReal (dist f g)
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
rcases p.dichotomy with (rfl | h)

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
inl : ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
rw [edist_eq_iSup, dist_eq_iSup]

Premises used: PiLp.dist_eq_iSup, PiLp.edist_eq_iSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
inl : IsEmpty ι → ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
inl₁ : Nonempty ι → ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : IsEmpty ι
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : Nonempty ι
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : Nonempty ι
inl :
  ∀ (r : ℝ≥0),
    ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) ≤ (↑r : ℝ≥0∞) ↔
      ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)) ≤ (↑r : ℝ≥0∞)
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))

Tactic:
refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : Nonempty ι
r : ℝ≥0
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ dist (f.ofLp i) (g.ofLp i))

Tactic:
have : BddAbove <| .range fun i ↦ dist (f i) (g i) := Finite.bddAbove_range _
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : Nonempty ι
r : ℝ≥0
this : BddAbove (α := ℝ) (range fun (i : ι) ↦ dist (f.ofLp i) (g.ofLp i))
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) ≤ (↑r : ℝ≥0∞) ↔
    ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)) ≤ (↑r : ℝ≥0∞)

Tactic:
simp [ciSup_le_iff this]

Premises used: ciSup_le_iff
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
rw : p ≠ ∞
⊢ 0 < p.toReal

Tactic:
rw [ENNReal.toReal_pos_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff_ne_top