awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
Y : Type u_2
inst_1 : MeasurableSpace Y
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : BorelSpace X
inst_5 : BorelSpace Y
inst_6 : SecondCountableTopologyEither X Y
rw : Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
rw₁ :
  Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (MeasurableSpace.comap ofLp (borel (X × Y)))
rw₂ :
  Eq (α := MeasurableSpace (WithLp p (X × Y))) (MeasurableSpace.comap ofLp inferInstance)
    (MeasurableSpace.comap ofLp (borel (X × Y)))
rw₃ rw₄ :
  Eq (α := MeasurableSpace (WithLp p (X × Y))) (MeasurableSpace.comap ofLp inferInstance)
    (MeasurableSpace.comap ofLp (borel (X × Y)))
⊢ Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))

Tactic:
rw [instProdTopologicalSpace, borel_comap, measurableSpace,
      BorelSpace.measurable_eq (α := X × Y)]

Premises used: WithLp.instProdTopologicalSpace, BorelSpace.measurable_eq, WithLp.measurableSpace, borel_comap
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
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)))
rw₃ 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))

Tactic:
rw [topologicalSpace, borel_comap, WithLp.measurableSpace,
      BorelSpace.measurable_eq (α := Π i, X i)]

Premises used: BorelSpace.measurable_eq, PiLp.topologicalSpace, WithLp.measurableSpace, borel_comap
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
⊢ Eq (α := (a : X) → WithLp p X) (⇑(MeasurableEquiv.toLp p X) : (a : X) → WithLp p X) (WithLp.toLp p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
⊢ Eq (α := (a : WithLp p X) → X) (⇑(symm (MeasurableEquiv.toLp p X)) : (a : WithLp p X) → X) WithLp.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
x : X
⊢ (MeasurableEquiv.toLp p X : (a : X) → WithLp p X) x = WithLp.toLp p x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
x : WithLp p X
⊢ (symm (MeasurableEquiv.toLp p X) : (a : WithLp p X) → X) x = x.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_1
α : ι → Type u_2
x y : PiLp p α
h : ∀ (i : ι), x.ofLp i = y.ofLp i
⊢ x = y

Tactic:
ofLp_injective p <| funext h

Premises used: WithLp.ofLp_injective, funext
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → SeminormedAddCommGroup (β i)
i : ι
⊢ Eq.{u_4 + 1} (α := β i) (ofLp (p := p) 0 i) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
i : ι
⊢ (x + y).ofLp i = x.ofLp i + y.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
i : ι
⊢ (x - y).ofLp i = x.ofLp i - y.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
β : ι → Type u_4
inst : Semiring 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
x : PiLp p β
i : ι
⊢ (c • x).ofLp i = c • x.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ (-x).ofLp i = -x.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
x : (i : ι) → α i
i : ι
⊢ (toLp p x).ofLp i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ (single p (β := β) i a).ofLp = Pi.single (M := β) i a

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ toLp p (Pi.single (M := β) i a) = single p (β := β) i a

Tactic:
rfl

Premises used: PiLp.single, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
rw₁ rw₂ : a = a
⊢ (single p (β := β) i a).ofLp i = a

Tactic:
rw [ofLp_single, Pi.single_eq_same]

Premises used: PiLp.ofLp_single, Pi.single_eq_same
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
rw₁ rw₂ : Eq.{u_4 + 1} (α := β i') 0 0
⊢ (single p (β := β) i a).ofLp i' = 0

Tactic:
rw [ofLp_single, Pi.single_eq_of_ne h]

Premises used: PiLp.ofLp_single, Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
rw₁ rw₂ : Eq.{u_4 + 1} (α := β i') 0 0
⊢ (single p (β := β) i a).ofLp i' = 0

Tactic:
rw [ofLp_single, Pi.single_eq_of_ne' h]

Premises used: PiLp.ofLp_single, Pi.single_eq_of_ne'
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := (fun (x : ι) ↦ 𝕜) j) (Pi.single (M := fun (x : ι) ↦ 𝕜) i a j : 𝕜)
    (Pi.single (M := fun (a : ι) ↦ 𝕜) i a j : 𝕜)
⊢ ofLp (single p (β := 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]

Premises used: PiLp.toLp_single, Pi.single_apply, PiLp.toLp_apply
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a : β i
⊢ single p (β := β) i a = 0 ↔ a = 0

Tactic:
(toLp_eq_zero p).trans Pi.single_eq_zero_iff

Premises used: PiLp.single, Iff.trans, WithLp.toLp_eq_zero, Pi.single_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
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)
⊢ single p (β := β) i (a + b) = single p (β := β) i a + single p (β := β) i b

Tactic:
simp_rw [← toLp_single, Pi.single_add, toLp_add]

Premises used: PiLp.toLp_single, Pi.single_add, WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
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)
⊢ single p (β := β) i (a - b) = single p (β := β) i a - single p (β := β) i b

Tactic:
simp_rw [← toLp_single, Pi.single_sub, toLp_sub]

Premises used: PiLp.toLp_single, Pi.single_sub, WithLp.toLp_sub
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
simp_rw₁ : toLp p (-Pi.single (M := β) i a) = -toLp p (Pi.single (M := β) i a)
⊢ single p (β := β) i (-a) = -single p (β := β) i a

Tactic:
simp_rw [← toLp_single, Pi.single_neg, toLp_neg]

Premises used: PiLp.toLp_single, WithLp.toLp_neg, Pi.single_neg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
this :
  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))))
⊢ 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)))

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
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))))
⊢ 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)))

Tactic:
suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2)) by
    simpa
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
⊢ InjOn (β := WithLp p ((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))
    (↑(Submodule.span 𝕜
          (range 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))))) :
      Set ((j : η) → Ms j))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
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)))
⊢ 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:
rw [LinearMap.linearIndependent_iff_of_injOn _ (by simp)]

Premises used: LinearMap.linearIndependent_iff_of_injOn
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 := (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:
Pi.linearIndependent_single v hs

Premises used: Pi.linearIndependent_single
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 := (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:
exact Pi.linearIndependent_single v hs

Premises used: Pi.linearIndependent_single
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
this :
  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)
⊢ LinearIndependent 𝕜 (M := PiLp.{u_2, u_1} p fun (i : ι) ↦ 𝕜) fun (i : ι) ↦ single p (β := fun (i : ι) ↦ 𝕜) i 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
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)
⊢ LinearIndependent 𝕜 (M := PiLp.{u_2, u_1} p fun (i : ι) ↦ 𝕜) fun (i : ι) ↦ single p (β := fun (i : ι) ↦ 𝕜) i 1

Tactic:
suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun i : ι ↦ Pi.single i (1 : 𝕜)) by
    simpa
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
⊢ InjOn (β := WithLp p ((j : ι) → 𝕜))
    (⇑((↑(LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : ι) → 𝕜))) : ((j : ι) → 𝕜) →ₗ[𝕜] WithLp p ((j : ι) → 𝕜)) :
          ((j : ι) → 𝕜) →ₗ[𝕜] WithLp p ((j : ι) → 𝕜)) :
      (a : (j : ι) → 𝕜) → WithLp p ((j : ι) → 𝕜))
    (↑(Submodule.span 𝕜 (range fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) : Set ((j : ι) → 𝕜))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
rw : LinearIndependent 𝕜 (M := (j : ι) → 𝕜) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1
⊢ 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:
rw [LinearMap.linearIndependent_iff_of_injOn _ (by simp)]

Premises used: LinearMap.linearIndependent_iff_of_injOn
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
⊢ LinearIndependent 𝕜 (M := (j : ι) → 𝕜) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1

Tactic:
Pi.linearIndependent_single_one ι 𝕜

Premises used: Pi.linearIndependent_single_one
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : Ring 𝕜
⊢ LinearIndependent 𝕜 (M := (j : ι) → 𝕜) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ 𝕜) i 1

Tactic:
exact Pi.linearIndependent_single_one ι 𝕜

Premises used: Pi.linearIndependent_single_one
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
this :
  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))
⊢ LinearIndependent 𝕜 (M := PiLp.{u_2, u_5} p fun (i : ι) ↦ M) fun (i : ι) ↦ single p (β := fun (i : ι) ↦ M) i (v i)

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
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))
⊢ LinearIndependent 𝕜 (M := PiLp.{u_2, u_5} p fun (i : ι) ↦ M) fun (i : ι) ↦ single p (β := fun (i : ι) ↦ M) i (v i)

Tactic:
suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun i : ι ↦ Pi.single i (v i)) by
    simpa
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
⊢ InjOn (β := WithLp p ((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))
    (↑(Submodule.span 𝕜 (range fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i))) : Set ((j : ι) → M))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
rw : LinearIndependent 𝕜 (M := (j : ι) → M) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i)
⊢ 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:
rw [LinearMap.linearIndependent_iff_of_injOn _ (by simp)]

Premises used: LinearMap.linearIndependent_iff_of_injOn
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 := (j : ι) → M) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i)

Tactic:
Pi.linearIndependent_single_of_ne_zero hv

Premises used: Pi.linearIndependent_single_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 := (j : ι) → M) fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ M) i (v i)

Tactic:
exact Pi.linearIndependent_single_of_ne_zero hv

Premises used: Pi.linearIndependent_single_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → EDist (β i)
f g : PiLp 0 β
⊢ edist f g =
    (↑(Finset.card.{u_2} (α := ι) (Finite.toFinset (s := {i : ι | edist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯)) : ℝ≥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 : ι) → EDist (β i)
p : ℝ≥0∞
hp : 0 < p.toReal
f g : PiLp p β
⊢ edist f g = HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (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_4
inst : Fintype ι
inst_1 : (i : ι) → EDist (β i)
f g : PiLp ∞ β
⊢ edist f g = ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i)

Tactic:
rfl

Premises used: Set.Mem, iSup, setOf, Set.range, rfl, ite
-- 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 β
inl : ∀ (f : PiLp 0 β), edist f f = 0
inr : ∀ (f : PiLp ∞ β), edist f f = 0
inr₁ : ∀ (h : 0 < p.toReal), edist f f = 0
⊢ edist f f = 0

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 : PiLp 0 β
⊢ edist f f = 0

Tactic:
simp [edist_eq_card]

Premises used: 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 : PiLp ∞ β
⊢ edist f f = 0

Tactic:
simp [edist_eq_iSup]

Premises used: PiLp.edist_eq_iSup