awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
ι : 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 : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y : StrongDual ℝ ((i : ι) → E i)
⊢ Eq (α := ℝ)
    ((((diagonalStrongDualPi (E := E) L : (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →L[ℝ] ℝ) x :
            StrongDual ℝ ((i : ι) → E i) →L[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        y :
      ℝ)
    (∑ 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)) :
      ℝ)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
ι : 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 : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y : StrongDual ℝ ((i : ι) → E i)
⊢ Eq (α := ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              x :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        y :
      ℝ)
    (∑ i : ι,
        ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
                (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
      ℝ)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
ι : 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 : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x y : StrongDual ℝ ((i : ι) → E i)
simp_rw :
  Eq (α := ℝ)
    (∑ i : ι,
      ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
            StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E i)) → ℝ)
        (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    (∑ i : ι,
      ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
            StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E i)) → ℝ)
        (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)))
⊢ Eq (α := ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              x :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        y :
      ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              y :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        x :
      ℝ)

Tactic:
simp_rw [toBilinForm_diagonalStrongDualPi_apply, fun i ↦ (hL i).eq]

Premises used: _private.0.ContinuousLinearMap.toBilinForm_diagonalStrongDualPi_apply, LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsPosSemidef.isSymm
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
ι : 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 : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x : StrongDual ℝ ((i : ι) → E i)
rw :
  LE.le (α := ℝ) 0
    (∑ i : ι,
      ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
            StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E i)) → ℝ)
        (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)))
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              x :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        x :
      ℝ)

Tactic:
rw [toBilinForm_diagonalStrongDualPi_apply]

Premises used: _private.0.ContinuousLinearMap.toBilinForm_diagonalStrongDualPi_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
ι : 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 : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x : StrongDual ℝ ((i : ι) → E i)
⊢ LE.le (α := ℝ) 0
    (∑ i : ι,
      ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
            StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E i)) → ℝ)
        (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)))

Tactic:
sum_nonneg fun i _ ↦ (hL i).nonneg _

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.single, Real, LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg, Finset.sum_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
ι : 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 : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x : StrongDual ℝ ((i : ι) → E i)
⊢ LE.le (α := ℝ) 0
    (∑ i : ι,
      ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
              (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
            StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ (E i)) → ℝ)
        (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)))

Tactic:
exact sum_nonneg fun i _ ↦ (hL i).nonneg _

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg, Finset.sum_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y z : StrongDual ℝ (E × F)
⊢ (fun (x y : StrongDual ℝ (E × F)) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ)
          ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              (y ∘SL inl ℝ E F) :
            ℝ)
          ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                (a : StrongDual ℝ F) → ℝ)
              (y ∘SL inr ℝ E F) :
            ℝ))
      (x + y) z =
    HAdd.hAdd (α := ℝ)
      ((fun (x y : StrongDual ℝ (E × F)) ↦
          HAdd.hAdd (α := ℝ) (β := ℝ)
            ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (y ∘SL inl ℝ E F) :
              ℝ)
            ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (y ∘SL inr ℝ E F) :
              ℝ))
        x z)
      ((fun (x y : StrongDual ℝ (E × F)) ↦
          HAdd.hAdd (α := ℝ) (β := ℝ)
            ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (y ∘SL inl ℝ E F) :
              ℝ)
            ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (y ∘SL inr ℝ E F) :
              ℝ))
        y z)

Tactic:
simp [add_add_add_comm]

Premises used: add_add_add_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
c : ℝ
m n : StrongDual ℝ (E × F)
⊢ (fun (x y : StrongDual ℝ (E × F)) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ)
          ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              (y ∘SL inl ℝ E F) :
            ℝ)
          ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                (a : StrongDual ℝ F) → ℝ)
              (y ∘SL inr ℝ E F) :
            ℝ))
      (c • m) n =
    HSMul.hSMul (β := ℝ) c
      ((fun (x y : StrongDual ℝ (E × F)) ↦
          HAdd.hAdd (α := ℝ) (β := ℝ)
            ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (y ∘SL inl ℝ E F) :
              ℝ)
            ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (y ∘SL inr ℝ E F) :
              ℝ))
        m n)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y z : StrongDual ℝ (E × F)
⊢ (fun (x y : StrongDual ℝ (E × F)) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ)
          ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              (y ∘SL inl ℝ E F) :
            ℝ)
          ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                (a : StrongDual ℝ F) → ℝ)
              (y ∘SL inr ℝ E F) :
            ℝ))
      x (y + z) =
    HAdd.hAdd (α := ℝ)
      ((fun (x y : StrongDual ℝ (E × F)) ↦
          HAdd.hAdd (α := ℝ) (β := ℝ)
            ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (y ∘SL inl ℝ E F) :
              ℝ)
            ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (y ∘SL inr ℝ E F) :
              ℝ))
        x y)
      ((fun (x y : StrongDual ℝ (E × F)) ↦
          HAdd.hAdd (α := ℝ) (β := ℝ)
            ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (y ∘SL inl ℝ E F) :
              ℝ)
            ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (y ∘SL inr ℝ E F) :
              ℝ))
        x z)

Tactic:
simp [add_add_add_comm]

Premises used: add_add_add_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
c : ℝ
m n : StrongDual ℝ (E × F)
⊢ (fun (x y : StrongDual ℝ (E × F)) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ)
          ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              (y ∘SL inl ℝ E F) :
            ℝ)
          ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                (a : StrongDual ℝ F) → ℝ)
              (y ∘SL inr ℝ E F) :
            ℝ))
      m (c • n) =
    HSMul.hSMul (β := ℝ) c
      ((fun (x y : StrongDual ℝ (E × F)) ↦
          HAdd.hAdd (α := ℝ) (β := ℝ)
            ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                (y ∘SL inl ℝ E F) :
              ℝ)
            ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (y ∘SL inr ℝ E F) :
              ℝ))
        m n)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
simp :
  ‖HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ)‖ ≤
    HAdd.hAdd (α := ℝ) sorry sorry * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
      ((((g : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x : StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ (E × F)) → ℝ)
          y :
        ℝ) ≤
    HAdd.hAdd (α := ℝ) sorry 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 Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
grw :
  norm (E := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ) +
      norm (E := ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ) ≤
    sorry * ‖x‖ * ‖y‖ + sorry * ‖x‖ * ‖y‖
⊢ ‖HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ)‖ ≤
    HAdd.hAdd (α := ℝ) sorry sorry * ‖x‖ * ‖y‖

Tactic:
grw [norm_add_le, add_mul, add_mul]

Premises used: add_mul, norm_add_le
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
h₁ :
  norm (E := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖
h₂ :
  norm (E := ℝ)
      ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ) +
      norm (E := ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ) ≤
    sorry * ‖x‖ * ‖y‖ + sorry * ‖x‖ * ‖y‖

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
h₁ : ‖L₁‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖

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

Premises used: ContinuousLinearMap.norm_inl_le_one, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.le_opNorm₂
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
h₁ : ‖L₁‖ * ‖x‖ * ‖y‖ ≤ sorry () * ‖x‖ * ‖y‖
⊢ ‖L₁‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
h₂ : ‖L₂‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
⊢ norm (E := ℝ)
      ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖

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

Premises used: ContinuousLinearMap.norm_inr_le_one, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.le_opNorm₂