mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable f (⇑κ ∘ₘ μ)
hg : AEMeasurable g (⇑κ ∘ₘ μ)
hφ : AEMeasurable φ (Measure.map f (⇑κ ∘ₘ μ))
hψ : AEMeasurable ψ (Measure.map g (⇑κ ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haψ : ∀ᵐ (ω : Ω) ∂κ a, ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)
ω : Ω
⊢ ψ (g ω) = AEMeasurable.mk ψ hψ (g ω) → (AEMeasurable.mk ψ hψ ∘ g) ω = (ψ ∘ g) ω

Tactic:
hωψ

Goal state after:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable f (⇑κ ∘ₘ μ)
hg : AEMeasurable g (⇑κ ∘ₘ μ)
hφ : AEMeasurable φ (Measure.map f (⇑κ ∘ₘ μ))
hψ : AEMeasurable ψ (Measure.map g (⇑κ ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
a : α
haψ : ∀ᵐ (ω : Ω) ∂κ a, ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)
ω : Ω
hωψ : ψ (g ω) = AEMeasurable.mk ψ hψ (g ω)
⊢ (AEMeasurable.mk ψ hψ ∘ g) ω = (ψ ∘ g) ω
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
⊢ Tendsto μs L (𝓝 μ)

Tactic:
by
  obtain rfl | _ := L.eq_or_neBot
  · simp
  refine tendsto_of_forall_isClosed_limsup_le <| fun F hF_closed ↦ ?_
  rw [← ENNReal.coe_le_coe, ENNReal.ofNNReal_limsup <|
      isBoundedUnder_of_eventually_le (a := 1) (by simp)]
  refine ENNReal.le_of_forall_pos_le_add <| fun ε hε _ ↦ ?_
  obtain ⟨K, hKc, hK_le⟩ := isTightMeasureSet_iff_exists_isCompact_measure_compl_le.mp
    h₁ ε (by positivity)
  grw [limsup_le_limsup (v := fun i ↦ μs i (F ∩ K) + (ε : ENNReal))]
  · rw [limsup_add_const _ _ _ (by isBoundedDefault) (by isBoundedDefault)]
    apply add_le_add _ (by simp)
    specialize h₂ (F ∩ K) <| hKc.inter_left hF_closed
    rw [← ENNReal.coe_le_coe, ENNReal.ofNNReal_limsup <|
      isBoundedUnder_of_eventually_le (a := 1) (by simp)] at h₂
    grw [h₂]
    simp [measure_mono]
  · refine .of_forall (fun i ↦ ?_)
    simp_rw [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
    grw [measure_mono (t := (F ∩ K) ∪ F \ K) (by simp), measure_union_le]
    gcongr
    exact le_trans (measure_mono (by simp)) <| hK_le (μs i) <| by simp

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

Goal state before:
pp: α : 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_Indep : iIndepFun f κ μ
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
i : ι
⊢ ∀ (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩

Tactic:
hi

Goal state after:
α : 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_Indep : iIndepFun f κ μ
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
i : ι
hi : i ∈ S
⊢ sets_s' i = sets_s ⟨i, hi⟩
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_5
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun k ↦ {s k}) S) (piiUnionInter (fun k ↦ {s k}) T) η μ

Tactic:
· exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST

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

Goal state before:
pp: α : 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_Indep : iIndepFun f κ μ
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⟩
i : ι
⊢ i ∈ T → sets_s' i = univ

Tactic:
hi

Goal state after:
α : 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_Indep : iIndepFun f κ μ
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⟩
i : ι
hi : i ∈ T
⊢ sets_s' i = univ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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_Indep : iIndepFun f κ μ
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
i : ι
⊢ i ∈ S → sets_t' i = univ

Tactic:
hi

Goal state after:
α : 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_Indep : iIndepFun f κ μ
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
i : ι
hi : i ∈ S
⊢ sets_t' i = univ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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_Indep : iIndepFun f κ μ
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
i : ι
⊢ i ∈ S → MeasurableSet (sets_s' i)

Tactic:
hi

Goal state after:
α : 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_Indep : iIndepFun f κ μ
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
i : ι
hi : i ∈ S
⊢ MeasurableSet (sets_s' i)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
r : ℝ≥0
hr : r < ν G
T : Finset (Set Ω)
TS : ∀ t ∈ T, t ∈ S
T_meas : r < ν (⋃ t ∈ T, t)
TG : ⋃ t ∈ T, t ⊆ G
this : Tendsto (fun i ↦ (μ i) (⋃ t ∈ T, t)) l (𝓝 (ν (⋃ t ∈ T, t)))
i : ι
⊢ r < (μ i) (⋃ t ∈ T, t) → r < (μ i) G

Tactic:
hi

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
r : ℝ≥0
hr : r < ν G
T : Finset (Set Ω)
TS : ∀ t ∈ T, t ∈ S
T_meas : r < ν (⋃ t ∈ T, t)
TG : ⋃ t ∈ T, t ⊆ G
this : Tendsto (fun i ↦ (μ i) (⋃ t ∈ T, t)) l (𝓝 (ν (⋃ t ∈ T, t)))
i : ι
hi : r < (μ i) (⋃ t ∈ T, t)
⊢ r < (μ i) G
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Var[X; μ] = ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
rw [← covariance_self hX.aemeasurable, covariance_eq_sub hX hX, pow_two, pow_two]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
exact (AEMeasurable.pow_const (hm.aemeasurable.sub_const _) _).aestronglyMeasurable

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)

Tactic:
have hb : ∀ᵐ ω ∂μ, X ω ≤ b := h.mono fun ω h => h.2

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
f : BoundedContinuousFunction E NNReal
⊢ Tendsto (fun i ↦ ∫⁻ (ω : E), ↑(f ω) ∂Measure.map (X i) μ') l (𝓝 (∫⁻ (a : Ω'), ↑(f (Z a)) ∂μ'))

Tactic:
conv in ∫⁻ _, _ ∂_ => rw [lintegral_map' (by fun_prop) (hX₁ i)]

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
f : BoundedContinuousFunction E NNReal
⊢ Tendsto (fun i ↦ ∫⁻ (a : Ω'), ↑(f (X i a)) ∂μ') l (𝓝 (∫⁻ (a : Ω'), ↑(f (Z a)) ∂μ'))
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h : IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) (AEMeasurable.mk (f k) ⋯) κ μ
a : α
⊢ (∀ᵐ (ω : Ω) ∂κ a, f i ω = AEMeasurable.mk (f i) ⋯ ω) →
    (∀ᵐ (ω : Ω) ∂κ a, f j ω = AEMeasurable.mk (f j) ⋯ ω) →
      (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) =ᵐ[κ a] fun a ↦ (f i a, f j a)

Tactic:
hi

Goal state after:
α : 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
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h : IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) (AEMeasurable.mk (f k) ⋯) κ μ
a : α
hi : ∀ᵐ (ω : Ω) ∂κ a, f i ω = AEMeasurable.mk (f i) ⋯ ω
⊢ (∀ᵐ (ω : Ω) ∂κ a, f j ω = AEMeasurable.mk (f j) ⋯ ω) →
    (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) =ᵐ[κ a] fun a ↦ (f i a, f j a)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
⊢ (∀ᵐ (ω : Ω) ∂κ a, f i ω = AEMeasurable.mk (f i) ⋯ ω) →
    (∀ᵐ (ω : Ω) ∂κ a, f j ω = AEMeasurable.mk (f j) ⋯ ω) →
      (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) =ᵐ[κ a] fun a ↦ (f i a, f j a)

Tactic:
hi

Goal state after:
α : 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
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hi : ∀ᵐ (ω : Ω) ∂κ a, f i ω = AEMeasurable.mk (f i) ⋯ ω
⊢ (∀ᵐ (ω : Ω) ∂κ a, f j ω = AEMeasurable.mk (f j) ⋯ ω) →
    (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) =ᵐ[κ a] fun a ↦ (f i a, f j a)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
have h : IndepFun (∏ j ∈ s, (hf_meas j).mk (f j)) ((hf_meas i).mk (f i)) κ μ := by
    refine iIndepFun.indepFun_finsetProd_of_notMem ?_ (fun i ↦ (hf_meas i).measurable_mk) hi
    exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ↑𝓕 i ≤ ↑𝓕 j

Tactic:
· exact 𝓕.mono hij

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this✝¹ : TopologicalSpace ι := Preorder.topology ι
this✝ : OrderTopology ι
this : (𝓝[>] i).NeBot
⊢ ↑𝓕₊ i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j

Tactic:
exact rightCont_eq_of_neBot_nhdsGT _ _

Goal state after: