mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
s✝ : Set (α × β)
x✝¹ : Set α
Hu : MeasurableSet x✝¹
x✝ : Set β
Hv : MeasurableSet x✝
Heq : x✝¹ ×ˢ x✝ = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) (x✝¹ ×ˢ x✝)

Tactic:
Measure.prod_prod,

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

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
exact fun f ↦
    tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass μs_lim mass_lim f

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

Goal state before:
pp: α : 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 : g =ᵐ[μ] 0
n : ι
x : α
⊢ μ[g | ℱ n] x = μ[0 | ℱ n] x → {x | 0 ≤ ‖μ[g | ℱ n] x‖₊}.indicator μ[g | ℱ n] x = 0 x

Tactic:
hx

Goal state after:
α : 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 : g =ᵐ[μ] 0
n : ι
x : α
hx : μ[g | ℱ n] x = μ[0 | ℱ n] x
⊢ {x | 0 ≤ ‖μ[g | ℱ n] x‖₊}.indicator μ[g | ℱ n] x = 0 x
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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ f i x = Exists.choose ⋯ x → {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
hx

Goal state after:
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ g i x = f i x

pp: case pos.h
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ x ∈ {x | C ≤ ‖g i x‖₊}

Tactic:
hx

Goal state after:
case pos
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ g i x = Exists.choose ⋯ x

case pos.h
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ x ∈ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos.h
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : C ≤ ‖f i x‖₊
⊢ x ∈ {x | C ≤ ‖g i x‖₊}

Tactic:
hx

Goal state after:
case pos.h
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : C ≤ ‖Exists.choose ⋯ x‖₊
⊢ x ∈ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : 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
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ ENNReal.ofReal 1 * eLpNorm g 1 μ

Tactic:
ENNReal.ofReal_one,

Goal state after:
α : 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
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ 1 * eLpNorm g 1 μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg.h
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : ¬C ≤ ‖f i x‖₊
⊢ x ∉ {x | C ≤ ‖g i x‖₊}

Tactic:
hx

Goal state after:
case neg.h
α : 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 : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : ¬C ≤ ‖Exists.choose ⋯ x‖₊
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: case h₁
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hκ_mem : κ ∈ μ
⊢ κ (K₁ᶜ ×ˢ univ) ≤ ε / 2

Tactic:
specialize hK₁_le _ <| mem_image_of_mem _ hκ_mem

Goal state after:
case h₁
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hK₁_le : κ.fst K₁ᶜ ≤ ε / 2
hκ_mem : κ ∈ μ
⊢ κ (K₁ᶜ ×ˢ univ) ≤ ε / 2
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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ f i x = Exists.choose ⋯ x → {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ f i x = g i x

pp: case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ x ∈ {x | C ≤ ‖g i x‖₊}

Tactic:
hx

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ Exists.choose ⋯ x = g i x

case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ x ∈ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : C ≤ ‖f i x‖₊
⊢ x ∈ {x | C ≤ ‖g i x‖₊}

Tactic:
hx

Goal state after:
case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : C ≤ ‖Exists.choose ⋯ x‖₊
⊢ x ∈ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : ¬C ≤ ‖f i x‖₊
⊢ x ∉ {x | C ≤ ‖g i x‖₊}

Tactic:
hx

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : ¬C ≤ ‖Exists.choose ⋯ x‖₊
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
⊢ IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ

Tactic:
peel 4
  refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩ <;>
  · filter_upwards [h, h'] with a ha h'a
    simpa [ha] using h'a

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s μ ↔ iIndep (fun i ↦ generateFrom {s i}) μ

Tactic:
by
  simp only [iIndepSet, iIndep, Kernel.iIndepSet]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
⊢ x ∈ {i, j} → (if x = i then t₁ else t₂) ∈ s x

Tactic:
hx

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx : x ∈ {i, j}
⊢ (if x = i then t₁ else t₂) ∈ s x
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx✝ : x ∈ {i, j}
hx : x ∈ {j}
⊢ (if x = i then t₁ else t₂) ∈ s x

Tactic:
· simp [Finset.mem_singleton.mp hx, hij.symm, ht₂]

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

Goal state before:
pp: Ω : 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
⊢ ∫ (x : Ω), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : Ω), f x ∂μs i) atTop

Tactic:
have same := lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
                  f.continuous f_nn h_opens

Goal state after:
Ω : 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
⊢ ∫ (x : Ω), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : Ω), f x ∂μs i) atTop
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∞
⊢ (∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n) → x ≤ ↑‖f‖₊

Tactic:
hx

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
⊢ x ≤ ↑‖f‖₊
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : 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 ν
⊢ (fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ Y ω.2

Tactic:
have : (fun ω ↦ mX.mk X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ mY.mk Y ω.2) :=
    indepFun_prod mX.measurable_mk mY.measurable_mk

Goal state after:
Ω : 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
⊢ (fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ Y ω.2