mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
g.lintegral_eq_lintegral

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case mk
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, StronglyMeasurable f
⊢ StronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M))) l))

Tactic:
simpa using l.stronglyMeasurable_prod (by simpa using hl)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))), ν (μ.sigmaFiniteSetWRT' ν) ≤
    ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetWRT' ν)
      measurableSet_sigmaFiniteSetWRT'

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ f ≤ᵐ[μ.trim hm] g

Tactic:
EventuallyLE,

Goal state after:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ ∀ᵐ (x : α) ∂μ.trim hm, f x ≤ g x
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
⊢ ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
let ⟨K, t, ht, hf⟩ := hf hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf✝ : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
K : ℝ≥0
t : Set α
ht : t ∈ nhdsWithin x s
hf : LipschitzOnWith K f t
⊢ ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
h : i ≤ j * i
⊢ i = 0 ∨ j = 1

Tactic:
by
  contrapose! h
  rw [← unitInterval.lt_one_iff_ne_one, ← coe_lt_one, ← unitInterval.pos_iff_ne_zero,
    ← coe_pos] at h
  rw [← Subtype.coe_lt_coe, coe_mul]
  simpa using mul_lt_mul_of_pos_right h.right h.left

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
by
  have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f n ∧ ∫⁻ a, f n a ∂μ = ∫⁻ a, g a ∂μ :=
    fun n ↦ exists_measurable_le_lintegral_eq _ _
  choose g gmeas gf hg using this
  let g' : ℕ → α → ℝ≥0∞ := Nat.rec (g 0) (fun n I x ↦ max (g (n + 1) x) (I x))
  have M n : Measurable (g' n) := by
    induction n with
    | zero => simp [g', gmeas 0]
    | succ n ih => exact Measurable.max (gmeas (n + 1)) ih
  have I : ∀ n x, g n x ≤ g' n x := by
    intro n x
    cases n with | zero | succ => simp [g']
  have I' : ∀ᵐ x ∂μ, ∀ n, g' n x ≤ f n x := by
    filter_upwards [hf_mono] with x hx n
    induction n with
    | zero => simpa [g'] using gf 0 x
    | succ n ih => exact max_le (gf (n + 1) x) (ih.trans (hx (Nat.le_succ n)))
  have Int_eq n : ∫⁻ x, g' n x ∂μ = ∫⁻ x, f n x ∂μ := by
    apply le_antisymm
    · apply lintegral_mono_ae
      filter_upwards [I'] with x hx using hx n
    · rw [hg n]
      exact lintegral_mono (I n)
  have : ∀ᵐ a ∂μ, Tendsto (fun i ↦ g' i a) atTop (𝓝 (F a)) := by
    apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
    · exact fun n ↦ (M n).aemeasurable
    · simp_rw [Int_eq]
      exact hf_tendsto
    · exact Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))
    · filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)
  filter_upwards [this, I', h_bound] with x hx h'x h''x
  exact tendsto_of_tendsto_of_tendsto_of_le_of_le hx tendsto_const_nhds h'x h''x

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Ici ↑x = Icc x 1

Tactic:
rw [preimage_subtype_val_Ici]

Goal state after:
x : ↑I
⊢ Ici x = Icc x 1
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + dist y z + ε

Tactic:
add_le_add_iff_right

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ ⨅ p, dist x (Φ p) + dist z (Ψ p) ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + dist y z
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := ⋯.comapPseudoMetricSpace
⊢ CompleteSpace X

Tactic:
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := ⋯.comapPseudoMetricSpace
⊢ IsComplete (range f)
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ CompleteSpace X

Tactic:
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ IsComplete (range f)
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ CompleteSpace α

Tactic:
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ IsComplete (range f)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (a : α) in g ⁻¹' g '' s, f (g a) ∂μ

Tactic:
Set.preimage_image_eq _ hge.injective

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (a : α) in s, f (g a) ∂μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
x : ↑t
⊢ F x ∈ ⋂ n, s n

Tactic:
refine mem_iInter.2 fun n => ?_

Goal state after:
case h₁
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
x : ↑t
n : ι
⊢ F x ∈ s n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 0
⊢ μ = 0 ∨ IsProbabilityMeasure μ

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 1
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
· apply Or.inl (measure_univ_eq_zero.mp h)

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 1
⊢ μ = 0 ∨ IsProbabilityMeasure μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 1
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
· exact Or.inr ⟨h⟩

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ x ∈ t

Tactic:
refine mem_iInter.2 fun n => ?_

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
n : ι
⊢ x ∈ {x | f n (x n) = f i₀ (x i₀)}
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ (∀ᵐ (a : α) ∂μ, a = a₁ ∨ a = a₂) ↔ μ = μ {a₁} • dirac a₁ + μ {a₂} • dirac a₂

Tactic:
convert! ae_mem_finset_iff (s := .cons a₁ { a₂ } <| by simpa)

Goal state after:
case e'_1.e'_2
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
x✝ : α
⊢ x✝ = a₁ ∨ x✝ = a₂ ↔ x✝ ∈ Finset.cons a₁ {a₂} ⋯

case e'_2
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ μ {a₁} • dirac a₁ + μ {a₂} • dirac a₂ = ∑ a ∈ Finset.cons a₁ {a₂} ⋯, μ {a} • dirac a
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I✝ :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
I : (↑(F (p n))).2.1 m = (↑(p n)).2.1 m
⊢ (↑(p (n + 1))).2.1 m = (↑(p (m + 1))).2.1 m

Tactic:
rw [prec, I, IH]

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

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
this :
  ∀ {f : α → ℝ≥0∞},
    AEMeasurable f m.join → Measurable f → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
hfg : f =ᵐ[m.join] g
⊢ ∫⁻ (a : α), g a ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
this hgm.aemeasurable hgm

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
this :
  ∀ {f : α → ℝ≥0∞},
    AEMeasurable f m.join → Measurable f → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
hfg : f =ᵐ[m.join] g
⊢ ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m
⊢ Monotone fun n μ ↦ ∑ r ∈ (SimpleFunc.eapprox f n).range, r * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {r})

Tactic:
· exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
⊢ {p | edist p.1 p.2 < ε} ∈ ⨅ i, ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 i) (a.2 i) < i_1}

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ δ * K.card < ε / 2 :=
        ENNReal.exists_pos_mul_lt (by simp) (by simpa using hε.ne')

Goal state after:
case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
⊢ {p | edist p.1 p.2 < ε} ∈ ⨅ i, ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 i) (a.2 i) < i_1}
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I✝ :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
I : (↑(F (p n))).2.2 m = (↑(p n)).2.2 m
⊢ (↑(p (n + 1))).2.2 m = (↑(p (m + 1))).2.2 m

Tactic:
rw [prec, I, IH]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
x✝ : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ ∫⁻ (x : α) in ⋃ n, S n, f x ∂μ ≤ ⨆ n, ∫⁻ (x : α) in S n, f x ∂μ

Tactic:
rw [setLIntegral_iUnion_of_directed]

Goal state after:
case hd
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
x✝ : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) S
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case const.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ < ∞

pp: case const.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ L < ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ

Tactic:
· simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', ENNReal.mul_lt_top ENNReal.coe_lt_top t_top]

Goal state after:
case const.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ L < ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
⊢ (m.bind f).bind g = m.bind fun a ↦ (f a).bind g

Tactic:
by
  ext1 s hs
  rw [bind_apply hs hg, lintegral_bind hf, bind_apply hs]
  · exact lintegral_congr_ae <| (hf.ae_of_bind hg).mono fun a ha ↦ .symm <| bind_apply hs ha
  · exact (aemeasurable_bind hg).comp_aemeasurable hf
  · exact (measurable_coe hs).comp_aemeasurable hg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
this : Measurable fun x ↦ c * ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x ↦ ∫⁻ (y : β), (Prod.mk x ⁻¹' s).indicator ((fun x ↦ c) ∘ Prod.mk x) y ∂ν

Tactic:
simpa [lintegral_indicator (m hs)]

Goal state after: