awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X_1 : Type u_1
inst : MeasurableSpace X_1
ι : Type u_2
X : ι → Type u_3
inst_1 : Countable ι
inst_2 : (i : ι) → MeasurableSpace (X i)
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (X i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (X i)
rw : Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i)) (borel (PiLp p X))
rw₁ :
  Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i))
    (MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i)))
rw₂ :
  Eq (α := MeasurableSpace (PiLp p X)) (MeasurableSpace.comap WithLp.ofLp inferInstance)
    (MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i)))
⊢ Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i)) (borel (PiLp p X))
have rw₃ : Eq (α := MeasurableSpace (PiLp p X)) (MeasurableSpace.comap WithLp.ofLp inferInstance)
  (MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i)))
Tactic: rw [topologicalSpace, borel_comap, WithLp.measurableSpace,
      BorelSpace.measurable_eq (α := Π i, X i)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ (single p (β := β) i a).ofLp i = a
have rw : Pi.single (M := β) i a i = a
Tactic: rw [ofLp_single, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i : ι
a : β i
rw : Pi.single (M := β) i a i = a
⊢ (single p (β := β) i a).ofLp i = a
have rw₁ : a = a
Tactic: rw [ofLp_single, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ (single p (β := β) i a).ofLp i' = 0
have rw : Pi.single (M := β) i a i' = 0
Tactic: rw [ofLp_single, Pi.single_eq_of_ne h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
rw : Pi.single (M := β) i a i' = 0
⊢ (single p (β := β) i a).ofLp i' = 0
have rw₁ : Eq.{u_4 + 1} (α := β i') 0 0
Tactic: rw [ofLp_single, Pi.single_eq_of_ne h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ (single p (β := β) i a).ofLp i' = 0
have rw : Pi.single (M := β) i a i' = 0
Tactic: rw [ofLp_single, Pi.single_eq_of_ne' h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
rw : Pi.single (M := β) i a i' = 0
⊢ (single p (β := β) i a).ofLp i' = 0
have rw₁ : Eq.{u_4 + 1} (α := β i') 0 0
Tactic: rw [ofLp_single, Pi.single_eq_of_ne' h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Zero 𝕜
i : ι
a : 𝕜
j : ι
⊢ ofLp (single p (β := fun (x : ι) ↦ 𝕜) i a) j = if j = i then a else 0
have rw : ofLp (toLp p (Pi.single (M := fun (x : ι) ↦ 𝕜) i a)) j = if j = i then a else 0
Tactic: rw [← toLp_single, PiLp.toLp_apply, ← Pi.single_apply i a j]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Zero 𝕜
i : ι
a : 𝕜
j : ι
rw : ofLp (toLp p (Pi.single (M := fun (x : ι) ↦ 𝕜) i a)) j = if j = i then a else 0
⊢ ofLp (single p (β := fun (x : ι) ↦ 𝕜) i a) j = if j = i then a else 0
have rw₁ : Pi.single (M := fun (x : ι) ↦ 𝕜) i a j = if j = i then a else 0
Tactic: rw [← toLp_single, PiLp.toLp_apply, ← Pi.single_apply i a j]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Zero 𝕜
i : ι
a : 𝕜
j : ι
rw : ofLp (toLp p (Pi.single (M := fun (x : ι) ↦ 𝕜) i a)) j = if j = i then a else 0
rw₁ : Pi.single (M := fun (x : ι) ↦ 𝕜) i a j = if j = i then a else 0
⊢ ofLp (single p (β := fun (x : ι) ↦ 𝕜) i a) j = if j = i then a else 0
have rw₂ : Eq.{u_1 + 1} (α := (fun (x : ι) ↦ 𝕜) j) (Pi.single (M := fun (x : ι) ↦ 𝕜) i a j : 𝕜)
  (Pi.single (M := fun (a : ι) ↦ 𝕜) i a j : 𝕜)
Tactic: rw [← toLp_single, PiLp.toLp_apply, ← Pi.single_apply i a j]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
⊢ single p (β := β) i (a + b) = single p (β := β) i a + single p (β := β) i b
have simp_rw : toLp p (Pi.single (M := β) i (a + b)) = toLp p (Pi.single (M := β) i a) + toLp p (Pi.single (M := β) i b)
Tactic: simp_rw [← toLp_single, Pi.single_add, toLp_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
simp_rw : toLp p (Pi.single (M := β) i (a + b)) = toLp p (Pi.single (M := β) i a) + toLp p (Pi.single (M := β) i b)
⊢ single p (β := β) i (a + b) = single p (β := β) i a + single p (β := β) i b
have simp_rw₁ : toLp p (Pi.single (M := β) i a + Pi.single (M := β) i b) =
  toLp p (Pi.single (M := β) i a) + toLp p (Pi.single (M := β) i b)
Tactic: simp_rw [← toLp_single, Pi.single_add, toLp_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
⊢ single p (β := β) i (a - b) = single p (β := β) i a - single p (β := β) i b
have simp_rw : toLp p (Pi.single (M := β) i (a - b)) = toLp p (Pi.single (M := β) i a) - toLp p (Pi.single (M := β) i b)
Tactic: simp_rw [← toLp_single, Pi.single_sub, toLp_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
simp_rw : toLp p (Pi.single (M := β) i (a - b)) = toLp p (Pi.single (M := β) i a) - toLp p (Pi.single (M := β) i b)
⊢ single p (β := β) i (a - b) = single p (β := β) i a - single p (β := β) i b
have simp_rw₁ : toLp p (Pi.single (M := β) i a - Pi.single (M := β) i b) =
  toLp p (Pi.single (M := β) i a) - toLp p (Pi.single (M := β) i b)
Tactic: simp_rw [← toLp_single, Pi.single_sub, toLp_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a : β i
⊢ single p (β := β) i (-a) = -single p (β := β) i a
have simp_rw : toLp p (Pi.single (M := β) i (-a)) = -toLp p (Pi.single (M := β) i a)
Tactic: simp_rw [← toLp_single, Pi.single_neg, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a : β i
simp_rw : toLp p (Pi.single (M := β) i (-a)) = -toLp p (Pi.single (M := β) i a)
⊢ single p (β := β) i (-a) = -single p (β := β) i a
have simp_rw₁ : toLp p (-Pi.single (M := β) i a) = -toLp p (Pi.single (M := β) i a)
Tactic: simp_rw [← toLp_single, Pi.single_neg, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
inst : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst_1 : (i : η) → AddCommGroup (Ms i)
inst_2 : (i : η) → Module.{u_1, u_7} 𝕜 (Ms i)
inst_3 : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
⊢ LinearIndependent 𝕜 (M := PiLp p Ms) fun (ji : (j : η) × ιs j) ↦
    single p (β := Ms) (ji.fst (β := fun (j : η) ↦ ιs j))
      (v (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
have suffices : LinearIndependent (ι := (j : η) × ιs j) 𝕜 (M := WithLp p ((j : η) → Ms j))
  (Function.comp (β := (j : η) → Ms j)
    (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : η) → Ms j))) :
            ((j : η) → Ms j) →ₗ[𝕜] WithLp p ((j : η) → Ms j)) :
          ((j : η) → Ms j) →ₗ[𝕜] WithLp p ((j : η) → Ms j)) :
      (a : (j : η) → Ms j) → WithLp p ((j : η) → Ms j))
    fun (ji : (j : η) × ιs j) ↦
    Pi.single (M := Ms) (ji.fst (β := fun (j : η) ↦ ιs j))
      (v (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))))
Tactic: suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2)) by
    simpa
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
inst : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst_1 : (i : η) → AddCommGroup (Ms i)
inst_2 : (i : η) → Module.{u_1, u_7} 𝕜 (Ms i)
inst_3 : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
⊢ LinearIndependent (ι := (j : η) × ιs j) 𝕜 (M := WithLp p ((j : η) → Ms j))
    (Function.comp (β := (j : η) → Ms j)
      (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : η) → Ms j))) :
              ((j : η) → Ms j) →ₗ[𝕜] WithLp p ((j : η) → Ms j)) :
            ((j : η) → Ms j) →ₗ[𝕜] WithLp p ((j : η) → Ms j)) :
        (a : (j : η) → Ms j) → WithLp p ((j : η) → Ms j))
      fun (ji : (j : η) × ιs j) ↦
      Pi.single (M := Ms) (ji.fst (β := fun (j : η) ↦ ιs j))
        (v (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))))
have rw : LinearIndependent 𝕜 (M := (j : η) → Ms j) fun (ji : (j : η) × ιs j) ↦
  Pi.single (M := Ms) (ji.fst (β := fun (j : η) ↦ ιs j))
    (v (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
Tactic: rw [LinearMap.linearIndependent_iff_of_injOn _ (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
⊢ LinearIndependent 𝕜 (M := PiLp.{u_2, u_1} p fun (i : ι) ↦ 𝕜) fun (i : ι) ↦ single p (β := fun (i : ι) ↦ 𝕜) i 1
have suffices : LinearIndependent (ι := ι) 𝕜 (M := WithLp p ((j : ι) → 𝕜))
  (Function.comp (β := (j : ι) → 𝕜)
    (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : ι) → 𝕜))) : ((j : ι) → 𝕜) →ₗ[𝕜] WithLp p ((j : ι) → 𝕜)) :
          ((j : ι) → 𝕜) →ₗ[𝕜] WithLp p ((j : ι) → 𝕜)) :
      (a : (j : ι) → 𝕜) → WithLp p ((j : ι) → 𝕜))
    fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)
Tactic: suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun i : ι ↦ Pi.single i (1 : 𝕜)) by
    simpa
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
⊢ LinearIndependent (ι := ι) 𝕜 (M := WithLp p ((j : ι) → 𝕜))
    (Function.comp (β := (j : ι) → 𝕜)
      (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : ι) → 𝕜))) : ((j : ι) → 𝕜) →ₗ[𝕜] WithLp p ((j : ι) → 𝕜)) :
            ((j : ι) → 𝕜) →ₗ[𝕜] WithLp p ((j : ι) → 𝕜)) :
        (a : (j : ι) → 𝕜) → WithLp p ((j : ι) → 𝕜))
      fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)
have rw : LinearIndependent 𝕜 (M := (j : ι) → 𝕜) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1
Tactic: rw [LinearMap.linearIndependent_iff_of_injOn _ (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
inst_2 : IsDomain 𝕜
M : Type u_5
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
inst_5 : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent 𝕜 (M := PiLp.{u_2, u_5} p fun (i : ι) ↦ M) fun (i : ι) ↦ single p (β := fun (i : ι) ↦ M) i (v i)
have suffices : LinearIndependent (ι := ι) 𝕜 (M := WithLp p ((j : ι) → M))
  (Function.comp (β := (j : ι) → M)
    (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : ι) → M))) : ((j : ι) → M) →ₗ[𝕜] WithLp p ((j : ι) → M)) :
          ((j : ι) → M) →ₗ[𝕜] WithLp p ((j : ι) → M)) :
      (a : (j : ι) → M) → WithLp p ((j : ι) → M))
    fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i))
Tactic: suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun i : ι ↦ Pi.single i (v i)) by
    simpa
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
inst_2 : IsDomain 𝕜
M : Type u_5
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
inst_5 : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent (ι := ι) 𝕜 (M := WithLp p ((j : ι) → M))
    (Function.comp (β := (j : ι) → M)
      (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : ι) → M))) : ((j : ι) → M) →ₗ[𝕜] WithLp p ((j : ι) → M)) :
            ((j : ι) → M) →ₗ[𝕜] WithLp p ((j : ι) → M)) :
        (a : (j : ι) → M) → WithLp p ((j : ι) → M))
      fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i))
have rw : LinearIndependent 𝕜 (M := (j : ι) → M) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i)
Tactic: rw [LinearMap.linearIndependent_iff_of_injOn _ (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
⊢ edist f f = 0
have inl : ∀ (f : PiLp 0 β), edist f f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
inl : ∀ (f : PiLp 0 β), edist f f = 0
⊢ edist f f = 0
have inr : ∀ (f : PiLp ∞ β), edist f f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
inl : ∀ (f : PiLp 0 β), edist f f = 0
inr : ∀ (f : PiLp ∞ β), edist f f = 0
⊢ edist f f = 0
have inr₁ : ∀ (h : 0 < p.toReal), edist f f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
⊢ edist f g = edist g f
have inl : ∀ (f g : PiLp 0 β), edist f g = edist g f
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ edist f g = edist g f
have inr : ∀ (f g : PiLp ∞ β), edist f g = edist g f
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ edist f g = edist g f
have inr₁ : ∀ (h : 0 < p.toReal), edist f g = edist g f
Tactic: rcases p.trichotomy with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 β
⊢ edist f h ≤ edist f g + edist g h
have inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g h : PiLp ∞ β), edist f h ≤ edist f g + edist g h
Tactic: rcases p.dichotomy with (rfl | hp)
Cleared hypotheses: p, inst, f, g, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ edist f h ≤ edist f g + edist g h
have inr : ∀ (hp : 1 ≤ p.toReal), edist f h ≤ edist f g + edist g h
Tactic: rcases p.dichotomy with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ∞ β
⊢ edist f h ≤ edist f g + edist g h
have 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))
Tactic: simp only [edist_eq_iSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 ∞ β
⊢ ⨆ (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))
have 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))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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))
⊢ ⨆ (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))
have 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))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 f h ≤ edist f g + edist g h
have 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)
Tactic: simp only [edist_eq_sum (zero_lt_one.trans_le hp)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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) (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)
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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) (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)
have edist : 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: 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
⊢ Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞
have intro : ∀ (val : Fintype ι), Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_5
inst : Finite ι
α : ι → Type u_6
inst_1 : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
val : Fintype ι
⊢ Ne (α := ℝ≥0∞) (⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)) ∞
have intro : ∀ (M : { r : ℝ // 0 ≤ r }) (hM : ∀ (i : ι), Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (dist (f.ofLp i) (g.ofLp i)) sorry ≤ M),
  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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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)) ∞
have intro : ∀ (i : ι), edist (f.ofLp i) (g.ofLp i) ≤ (↑M : ℝ≥0∞)
Tactic: refine ne_of_lt ((iSup_le fun i => ?_).trans_lt (@ENNReal.coe_lt_top M))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 : ι
⊢ edist (f.ofLp i) (g.ofLp i) ≤ (↑M : ℝ≥0∞)
have intro : (↑(NNReal.mk (dist (f.ofLp i) (g.ofLp i)) sorry) : ℝ≥0∞) ≤ (↑M : ℝ≥0∞)
Tactic: simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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 α
⊢ 0 ≤ dist f g
have inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : PiLp ∞ α), 0 ≤ dist f g
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, inst, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 0 ≤ dist f g
have inr : ∀ (h : 1 ≤ p.toReal), 0 ≤ dist f g
Tactic: rcases p.dichotomy with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
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
⊢ 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)
have pos : ∀ (hp : p = 0), LE.le (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) sorry).card : ℝ)
Tactic: split_ifs with hp