awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
θ : ℝ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
have refine : Eq (α := (L : StrongDual ℝ (E × E)) → ℂ)
  (charFunDual (mE := Prod.instMeasurableSpace)
    (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)))
  (charFunDual (μ.prod μ))
Tactic: refine Measure.ext_of_charFunDual ?_
-- 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
θ : ℝ
⊢ Eq (α := (L : StrongDual ℝ (E × E)) → ℂ)
    (charFunDual (mE := Prod.instMeasurableSpace)
      (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)))
    (charFunDual (μ.prod μ))
have h : ∀ (L : StrongDual ℝ (E × E)),
  charFunDual (mE := Prod.instMeasurableSpace)
      (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)) L =
    charFunDual (μ.prod μ) L
Tactic: ext L
-- 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)
⊢ charFunDual (mE := Prod.instMeasurableSpace)
      (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)) L =
    charFunDual (μ.prod μ) L
have h : cexp
    (-(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                  (a : E) → ℝ);
                μ] :
            ℂ) /
        2 +
      -(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
                  (a : E) → ℝ);
                μ] :
            ℂ) /
        2) =
  cexp
    (-(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
            ℂ) /
        2 +
      -(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] :
            ℂ) /
        2)
Tactic: simp_rw [charFunDual_map, charFunDual_prod, charFunDual_eq_of_forall_strongDual_eq_zero hμ,
    ← Complex.exp_add]
-- 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)
⊢ cexp
      (-(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) /
          2 +
        -(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) /
          2) =
    cexp
      (-(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) /
          2 +
        -(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) /
          2)
have h : cexp
    (-((↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                  (a : E) → ℝ);
                μ] :
            ℂ) +
          (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
                  (a : E) → ℝ);
                μ] :
            ℂ)) /
      2) =
  cexp
    (-((↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
            ℂ) +
          (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                μ] :
            ℂ)) /
      2)
Tactic: rw [← add_div, ← add_div, ← neg_add, ← neg_add]
-- 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)
⊢ cexp
      (-((↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) +
            (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ)
                        (ContinuousLinearMap.inr ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ)) /
        2) =
    cexp
      (-((↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) +
            (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ] :
              ℂ)) /
        2)
have h : (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
            (a : E) → ℝ);
          μ] :
      ℂ) +
    (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (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) → ℝ); μ] : ℂ)
Tactic: congr 3
-- 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)
⊢ (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
              (a : E) → ℝ);
            μ] :
        ℂ) +
      (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (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 : Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
        (a : E) → ℝ);
      μ] +
    Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (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) → ℝ); μ]
Tactic: norm_cast
-- 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)
⊢ (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))
have h : ∀ (x : E),
  Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E : (a : E) → ℝ) x : ℝ)
    ((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)) :
          (a : E) → ℝ)
        x :
      ℝ)
Tactic: ext x
-- 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)
x : E
⊢ Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E : (a : E) → ℝ) x : ℝ)
    ((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)) :
          (a : E) → ℝ)
        x :
      ℝ)
have h : Eq (α := ℝ) ((L : (a : E × E) → ℝ) (Real.cos θ • x, -Real.sin θ • x) : ℝ)
  ((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)) :
        (a : E) → ℝ)
      x :
    ℝ)
Tactic: simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inl_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
-- 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)
x : E
⊢ Eq (α := ℝ) ((L : (a : E × E) → ℝ) (Real.cos θ • x, -Real.sin θ • x) : ℝ)
    ((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)) :
          (a : E) → ℝ)
        x :
      ℝ)
have h : HAdd.hAdd (α := ℝ) (β := ℝ)
    ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E) : (a : E) → ℝ)
        (Real.cos θ • x, -Real.sin θ • x).1 :
      ℝ)
    ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E) : (a : E) → ℝ)
        (Real.cos θ • x, -Real.sin θ • x).2 :
      ℝ) =
  (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)) :
      (a : E) → ℝ)
    x
Tactic: rw [← L.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (hypothesis)
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)
⊢ Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
          (a : E) → ℝ);
        μ] +
      Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (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 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))
Tactic: have h1 : (L.comp (.rotation θ)).comp (.inl ℝ E E)
      = Real.cos θ • L.comp (.inl ℝ E E) - Real.sin θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inl_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
    rw [← L.comp_inl_add_comp_inr]
    simp [-neg_smul, sub_eq_add_neg]
-- 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))
⊢ (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))
have h : ∀ (x : E),
  Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E : (a : E) → ℝ) x : ℝ)
    ((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)) :
          (a : E) → ℝ)
        x :
      ℝ)
Tactic: ext x
-- 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))
x : E
⊢ Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E : (a : E) → ℝ) x : ℝ)
    ((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)) :
          (a : E) → ℝ)
        x :
      ℝ)
have h : (L : (a : E × E) → ℝ) (Real.sin θ • x, Real.cos θ • x) =
  HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
    HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)
Tactic: simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inr_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', Pi.smul_apply, ContinuousLinearMap.inl_apply, smul_eq_mul]
-- 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))
x : E
⊢ (L : (a : E × E) → ℝ) (Real.sin θ • x, Real.cos θ • x) =
    HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
      HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)
have h : HAdd.hAdd (α := ℝ) (β := ℝ)
    ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E) : (a : E) → ℝ)
        (Real.sin θ • x, Real.cos θ • x).1 :
      ℝ)
    ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E) : (a : E) → ℝ)
        (Real.sin θ • x, Real.cos θ • x).2 :
      ℝ) =
  HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
    HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)
Tactic: rw [← L.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (hypothesis)
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))
⊢ Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
          (a : E) → ℝ);
        μ] +
      Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (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 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))
Tactic: have h2 : (L.comp (.rotation θ)).comp (.inr ℝ E E)
      = Real.sin θ • L.comp (.inl ℝ E E) + Real.cos θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inr_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', Pi.smul_apply, ContinuousLinearMap.inl_apply, smul_eq_mul]
    rw [← L.comp_inl_add_comp_inr]
    simp
-- 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))
⊢ Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
          (a : E) → ℝ);
        μ] +
      Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (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 : Var[(⇑(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))) :
        (a : E) → ℝ);
      μ] +
    Var[(⇑(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))) :
        (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) → ℝ); μ]
Tactic: rw [h1, h2]