awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
Y : Ω → F
inst_8 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_9 : Fact (1 ≤ p)
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw (E := WithLp p (E × F)) (fun (ω : Ω) ↦ toLp p (X ω, Y ω)) P

Tactic:
hXY.map_equiv (WithLp.prodContinuousLinearEquiv p ℝ E F).symm

Premises used: ContinuousLinearEquiv.symm, Real, WithLp.prodContinuousLinearEquiv, setOf, ProbabilityTheory.HasGaussianLaw.map_equiv
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw X P

Tactic:
hXY.map_of_measurable (.fst ℝ E F) measurable_fst

Premises used: Real, ProbabilityTheory.HasGaussianLaw.map_of_measurable, ContinuousLinearMap.fst, measurable_fst
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
X : Ω → E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw Y P

Tactic:
hXY.map_of_measurable (.snd ℝ E F) measurable_snd

Premises used: Real, ContinuousLinearMap.snd, ProbabilityTheory.HasGaussianLaw.map_of_measurable, measurable_snd
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
Y : Ω → E
hXY : HasGaussianLaw.{u_1, u_2} (E := E × E) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw (X + Y) P

Tactic:
hXY.map (ContinuousLinearMap.fst ℝ E E + ContinuousLinearMap.snd ℝ E E)

Premises used: Real, ContinuousLinearMap.snd, ProbabilityTheory.HasGaussianLaw.map, HAdd.hAdd, ContinuousLinearMap.fst
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
Y : Ω → E
hXY : HasGaussianLaw.{u_1, u_2} (E := E × E) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ X ω + Y ω) P

Tactic:
hXY.add

Premises used: ProbabilityTheory.HasGaussianLaw.add
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
Y : Ω → E
hXY : HasGaussianLaw.{u_1, u_2} (E := E × E) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw (X - Y) P

Tactic:
hXY.map (ContinuousLinearMap.fst ℝ E E - ContinuousLinearMap.snd ℝ E E)

Premises used: Real, HSub.hSub, ContinuousLinearMap.snd, ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearMap.fst
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
Y : Ω → E
hXY : HasGaussianLaw.{u_1, u_2} (E := E × E) (fun (ω : Ω) ↦ (X ω, Y ω)) P
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ X ω - Y ω) P

Tactic:
hXY.sub

Premises used: ProbabilityTheory.HasGaussianLaw.sub
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
E : ι → Type u_5
inst : (i : ι) → NormedAddCommGroup (E i)
inst_1 : (i : ι) → NormedSpace ℝ (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), BorelSpace.{u_5} (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (E := (x : ι) → E x) (fun (ω : Ω) (x : ι) ↦ X x ω) P
i : ι
⊢ HasGaussianLaw (X i) P

Tactic:
hX.map_of_measurable (.proj i) (measurable_pi_apply i)

Premises used: measurable_pi_apply, ProbabilityTheory.HasGaussianLaw.map_of_measurable, ContinuousLinearMap.proj
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
E : ι → Type u_5
inst : (i : ι) → NormedAddCommGroup (E i)
inst_1 : (i : ι) → NormedSpace ℝ (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), BorelSpace.{u_5} (E i)
X : (i : ι) → Ω → E i
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_5 : Finite ι
hX : HasGaussianLaw (E := (x : ι) → E x) (fun (ω : Ω) (x : ι) ↦ X x ω) P
i j : ι
⊢ HasGaussianLaw.{u_1, u_5} (E := E i × E j) (fun (ω : Ω) ↦ (X i ω, X j ω)) P

Tactic:
letI := Fintype.ofFinite ι
  hX.map (.prod (.proj i) (.proj j))

Premises used: setOf, ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearMap.proj, Function.prod, ContinuousLinearMap.prod
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
E : ι → Type u_5
inst : (i : ι) → NormedAddCommGroup (E i)
inst_1 : (i : ι) → NormedSpace ℝ (E i)
inst_2 : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), BorelSpace.{u_5} (E i)
X : (i : ι) → Ω → E i
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_5 : Finite ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
hX : HasGaussianLaw (E := (x : ι) → E x) (fun (ω : Ω) (x : ι) ↦ X x ω) P
⊢ HasGaussianLaw (E := WithLp p ((x : ι) → E x)) (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P

Tactic:
have := Fintype.ofFinite ι
  hX.map_equiv (PiLp.continuousLinearEquiv p ℝ E).symm

Premises used: ContinuousLinearEquiv.symm, Real, Fintype.ofFinite, ProbabilityTheory.HasGaussianLaw.map_equiv, PiLp.continuousLinearEquiv
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
⊢ HasGaussianLaw.{u_1, u_6} (E := E)
    (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
      fun (ω : Ω) (x : ι) ↦ X x ω)
    P

Tactic:
hX.map (∑ i, .proj i)

Premises used: Finset.univ, ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearMap.proj, Finset.sum
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
h :
  Eq (α := Ω → E) (∑ i : ι, X i)
    (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
      fun (ω : Ω) (x : ι) ↦ X x ω)
⊢ HasGaussianLaw.{u_1, u_6} (E := E) (∑ i : ι, X i) P

Tactic:
convert! hX.map (∑ i, .proj i)

Premises used: Finset.univ, ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearMap.proj, Finset.sum
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
h :
  ∀ (x : Ω),
    Eq.{u_6 + 1} (α := E) ((∑ i : ι, X i) x)
      (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
        (fun (ω : Ω) (x : ι) ↦ X x ω) x)
⊢ Eq (α := Ω → E) (∑ i : ι, X i)
    (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
      fun (ω : Ω) (x : ι) ↦ X x ω)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
x : Ω
⊢ Eq.{u_6 + 1} (α := E) ((∑ i : ι, X i) x)
    (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
      (fun (ω : Ω) (x : ι) ↦ X x ω) x)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
⊢ HasGaussianLaw.{u_1, u_6} (E := E) (∑ i : ι, X i) P

Tactic:
hX.sum

Premises used: ProbabilityTheory.HasGaussianLaw.sum
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
h : ∀ (x : Ω), Eq.{u_6 + 1} (α := E) (∑ i : ι, X i x) ((∑ i : ι, X i) x)
⊢ HasGaussianLaw.{u_1, u_6} (E := E) (fun (ω : Ω) ↦ ∑ i : ι, X i ω) P

Tactic:
convert! hX.sum

Premises used: ProbabilityTheory.HasGaussianLaw.sum
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
x : Ω
⊢ Eq.{u_6 + 1} (α := E) (∑ i : ι, X i x) ((∑ i : ι, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y z : StrongDual ℝ ((i : ι) → E i)
⊢ (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
        (∑ i : ι,
            (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                    (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                  StrongDual ℝ (E i) →L[ℝ] ℝ) :
                (a : StrongDual ℝ (E i)) → ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
      (x + y) z =
    HAdd.hAdd (α := ℝ)
      ((fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
          (∑ i : ι,
              (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                    StrongDual ℝ (E i) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E i)) → ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ))
        x z)
      ((fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
          (∑ i : ι,
              (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                    StrongDual ℝ (E i) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E i)) → ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ))
        y z)

Tactic:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
c : ℝ
m n : StrongDual ℝ ((i : ι) → E i)
⊢ (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
        (∑ i : ι,
            (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                    (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                  StrongDual ℝ (E i) →L[ℝ] ℝ) :
                (a : StrongDual ℝ (E i)) → ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
      (c • m) n =
    HSMul.hSMul (β := ℝ) c
      ((fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
          (∑ i : ι,
              (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                    StrongDual ℝ (E i) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E i)) → ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ))
        m n)

Tactic:
simp [mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y z : StrongDual ℝ ((i : ι) → E i)
⊢ (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
        (∑ i : ι,
            (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                    (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                  StrongDual ℝ (E i) →L[ℝ] ℝ) :
                (a : StrongDual ℝ (E i)) → ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
      x (y + z) =
    HAdd.hAdd (α := ℝ)
      ((fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
          (∑ i : ι,
              (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                    StrongDual ℝ (E i) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E i)) → ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ))
        x y)
      ((fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
          (∑ i : ι,
              (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                    StrongDual ℝ (E i) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E i)) → ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ))
        x z)

Tactic:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
c : ℝ
m n : StrongDual ℝ ((i : ι) → E i)
⊢ (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
        (∑ i : ι,
            (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                    (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                  StrongDual ℝ (E i) →L[ℝ] ℝ) :
                (a : StrongDual ℝ (E i)) → ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
      m (c • n) =
    HSMul.hSMul (β := ℝ) c
      ((fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
          (∑ i : ι,
              (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                    StrongDual ℝ (E i) →L[ℝ] ℝ) :
                  (a : StrongDual ℝ (E i)) → ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ))
        m n)

Tactic:
simp [mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
simp :
  norm (E := ℝ)
      (∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i))) ≤
    (∑ i : ι, sorry) * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
      ((((g : (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) x :
              StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
          y :
        ℝ) ≤
    (∑ i : ι, sorry) * ‖x‖ * ‖y‖

Tactic:
simp only [LinearMap.mk₂_apply, g]

Premises used: LinearMap.mk₂_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
grw :
  LE.le (α := ℝ)
    (∑ i : ι,
      norm (E := ℝ)
        ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                StrongDual ℝ (E i) →L[ℝ] ℝ) :
              (a : StrongDual ℝ (E i)) → ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
    (∑ i : ι, sorry * ‖x‖ * ‖y‖)
⊢ norm (E := ℝ)
      (∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i))) ≤
    (∑ i : ι, sorry) * ‖x‖ * ‖y‖

Tactic:
grw [norm_sum_le, sum_mul, sum_mul]

Premises used: norm_sum_le, Finset.sum_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
h :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      norm (E := ℝ)
          ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ)
                    (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                  StrongDual ℝ (E i) →L[ℝ] ℝ) :
                (a : StrongDual ℝ (E i)) → ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            ℝ) ≤
        sorry * ‖x‖ * ‖y‖
⊢ LE.le (α := ℝ)
    (∑ i : ι,
      norm (E := ℝ)
        ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                StrongDual ℝ (E i) →L[ℝ] ℝ) :
              (a : StrongDual ℝ (E i)) → ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
    (∑ i : ι, sorry * ‖x‖ * ‖y‖)

Tactic:
gcongr with i _
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
h_1 : Membership.mem (γ := Finset ι) univ i
h : ‖L i‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
      ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖

Tactic:
grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_single_le_one]

Premises used: ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.le_opNorm₂, ContinuousLinearMap.norm_single_le_one
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
h_1 : Membership.mem (γ := Finset ι) univ i
h : ‖L i‖ * ‖x‖ * ‖y‖ ≤ sorry () * ‖x‖ * ‖y‖
⊢ ‖L i‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖

Tactic:
simp