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
θ : ℝ
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[(⇑(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) → ℝ); μ]
have h : 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) → ℝ); μ]
Tactic: simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.coe_smul',
    ContinuousLinearMap.coe_add']
-- 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))
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))
⊢ 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) → ℝ); μ]
have h : HPow.hPow (β := ℕ) (Real.cos θ) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 1
Tactic: have h := Real.cos_sq_add_sin_sq θ
-- 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
L : StrongDual ℝ E
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) 0
have rw : Eq (α := ℝ)
  (∫ (x : E),
    @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      (L : (a : E) → ℝ) (x + y) ∂μ)
  0
Tactic: rw [integral_conv (by fun_prop)]
-- 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
L : StrongDual ℝ E
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) (x + y) ∂μ)
    0
have simp : Eq (α := ℝ)
  (∫ (x : E),
    @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
  0
Tactic: simp only [map_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
L : StrongDual ℝ E
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    (∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ)
have e_f : ∀ (x : E),
  (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ)
Tactic: congr with 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
L : StrongDual ℝ E
x : E
⊢ @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ (L : (a : E) → ℝ) x)
    (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
have funProp : enorm (E := ℝ) ((L : (a : E) → ℝ) x : ℝ) ≠ ∞
Tactic: fun_prop
-- 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
L : StrongDual ℝ E
x : E
⊢ (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ)
have e_f : HAdd.hAdd (α := ℝ)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (a : E) ↦
      (L : (a : E) → ℝ) x)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (a : E) ↦
      (L : (a : E) → ℝ) a) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y :
      ℝ)
Tactic: rw [integral_add (by fun_prop) (by fun_prop)]
-- 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
L : StrongDual ℝ E
⊢ Integrable (ε := ℝ)
    (fun (x : E) ↦
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)
    μ
have funProp : enorm (E := ℝ)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      (L : (a : E) → ℝ) y) ≠
  ∞
Tactic: fun_prop
-- 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
L : StrongDual ℝ E
⊢ ∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)
have rw : HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ)
    (∫ (a : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y ∂μ) =
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      (L : (a : E) → ℝ) y)
Tactic: rw [integral_add (by fun_prop) (by fun_prop)]
-- 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
L : StrongDual ℝ E
⊢ HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y) =
    0
have rw : HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
    (∫ (x : E), (L : (a : E) → ℝ) ((ContinuousLinearEquiv.neg ℝ : (a : E) → E) x : E) ∂μ) =
  0
Tactic: rw [integral_map (by fun_prop) (by fun_prop)]
-- 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
L : StrongDual ℝ E
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    0
have calc : Eq (α := ℝ)
  (∫ (x : E),
    @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
  (∫ (x : E),
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ) ∂μ)
Tactic: calc ∫ x, ∫ y, L x + L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ
  _ = ∫ x, L x + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ := by
    congr with x
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]
  _ = ∫ x, L x ∂μ + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) := by
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp
  _ = 0 := by
    rw [integral_map (by fun_prop) (by fun_prop)]
    simp [integral_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
L : StrongDual ℝ E
calc :
  Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    (∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ)
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    0
have calc₁ : ∫ (x : E),
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ) ∂μ =
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      (L : (a : E) → ℝ) y)
Tactic: calc ∫ x, ∫ y, L x + L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ
  _ = ∫ x, L x + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ := by
    congr with x
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]
  _ = ∫ x, L x ∂μ + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) := by
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp
  _ = 0 := by
    rw [integral_map (by fun_prop) (by fun_prop)]
    simp [integral_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
L : StrongDual ℝ E
calc :
  Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    (∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ)
calc₁ :
  ∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    0
have calc₂ : HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      (L : (a : E) → ℝ) y) =
  0
Tactic: calc ∫ x, ∫ y, L x + L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ
  _ = ∫ x, L x + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ := by
    congr with x
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]
  _ = ∫ x, L x ∂μ + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) := by
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp
  _ = 0 := by
    rw [integral_map (by fun_prop) (by fun_prop)]
    simp [integral_neg]
-- 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
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
⊢ ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
have hint₁ : (∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
      (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
  Integrable (ε := ℝ)
    (fun (x : E) ↦
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
    μ
Tactic: rw [integrable_conv_iff (by fun_prop)] at hint
Cleared hypotheses: hint, hC'_pos, hC'_lt
-- 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
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
⊢ ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
have hC : ∀ᵐ (x : E) ∂μ,
  @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
    (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
Tactic: replace hC := hint.1
-- 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
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC :
  ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)) (Measure.map (-id) μ)
⊢ ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
have h : ∀ (y : E)
  (hy : @Integrable ℝ _ _ _ inst_2 (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) (Measure.map (-id) μ)),
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
Tactic: filter_upwards [hC] with y hy
-- 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
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC :
  ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)) (Measure.map (-id) μ)
y : E
hy : @Integrable ℝ _ _ _ inst_2 (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) (Measure.map (-id) μ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
have hy₁ : Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ
Tactic: rw [integrable_map_measure (by fun_prop) (by fun_prop)] at hy
Cleared hypotheses: hy
-- 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
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC :
  ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
have h : ∀ (x : E),
  rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2) = ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) x
Tactic: convert! hy with x