mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E

Tactic:
cthickening_eq_iInter_cthickening' s hsδ hs E

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ ⋂ ε ∈ s, cthickening ε E
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), thickening ε E

Tactic:
by
  apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset
  simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]
  exact fun _ hε => nonempty_Ioc.mpr hε

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

Goal state before:
pp: case refine_3
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Tactic:
· rintro _ ⟨l, -, u, -, hlt, rfl⟩
    exact hμ hlt

Goal state after:
case refine_4
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg.h₂
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
· rw [← cthickening_of_nonpos δ_nonpos E]
    exact biInter_subset_of_mem hδs

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

Goal state before:
pp: case refine_3
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l ≤ u ∧ Icc l u = S}, μ s = ν s

Tactic:
· rintro _ ⟨l, -, u, -, hlt, rfl⟩
    exact hμ hlt

Goal state after:
case refine_4
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l ≤ u ∧ Icc l u = S}, μ s = ν s
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case hunion
α : 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 α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U

Tactic:
calc thickening (ε₁ ⊓ ε₂) (f '' V₁) ∪ thickening (ε₁ ⊓ ε₂) (f '' V₂)
      _ ⊆ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) := by gcongr <;> norm_num
      _ ⊆ U ∪ U := by gcongr
      _ = U := union_self _

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

Goal state before:
pp: case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' ↦ IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : {a | ∃ i, mk (f i) ⋯ b = a} = {a | ∃ i, f i b = a}
⊢ IsLUB {a | ∃ i, mk (f i) ⋯ b = a} (g b)

Tactic:
h_set_eq

Goal state after:
case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' ↦ IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : {a | ∃ i, mk (f i) ⋯ b = a} = {a | ∃ i, f i b = a}
⊢ IsLUB {a | ∃ i, f i b = a} (g b)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
⊢ ∀ t ∈ range fun a ↦ Ioi ↑a, MeasurableSet t

Tactic:
rintro _ ⟨q, rfl⟩

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet ((fun a ↦ Ioi ↑a) q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
⊢ ∀ t ∈ range fun a ↦ Iic ↑a, MeasurableSet t

Tactic:
rintro _ ⟨q, rfl⟩

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet ((fun a ↦ Iic ↑a) q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
⊢ ∀ t ∈ range fun a ↦ Iio ↑a, MeasurableSet t

Tactic:
rintro _ ⟨q, rfl⟩

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet ((fun a ↦ Iio ↑a) q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
⊢ ∀ t ∈ range fun a ↦ Ici ↑a, MeasurableSet t

Tactic:
rintro _ ⟨q, rfl⟩

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet ((fun a ↦ Ici ↑a) q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ IsPiSystem (⋃ a, {Ioi ↑a})

Tactic:
convert! isPiSystem_image_Ioi (((↑) : ℚ → ℝ) '' univ)

Goal state after:
⊢ ⋃ a, {Ioi ↑a} = Ioi '' Rat.cast '' univ
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
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ AEMeasurable g μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
⊢ AEMeasurable g μ

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ AEMeasurable g μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
⊢ Tendsto (fun i ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᵐ[μ] aeSeqLim

Tactic:
· simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᵐ[μ] aeSeqLim
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p ↦ f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r ↦ f (⊥, ↑r)
h_top_left : Measurable fun r ↦ f (⊤, ↑r)
h_bot_right : Measurable fun r ↦ f (↑r, ⊥)
h_top_right : Measurable fun r ↦ f (↑r, ⊤)
⊢ Measurable f

Tactic:
by
  refine measurable_of_real_prod ?_ ?_ ?_
  · refine measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right
    exact h_real.comp measurable_swap
  · exact measurable_of_measurable_real h_bot_left
  · exact measurable_of_measurable_real h_top_left

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
rcases eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ | h₀

Goal state after:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {a | f a ≤ g a} μ

Tactic:
apply
    (hf.stronglyMeasurable_mk.measurableSet_le hg.stronglyMeasurable_mk).nullMeasurableSet.congr
  filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
  change (hf.mk f x ≤ hg.mk g x) = (f x ≤ g x)
  simp only [hfx, hgx]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
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})
h_lt_top : (μ.restrict t) (spanningSets (μ.restrict t) n) < ∞
⊢ μ (S n ∩ t) < ∞

Tactic:
Measure.restrict_apply' 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})
h_lt_top : μ (spanningSets (μ.restrict t) n ∩ t) < ∞
⊢ μ (S n ∩ t) < ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
congr
    exact funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n)

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))
this : Antitone fun n ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
by
    rw [key]
    exact tendsto_atTop_iInf this

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 μ) + ⨆ n, (eapprox g n).lintegral μ =
    (⨆ n, (eapprox f n).lintegral μ) + ∫⁻ (a : α), g a ∂μ

Tactic:
lintegral_eq_iSup_eapprox_lintegral hg

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 μ) + ⨆ n, (eapprox g n).lintegral μ
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 : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (range g)

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩

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 : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ IsSeparable (range g)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
t : Set α
ht :
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), ν t
ht_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
⊢ (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

Tactic:
simp only [ht_meas, ht_mem, iSup_true] at ht

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
t : Set α
ht_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
ht : (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n < ν t
⊢ (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PerfectSpace α
U : Set α
hU : IsOpen[inst✝¹] U
⊢ Preperfect U

Tactic:
by
  simpa using PerfectSpace.univ_preperfect.open_inter hU

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Ici x = Icc x 1

Tactic:
exact Icc_top.symm

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case h
α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : ↑unitInterval
⊢ ↑s * (1 - ↑t) ≤ 1 - ↑s * ↑t

Tactic:
nlinarith [s.2.2]

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

Goal state before:
pp: case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n → cylinder y n = cylinder x n

Tactic:
intro hy

Goal state after:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n = cylinder x n
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
intro hy

Goal state after:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
⊢ n ≤ firstDiff y x
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 : Y
x✝ : X ⊕ Y
r : X
⊢ Sum.dist (Sum.inr p) (Sum.inl r) ≤ Sum.dist (Sum.inr p) x✝ + Sum.dist x✝ (Sum.inl r)

Tactic:
by
      simp only [Sum.dist_eq_glueDist r p]
      exact glueDist_triangle _ _ _ (by simp) _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist ↑x ↑y + |(infDist (↑x) (↑s)ᶜ)⁻¹ - (infDist (↑y) (↑s)ᶜ)⁻¹| < ε → y ∈ t
⊢ ↑x ∉ (↑s)ᶜ

Tactic:
mem_compl_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist ↑x ↑y + |(infDist (↑x) (↑s)ᶜ)⁻¹ - (infDist (↑y) (↑s)ᶜ)⁻¹| < ε → y ∈ t
⊢ ¬↑x ∉ ↑s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x ⋯.some + 1 + 0 + (0 + 0 + dist ⋯.some z) ≤
    dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]

Goal state after: