mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
⊢ 1 < finrank K (V ⧸ (↑e).fixedSubmodule)

Tactic:
by omega

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun n ↦ v (t n)) (v (⋃ n, s n))
⊢ Tendsto (fun n ↦ v (s n)) atTop (𝓝 (v (⋃ n, s n)))

Tactic:
convert! (HasSum.tendsto_sum_nat this).comp (tendsto_add_atTop_nat 1) with n

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun n ↦ v (t n)) (v (⋃ n, s n))
n : ℕ
⊢ v (s n) = ((fun n ↦ ∑ i ∈ Finset.range n, v (t i)) ∘ fun a ↦ a + 1) n
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal ((ε / M) ^ p.toReal) ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal

Tactic:
← ENNReal.ofReal_rpow_of_pos (div_pos hε hM)

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal (ε / M) ^ p.toReal ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
⊢ j.toSignedMeasure.toJordanDecomposition = j

Tactic:
toJordanDecomposition_toSignedMeasure

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
⊢ j = j
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f μ
⊢ μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f

Tactic:
ext1 i hi
    rw [withDensityᵥ_apply (hf.smul r) hi, _root_.smul_apply, withDensityᵥ_apply hf hi, ←
      integral_smul r f]
    simp only [Pi.smul_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c

Tactic:
refine (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null ?_ ?_

Goal state after:
case neg.refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∀ t ∈ Set.range (spanningSets (μ.trim hm)), MeasurableSet t

case neg.refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∀ t ∈ Set.range (spanningSets (μ.trim hm)), (μ.restrict t) {x | (fun x ↦ μ[f | m] x ≤ c) x}ᶜ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
⊢ (fun a ↦ |f a|) =ᵐ[μ] f

Tactic:
filter_upwards [hf] with ω hω using abs_of_nonneg hω

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) (u ×ˢ v)

Tactic:
Measure.prod_prod

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ↑a.1 u * ↑a.2 v
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case e_μ.e_a
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
nonzero : μ ≠ 0
f : Ω → E
⊢ (↑μ univ)⁻¹ = ↑μ.mass⁻¹

Tactic:
simp [ENNReal.coe_inv (μ.mass_nonzero_iff.mpr nonzero), ennreal_mass]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ : FiniteMeasure Ω
⊢ ∀ ⦃a₂ : FiniteMeasure Ω⦄, μ.toWeakDualBCNN = a₂.toWeakDualBCNN → μ = a₂

Tactic:
ν

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
⊢ μ.toWeakDualBCNN = ν.toWeakDualBCNN → μ = ν
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖{x | ‖f i x‖₊ < C}.indicator (f i) x‖₊ ≤ C
⊢ ↑C * μ univ ^ p.toReal⁻¹ ≤ ↑C * μ univ ^ p.toReal⁻¹

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
have : ∀ n, μ {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ := by
    intro n
    have : C ^ ENNReal.toReal 1 * μ {x | ENNReal.ofNNReal C ≤ ‖μ[g|ℱ n] x‖₊} ≤
        eLpNorm μ[g | ℱ n] 1 μ ^ ENNReal.toReal 1 := by
      rw [ENNReal.toReal_one, ENNReal.rpow_one]
      convert!
        mul_meas_ge_le_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top
          (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable C
      · rw [ENNReal.toReal_one, ENNReal.rpow_one, enorm_eq_nnnorm]
    rw [ENNReal.toReal_one, ENNReal.rpow_one, mul_comm, ←
      ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne)] at this
    simp_rw [ENNReal.coe_le_coe] at this
    refine this.trans ?_
    rw [ENNReal.div_le_iff_le_mul (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne'))
        (Or.inl ENNReal.coe_lt_top.ne),
      hC, NNReal.inv_mk, ENNReal.coe_mul, ENNReal.coe_toNNReal hg.eLpNorm_lt_top.ne, ← mul_assoc, ←
      ENNReal.ofReal_eq_coe_nnreal, ← ENNReal.ofReal_mul hδ.le, mul_inv_cancel₀ hδ.ne',
      ENNReal.ofReal_one, one_mul, ENNReal.rpow_one]
    exact eLpNorm_condExp_le_eLpNorm _ le_rfl

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ENNReal.ofReal δ
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
B : ∀ {ν : FiniteMeasure Ω'}, ν (range f)ᶜ = 0 → ∫ (y : Ω') in range f, g' y ∂↑ν = ∫ (y : Ω'), g' y ∂↑ν
⊢ Tendsto (fun i ↦ ∫ (y : Ω') in range f, g' y ∂↑i) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (y : Ω') in range f, g' y ∂↑μ))

Tactic:
B hμ

Goal state after:
Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
B : ∀ {ν : FiniteMeasure Ω'}, ν (range f)ᶜ = 0 → ∫ (y : Ω') in range f, g' y ∂↑ν = ∫ (y : Ω'), g' y ∂↑ν
⊢ Tendsto (fun i ↦ ∫ (y : Ω') in range f, g' y ∂↑i) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (y : Ω'), g' y ∂↑μ))
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
⊢ ∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0

Tactic:
have mbles : ∀ r : ℝ, MeasurableSet (frontier (Metric.thickening r s)) :=
    fun r ↦ isClosed_frontier.measurableSet

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
⊢ ∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
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 g : (i : ι) → Ω → β i
hf :
  ∀ (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 : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i
a : α
ha : ∀ i ∈ S, f i =ᵐ[κ a] g i
h'a : (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
i : ι
hi : i ∈ S
⊢ (κ a) (g i ⁻¹' sets i) = (κ a) (f i ⁻¹' sets i)

Tactic:
apply measure_congr

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 g : (i : ι) → Ω → β i
hf :
  ∀ (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 : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i
a : α
ha : ∀ i ∈ S, f i =ᵐ[κ a] g i
h'a : (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
i : ι
hi : i ∈ S
⊢ g i ⁻¹' sets i =ᵐ[κ a] f i ⁻¹' sets i
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 g : (i : ι) → Ω → β i
hf :
  ∀ (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 : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i
a : α
ha : ∀ i ∈ S, f i =ᵐ[κ a] g i
h'a : (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
A : ∀ i ∈ S, (κ a) (g i ⁻¹' sets i) = (κ a) (f i ⁻¹' sets i)
⊢ (κ a) (⋂ i ∈ S, g i ⁻¹' sets i) = (κ a) (⋂ i ∈ S, f i ⁻¹' sets i)

Tactic:
apply measure_congr

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 g : (i : ι) → Ω → β i
hf :
  ∀ (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 : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i
a : α
ha : ∀ i ∈ S, f i =ᵐ[κ a] g i
h'a : (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
A : ∀ i ∈ S, (κ a) (g i ⁻¹' sets i) = (κ a) (f i ⁻¹' sets i)
⊢ ⋂ i ∈ S, g i ⁻¹' sets i =ᵐ[κ a] ⋂ i ∈ S, f i ⁻¹' sets i
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case mpr
Ω : 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 μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((Measure.map f μ).prod (Measure.map g μ)) (s ×ˢ t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
Measure.prod_prod

Goal state after:
case mpr
Ω : 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 μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (Measure.map f μ) s * (Measure.map g μ) t = (Measure.map f μ) s * (Measure.map g μ) t
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
⊢ x ≤ ↑‖f‖₊

Tactic:
apply le_trans hi

Goal state after:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i ≤ ↑‖f‖₊
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.basic
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t

Tactic:
exact measurableSet_generateFrom ht

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
t : Set Ω
ht : MeasurableSet t
iht : ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
a : α
ha : (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
⊢ (κ a) (tᶜ ∩ t2) = (κ a) tᶜ * (κ a) t2

Tactic:
have : tᶜ ∩ t2 = t2 \ (t ∩ t2) := by
      rw [Set.inter_comm t, Set.sdiff_self_inter, Set.sdiff_eq_compl_inter]

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
t : Set Ω
ht : MeasurableSet t
iht : ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
a : α
ha : (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
this : tᶜ ∩ t2 = t2 \ (t ∩ t2)
⊢ (κ a) (tᶜ ∩ t2) = (κ a) tᶜ * (κ a) t2
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2.hf
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable Prod.snd (μ.prod ν)

pp: case refine_2.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᵐ[Measure.map Prod.snd (μ.prod ν)] Y

Tactic:
· exact measurable_snd.aemeasurable

Goal state after:
case refine_2.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᵐ[Measure.map Prod.snd (μ.prod ν)] Y
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) κ μ
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ

Tactic:
have hφ_ae := ae_of_ae_map hf hφ.ae_eq_mk

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)
⊢ IndepFun (φ ∘ f) (ψ ∘ g) κ μ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
u : ℕ → ι
hu : Tendsto u atTop L
G : Set Ω
hG : IsOpen[inst✝²] G
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) (map u atTop) fun i ↦ (μs i) G

Tactic:
exact isBoundedUnder_of ⟨1, by simp⟩ |>.isCoboundedUnder_ge

Goal state after: