mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
refine eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ -(↑(-r).toNNReal •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
← neg_smul,

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ -↑(-r).toNNReal •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ↑(ν.toFiniteMeasure s) = ↑ν s

Tactic:
FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ↑ν.toFiniteMeasure s = ↑ν s
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ s = μ.mass * μ.normalize s

Tactic:
have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff]

Goal state after:
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
⊢ μ s = μ.mass * μ.normalize s
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ 𝕜
⊢ Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
← integral_re_add_im (integrable μ f)

Goal state after:
case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ 𝕜
⊢ Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F
    (𝓝 (↑(∫ (x : Ω), RCLike.re (f x) ∂↑μ) + ↑(∫ (x : Ω), RCLike.im (f x) ∂↑μ) * RCLike.I))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : AEMeasurable f ↑μ
⊢ (Measure.map f ↑μ) univ ≤ ↑μ univ

Tactic:
rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ]
    exact measure_mono (subset_univ _)

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
⊢ IndepSets 𝒜 ℬ μ

Tactic:
rw [← 𝒜.biUnion_of_singleton]

Goal state after:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
⊢ IndepSets (⋃ x ∈ 𝒜, {x}) ℬ μ
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
by rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht]

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h : (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)
⊢ ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

Tactic:
intro s t hs ht

Goal state after:
case refine_2
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h : (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X Y : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
hY : Y =ᵐ[P] X
⊢ map X P = μ

Tactic:
hX.map_eq

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X Y : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
hY : Y =ᵐ[P] X
⊢ μ = μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y (map X P)

Tactic:
hX.map_eq

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map X P)

Tactic:
hX.map_eq

Goal state after:
case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (map X P)

Tactic:
hX.map_eq

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ AEMeasurable f (map X P)

Tactic:
hX.map_eq

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ AEMeasurable f μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case hX
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable f (map X P)

Tactic:
hX.map_eq

Goal state after:
case hX
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case hY
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable g (map X P)

Tactic:
hX.map_eq

Goal state after:
case hY
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable g μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
c : ℝ≥0∞
inst✝ : MeasurableSingletonClass 𝓧
x : 𝓧
hX : HasLaw X (c • dirac x) P
⊢ ∀ᵐ (y : 𝓧) ∂map X P, y = x

Tactic:
hX.map_eq

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
c : ℝ≥0∞
inst✝ : MeasurableSingletonClass 𝓧
x : 𝓧
hX : HasLaw X (c • dirac x) P
⊢ ∀ᵐ (y : 𝓧) ∂c • dirac x, y = x
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
c : ℝ≥0∞
inst✝ : MeasurableSingletonClass 𝓧
x : 𝓧
hX : HasLaw X (c • dirac x) P
⊢ X =ᵐ[P] fun x_1 ↦ x

Tactic:
by
  apply ae_of_ae_map (p := fun y ↦ y = x) hX.aemeasurable
  rw [hX.map_eq]
  apply Measure.ae_smul_measure (by simp)

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case pos
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB✝ : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖(B x) y‖ₑ
h : Integrable (fun ω ↦ (B (f (X ω))) (g (Y ω))) μ
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
have h1 : Integrable f (μ.map X) := (integrable_map_measure hf hX).2 <|
      hfXgY.integrable_left_of_integrable_op (B · ·) c hc hB h hfX hgY h'Y
    have h2 : Integrable g (μ.map Y) := (integrable_map_measure hg hY).2 <|
      hfXgY.integrable_right_of_integrable_op (B · ·) c hc hB h hfX hgY h'X
    exact hXY.integral_bilin_comp_comp hX hY h1 h2 B

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
by_cases h0 : p = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case e_a
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
h_sets_t'_univ : ∀ {i : ι}, i ∈ S → sets_t' i = univ
h_meas_s' : ∀ i ∈ S, MeasurableSet (sets_s' i)
h_meas_t' : ∀ i ∈ T, MeasurableSet (sets_t' i)
h_eq_inter_S : (fun ω i ↦ f (↑i) ω) ⁻¹' univ.pi sets_s = ⋂ i ∈ S, f i ⁻¹' sets_s' i
h_eq_inter_T : (fun ω i ↦ f (↑i) ω) ⁻¹' univ.pi sets_t = ⋂ i ∈ T, f i ⁻¹' sets_t' i
hf_Indep :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets i)
h_Inter_inter : (⋂ i ∈ S, f i ⁻¹' sets_s' i) ∩ ⋂ i ∈ T, f i ⁻¹' sets_t' i = ⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i)
h_meas_inter : ∀ i ∈ S ∪ T, MeasurableSet (sets_s' i ∩ sets_t' i)
a : α
h_indepS : (η a) (⋂ i ∈ S, f i ⁻¹' sets_s' i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets_s' i)
h_indepT : (η a) (⋂ i ∈ T, f i ⁻¹' sets_t' i) = ∏ i ∈ T, (η a) (f i ⁻¹' sets_t' i)
h_indepST : (η a) (⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i)) = ∏ i ∈ S ∪ T, (η a) (f i ⁻¹' (sets_s' i ∩ sets_t' i))
⊢ ∏ x ∈ T, (η a) (f x ⁻¹' (sets_s' x ∩ sets_t' x)) = ∏ i ∈ T, (η a) (f i ⁻¹' sets_t' i)

Tactic:
· refine Finset.prod_congr rfl fun i hi => ?_
    rw [h_sets_s'_univ hi, Set.univ_inter]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ filtrationOfSet hsm = natural (fun i ↦ (s i).indicator fun x ↦ 1) ⋯

Tactic:
simp only [filtrationOfSet, natural, measurableSpace_iSup_eq, exists_prop, mk.injEq]
  ext1 i
  refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)
  · rintro _ ⟨j, hij, rfl⟩
    refine measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, ?_⟩⟩
    rw [comap_eq_generateFrom]
    refine measurableSet_generateFrom ⟨{1}, measurableSet_singleton 1, ?_⟩
    ext x
    simp
  · rintro t ⟨n, ht⟩
    suffices MeasurableSpace.generateFrom {t | n ≤ i ∧
      MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β n)) (mβ n)] t} ≤
        MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t} by
      exact this _ ht
    refine generateFrom_le ?_
    rintro t ⟨hn, u, _, hu'⟩
    obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)
    on_goal 4 => rw [Set.mem_singleton_iff] at heq
    all_goals rw [heq] at hu'; rw [← hu']
    exacts [MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩,
      MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩), measurableSet_empty _]

Goal state after:
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
⊢ mean μ u F (s ∪ t) = mean μ u F s + mean μ u F t

Tactic:
refine tendsto_nhds_unique_of_eventuallyEq
    (hfoel.tendsto_nhds_mean _) (hfoel.tendsto_nhds_mean _ |>.add <| hfoel.tendsto_nhds_mean _) ?_

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
⊢ (fun i ↦ μ ((s ∪ t) ∩ F i) / μ (F i)) =ᶠ[↑u] fun x ↦ μ (s ∩ F x) / μ (F x) + μ (t ∩ F x) / μ (F x)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
⊢ (fun i ↦ μ ((s ∪ t) ∩ F i) / μ (F i)) =ᶠ[↑u] fun x ↦ μ (s ∩ F x) / μ (F x) + μ (t ∩ F x) / μ (F x)

Tactic:
filter_upwards [hfoel.eventually_measurableSet] with i hi

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
⊢ μ ((s ∪ t) ∩ F i) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : Group G
inst✝² : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst✝¹ : SMulInvariantMeasure G X μ
inst✝ : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∃ m,
    m univ = 1 ∧
      (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s

Tactic:
by
  use mean μ (Ultrafilter.of l) F
  refine ⟨?_, ?_, ?_⟩
  · exact (hfoel.mono <| Ultrafilter.of_le l).mean_univ_eq_one
  · exact (hfoel.mono <| Ultrafilter.of_le l).mean_union_eq_add_of_disjoint
  · exact (hfoel.mono <| Ultrafilter.of_le l).mean_smul_eq_mean

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F μ
hS : NullMeasurableSet s μ
h : μ F < μ s
⊢ ∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)

Tactic:
contrapose! h

Goal state after:
E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F μ
hS : NullMeasurableSet s μ
h : ∀ (x y : L), x ≠ y → Disjoint (x +ᵥ s) (y +ᵥ s)
⊢ μ s ≤ μ F
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ¬ε ≠ ∞
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
rw [not_ne_iff.mp hfinε]

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ¬ε ≠ ∞
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ∞
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: case h₀
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0

Tactic:
have ha2 : a ∈ ball z R := closedBall_subset_ball hr ha

Goal state after:
case h₀
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
ha2 : a ∈ ball z R
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:

Tactic:
_ = ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) := by
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
      all_goals positivity
    _ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) := by
      rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
      all_goals positivity
    _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by
      rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
      · congr; ring
      all_goals positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
a b : E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ (fun x ↦ (ω (γ.extend x)) (derivWithin ⇑γ.extend I x)) =ᵐ[volume.restrict (Ioc 0 1)] fun x ↦
    (ω (γ.extend x)) (deriv (⇑γ.extend) x)

Tactic:
← restrict_Ioo_eq_restrict_Ioc

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
a b : E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ (fun x ↦ (ω (γ.extend x)) (derivWithin ⇑γ.extend I x)) =ᵐ[volume.restrict (Ioo 0 1)] fun x ↦
    (ω (γ.extend x)) (deriv (⇑γ.extend) x)