mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
h : ∀ (n_1 : ℕ), ∃ S, ↑S ⊆ memPartition t n ∧ f n_1 = ⋃₀ ↑S
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

Tactic:
choose S hS_subset hS_eq using h
      have : Fintype (⋃ n, (S n : Set (Set α))) := by
        refine (Finite.subset (finite_memPartition t n) ?_).fintype
        simp only [iUnion_subset_iff]
        exact hS_subset
      refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
      · simp only [coe_toFinset, iUnion_subset_iff]
        exact hS_subset
      · simp only [coe_toFinset, sUnion_iUnion, hS_eq]

Goal state after:
Module: Mathlib.MeasureTheory.Order.Lattice

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ Measurable fun x ↦ (range (n + 1)).sup' ⋯ fun k ↦ f k x

Tactic:
convert! Finset.measurable_range_sup' hf using 1

Goal state after:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ (fun x ↦ (range (n + 1)).sup' ⋯ fun k ↦ f k x) = (range (n + 1)).sup' ⋯ f
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ Measure.map g (Measure.map f μ) = Measure.map (g ∘ f) μ

Tactic:
ext1 s hs
  rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]

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

Goal state before:
pp: case basic
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u✝ u : Set α
hu : u ∈ s
⊢ MeasurableSet u

Tactic:
| basic u hu =>

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ MeasurableSet u

Tactic:
induction hu with

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)

Tactic:
let : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
mem_closure_iff_infEDist_zero,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x E ↔ ¬infEDist x E = 0
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
simp only [closedBall_eq_empty.mpr hδ, empty_subset]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x s = ⨅ y, dist x ↑y

Tactic:
rw [infDist, infEDist, iInf_subtype', ENNReal.toReal_iInf]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ⨅ i, (edist x ↑i).toReal = ⨅ y, dist x ↑y

α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x ↑i ≠ ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
exact ⟨y, hy, yr⟩

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

Goal state before:
pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
rcases hC with ⟨t, h1t, h2t⟩
      rw [← univ_prod, ← h2t, iUnion_prod_const]
      apply MeasurableSet.iUnion
      rintro n
      apply measurableSet_generateFrom
      exact mem_image2_of_mem (h1t n) hs

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range fun a ↦ Ioi ↑a) = generateFrom (range fun a ↦ Iic ↑a)

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Iic]; rw [← compl_Ioi]] <;>
  exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case hunion
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
⊢ (∃ g s, MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) →
    ∃ g s, MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
⟨g', s', s'_meas, t's', hg'⟩

Goal state after:
case hunion
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
⊢ ∃ g s, MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ FinStronglyMeasurable f μ

Tactic:
have : SigmaFinite (μ.restrict t) := htμ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
⊢ FinStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
n : ℕ
x : α
hxt : x ∉ t
⊢ (fs n) x = 0

Tactic:
SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
n : ℕ
x : α
hxt : x ∉ t
⊢ (S n ∩ t).indicator (⇑(f_approx n)) x = 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ μ t

Tactic:
rw [← lintegral_indicator hs]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ μ t
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = 0

Tactic:
by
  have : Subsingleton (Measure α) := inferInstance
  convert! lintegral_zero_measure f

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : μ s = 0
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0

Tactic:
convert! lintegral_zero_measure _
  exact Measure.restrict_eq_zero.2 hs'

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

Goal state before:
pp: case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

Tactic:
by_cases H : t = 0

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : t = 0
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure[inst✝] (⋃ n, range ⇑(hf.approx n)))
x : α
n : ℕ
⊢ (hf.approx n) x ∈ ⋃ n, range ⇑(hf.approx n)

Tactic:
apply mem_iUnion_of_mem n

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure[inst✝] (⋃ n, range ⇑(hf.approx n)))
x : α
n : ℕ
⊢ (hf.approx n) x ∈ range ⇑(hf.approx n)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (⨆ n, (eapprox f n).lintegral μ) + ⨆ n, (eapprox g n).lintegral μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
lintegral_eq_iSup_eapprox_lintegral hf,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (⨆ n, (eapprox f n).lintegral μ) + ⨆ n, (eapprox g n).lintegral μ =
    (⨆ n, (eapprox f n).lintegral μ) + ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞
⊢ MeasurableSet ∅

Tactic:
· exact MeasurableSet.empty

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
⊢ IsSeparable (range f)

Tactic:
have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.isSeparable_preimage H.isSeparable_range
    rwa [range_comp, hg.injective.preimage_image] at this

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure[inst✝³] (⋃ i, range (f (v i))))
x : α
n : ℕ
⊢ ((fun i ↦ f i x) ∘ v) n ∈ ⋃ i, range (f (v i))

Tactic:
apply mem_iUnion_of_mem n

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := ⋯
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure[inst✝³] (⋃ i, range (f (v i))))
x : α
n : ℕ
⊢ ((fun i ↦ f i x) ∘ v) n ∈ range (f (v n))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 : α
⊢ F a < ∞ → F a ≠ ∞

Tactic:
ha

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 : α
ha : F a < ∞
⊢ F a ≠ ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, (fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 0)

Tactic:
funext fun n => h_fs_zero n x hxt

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, (fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
a : α
⊢ (∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)) → Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))

Tactic:
ha

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
a : α
ha : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : α), f n x) atTop univ

Tactic:
exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x

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 : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
a : α
⊢ (∀ (i : ℕ), F a ≤ f i a) → F a ≤ f 0 a

Tactic:
ha

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
a : α
ha : ∀ (i : ℕ), F a ≤ f i a
⊢ F a ≤ f 0 a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
a : α
⊢ (∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)) → Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))

Tactic:
ha

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
a : α
ha : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀
u : ι → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
hut : ∀ (i : ι), (u i).toTopologicalSpace = t i
⊢ ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i

Tactic:
obtain rfl : t = fun i ↦ (u i).toTopologicalSpace := (funext hut).symm

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : Countable ι
u : ι → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), (fun i ↦ (u i).toTopologicalSpace) i ≤ t₀
hut : ∀ (i : ι), (u i).toTopologicalSpace = (fun i ↦ (u i).toTopologicalSpace) i
⊢ ∃ u_1,
    CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u_1.toTopologicalSpace = ⨅ i, (fun i ↦ (u i).toTopologicalSpace) i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff y x
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_le h)

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ MeasurePreserving f' μa μb

Tactic:
refine ⟨hf', ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ map f' μa = μb
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ (dirac x) A = (dirac y) A

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A

Tactic:
· simp only [Measure.dirac_apply' _ A_mble, x_in_A, indicator_of_mem, Pi.one_apply,
                 (h A A_mble).mp x_in_A]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (b.1 + b.2) s

Tactic:
simp_rw [Measure.coe_add, Pi.add_apply]

Goal state after:
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ b.1 s + b.2 s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable dirac

pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable f

Tactic:
exacts [measurable_dirac, hf]

Goal state after: