Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
⊢ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

pp: case neg.h₁
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) ((μ Set.univ)⁻¹ • μ)
⊢ (μ Set.univ)⁻¹ ≠ 0

pp: case neg.h₂
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) ((μ Set.univ)⁻¹ • μ)
⊢ (μ Set.univ)⁻¹ ≠ ∞

Tactic:
]

Goal state after:
case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
⊢ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

case neg.h₁
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) ((μ Set.univ)⁻¹ • μ)
⊢ (μ Set.univ)⁻¹ ≠ 0

case neg.h₂
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot✝ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) ((μ Set.univ)⁻¹ • μ)
⊢ (μ Set.univ)⁻¹ ≠ ∞