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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (t \ s)

Tactic:
measure_inter_add_sdiff₀ _ ht,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ s = μ (s ∩ t) + μ (t \ s)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
then

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ (s \ tᶜ) = μ s

Tactic:
measure_sdiff_null ht

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ s = μ s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), SFinite (m n)
⊢ SFinite (sum fun i ↦ m i)

Tactic:
← sum_sfiniteSeq (m _),

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), SFinite (m n)
⊢ SFinite (sum fun i ↦ sum (sfiniteSeq (m i)))
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite ((μ.trim hm).trim hm₂)
⊢ SigmaFinite (μ.trim hm)

Tactic:
exact ⟨⟨
    { set := spanningSets ((μ.trim hm).trim hm₂)
      set_mem := fun _ => Set.mem_univ _
      finite := fun i => measure_spanningSets_trim_lt_top hm₂ (μ.trim hm) i
      spanning := iUnion_spanningSets _ }⟩⟩

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ memPartitionSet f (n + 1) a

Tactic:
memPartitionSet_succ

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : (⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)

Tactic:
then

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : (⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᵐ[μ.restrict sᶜ] g

Tactic:
by
  rw [ae_restrict_eq hs.compl]
  exact (piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right

Goal state after:
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:
| iUnion f _ h =>

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

Goal state before:
pp: case e_f
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
i : ι
⊢ ∑' (C : ↑(G i)), (μ.restrict (P ↑C)) t = ∑' (b : Finset ι), (G i).indicator (fun C ↦ (μ.restrict (P C)) t) b

Tactic:
rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ioc x a)) atBot (𝓝 (μ (Iic a)))

Tactic:
rw [← iUnion_Ioc_left]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ioc x a)) atBot (𝓝 (μ (⋃ b, Ioc b a)))
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ s ⊆ ⋃ n, (closure[inst✝¹] (g' n))ᶜ

Tactic:
← compl_iInter,

Goal state after:
case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ s ⊆ (⋂ i, closure[inst✝¹] (g' i))ᶜ
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case negSucc
α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x ↦ x ^ Int.negSucc n

Tactic:
zpow_negSucc

Goal state after:
case negSucc
α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x ↦ (x ^ (n + 1))⁻¹
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
⊢ OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen[inst✝¹] s → MeasurableSet s

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩
  exact OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEDist x t ≤ r
H2 : ∀ x ∈ t, infEDist x s ≤ r
⊢ (∀ i ∈ s, infEDist i t ≤ r) ∧ ∀ i ∈ t, infEDist i s ≤ r

Tactic:
exact ⟨H1, H2⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
⊢ hausdorffEDist s t ≤ r

Tactic:
by
  refine hausdorffEDist_le_of_infEDist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
  · rcases H1 x xs with ⟨y, yt, hy⟩
    exact le_trans (infEDist_le_edist_of_mem yt) hy
  · rcases H2 x xt with ⟨y, ys, hy⟩
    exact le_trans (infEDist_le_edist_of_mem ys) hy

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infDist x s = 0

Tactic:
rw [← infDist_closure]
  exact infDist_zero_of_mem hx

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
rcases hne with ⟨z, hz⟩
  rw [← infDist_inter_closedBall_of_mem hz]
  set t := s ∩ closedBall x (dist z x)
  have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
  have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
  obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x
  exact ⟨y, hys, hyd⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (f a)} = ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}
⊢ MeasurableSet (⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b})

Tactic:
exact
    MeasurableSet.biUnion f.finite_range.countable fun b _ =>
      MeasurableSet.inter (h b) (f.measurableSet_fiber _)

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

Goal state before:
pp: case hmono
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U

Tactic:
exact fun s t hst ⟨ε, hε, V, hV, hthickening⟩ ↦ ⟨ε, hε, V, nhdsSet_mono hst hV, hthickening⟩

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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableSet (range (Prod.map g f))

Tactic:
range_prodMap

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableSet (range g ×ˢ range f)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ↑(↑q).toNNReal ≤ f a), ↑(↑q).toNNReal

Tactic:
exact le_iSup_of_le (le_of_lt q_lt) le_rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f * g).FinMeasSupp μ

Tactic:
mul_eq_map₂

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p ↦ p.1 * p.2) (f.pair g)).FinMeasSupp μ
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ Tendsto (fun i ↦ (As i).indicator (fun x ↦ b) x) L (𝓝 (A.indicator (fun x ↦ b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
  · convert! heart
    by_cases hxA : x ∈ A <;> simp [hxA]
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ MeasurableSet (g ⁻¹' s)

Tactic:
have : Measurable fun x => infNndist (g x) s := by
    suffices Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s) from
      NNReal.measurable_of_tendsto' u (fun i => (hf i).infNndist) this
    rw [tendsto_pi_nhds] at lim ⊢
    intro x
    exact ((continuous_infNndist_pt s).tendsto (g x)).comp (lim x)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x ↦ infNndist (g x) s
⊢ MeasurableSet (g ⁻¹' s)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ N + 1

pp: case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ (nearestPtInd e N) x ≤ N + 1

Tactic:
exacts [le_rfl, ihN.trans N.le_succ]

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

Goal state before:
pp: case refine_1
α : 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)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ μ (⇑(fs n) ⁻¹' {y}) < ∞

Tactic:
rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]

Goal state after:
case refine_1
α : 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)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ μ (S n ∩ t ∩ ⇑(f_approx n) ⁻¹' {y}) < ∞

case refine_1
α : 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)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ y ≠ 0
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)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ x ∈ univ

Tactic:
trivial

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦
    lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij)
  suffices key : ∫⁻ x, F x ∂μ = ⨅ n, ∫⁻ x, f n x ∂μ by
    rw [key]
    exact tendsto_atTop_iInf this
  rw [← lintegral_iInf' hf h_anti h0]
  refine lintegral_congr_ae ?_
  filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto
    using tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)

Goal state after:
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 μ + (eapprox g n).lintegral μ =
    (⨆ n, (eapprox f n).lintegral μ) + ⨆ n, (eapprox g n).lintegral μ

Tactic:
refine (ENNReal.iSup_add_iSup_of_monotone ?_ ?_).symm <;>
        · intro i j h
          exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ

pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ →
            ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ →
              ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ

Tactic:
· intro c s hs
    rw [lintegral_indicator hs, lintegral_indicator (hm s hs), setLIntegral_const,
      setLIntegral_const]
    suffices h_trim_s : μ.trim hm s = μ s by rw [h_trim_s]
    exact trim_measurableSet_eq hm hs

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ →
            ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ →
              ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty β
inst✝ : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun x ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun x_1 ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
⊢ P f hf

Tactic:
by
  let s := hf.approx
  refine lim (fun n ↦ (s n).stronglyMeasurable) hf (fun n ↦ ?_) hf.tendsto_approx
  induction s n with
  | const c => exact const c
  | @pcw f g s hs Pf Pg =>
    simp_rw [SimpleFunc.coe_piecewise]
    exact pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
⊢ CauchySeq fun n ↦ ∑ i ∈ range n, f i

Tactic:
refine Metric.cauchySeq_iff'.2 fun ε hε => ?_
  refine (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_
  specialize hg n hn
  rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢
  calc
    ‖∑ k ∈ Ico N n, f k‖ ≤ ∑ k ∈ _, ‖f k‖ := norm_sum_le _ _
    _ ≤ ∑ k ∈ _, g k := sum_le_sum fun x _ => hf x
    _ ≤ ‖∑ k ∈ _, g k‖ := le_abs_self _
    _ < ε := hg

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
h : Sum.dist p q = 0
⊢ p = q

Tactic:
rcases p with p | p

Goal state after:
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : X
h : Sum.dist (Sum.inl p) q = 0
⊢ Sum.inl p = q

case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : Y
h : Sum.dist (Sum.inr p) q = 0
⊢ Sum.inr p = q
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_2
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' cylinder (↑x) n)

Tactic:
apply continuous_subtype_val.isOpen_preimage

Goal state after:
case refine_2
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
⊢ IsOpen[Pi.topologicalSpace] (cylinder (↑x) n)