-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
h2 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) +
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
h :
  HPow.hPow (β := ℕ) (Real.cos θ) 2 *
            Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ);
              μ] -
          2 *
            (Real.cos θ *
              (Real.sin θ *
                cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ),
                  (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ])) +
        HPow.hPow (β := ℕ) (Real.sin θ) 2 *
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] +
      (HPow.hPow (β := ℕ) (Real.sin θ) 2 *
            Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ);
              μ] +
          2 *
            (Real.sin θ *
              (Real.cos θ *
                cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ),
                  (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ])) +
        HPow.hPow (β := ℕ) (Real.cos θ) 2 *
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ]) =
    Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] +
      Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ]
h₁ :
  MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ))
    2 μ
h₂ :
  MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ))
    2 μ
h₃ :
  MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ))
    2 μ
⊢ Var[HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ) -
          HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
        μ] +
      Var[HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ) +
          HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
        μ] =
    Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] +
      Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ]
have h₄ : MemLp
  (HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
    (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ))
  2 μ
Tactic: rw [variance_sub, variance_smul, variance_add, variance_smul, variance_smul, covariance_smul_left,
    covariance_smul_right, variance_smul, covariance_smul_left, covariance_smul_right]