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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : (hausdorffEDist s t).toReal < (ENNReal.ofReal r).toReal
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r

Tactic:
ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffEDist s t < ENNReal.ofReal r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case hle
α : 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
⊢ min ε₁ ε₂ ≤ ε₁

Tactic:
norm_num

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

Goal state before:
pp: case hle
α : 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
⊢ min ε₁ ε₂ ≤ ε₂

Tactic:
norm_num

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

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∉ s
⊢ IsLUB {a | ∃ i, f' i b = a} (g b)

Tactic:
have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
      simp [A, hg' hb, isLUB_singleton]

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

Goal state before:
pp: case hnhds
α : 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
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U

Tactic:
· intro x hx
    have : {f x} ⊆ U := by rw [singleton_subset_iff]; exact hKU hx
    obtain ⟨δ, hδ, hthick⟩ := (isCompact_singleton (x := f x)).exists_thickening_subset_open ho this
    let V := f ⁻¹' (thickening (δ / 2) {f x})
    have : V ∈ 𝓝 x := by
      apply hf x hx
      apply isOpen_thickening.mem_nhds
      exact (self_subset_thickening (by positivity) _) rfl
    refine ⟨K ∩ (interior V), inter_mem_nhdsWithin K (interior_mem_nhds.mpr this),
      δ / 2, by positivity, V, by rw [← subset_interior_iff_mem_nhdsSet]; simp, ?_⟩
    calc thickening (δ / 2) (f '' V)
      _ ⊆ thickening (δ / 2) (thickening (δ / 2) {f x}) :=
        thickening_subset_of_subset _ (image_preimage_subset f _)
      _ ⊆ thickening ((δ / 2) + (δ / 2)) ({f x}) :=
        thickening_thickening_subset (δ / 2) (δ / 2) {f x}
      _ ⊆ U := by simp [hthick]

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x ↦ sSup ((fun i ↦ f i x) '' s)

Tactic:
simp_rw [image_eq_range]
  have : Countable s := hs.to_subtype
  exact .iSup fun i ↦ hf i i.2

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun i ↦ if p i then a else b) L F
i : ι
⊢ i ∈ (fun i ↦ if p i then a else b) ⁻¹' {b}ᶜ → (p i ↔ q)

Tactic:
hi

Goal state after:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun i ↦ if p i then a else b) L F
i : ι
hi : i ∈ (fun i ↦ if p i then a else b) ⁻¹' {b}ᶜ
⊢ p i ↔ q
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun i ↦ if p i then a else b) L G
i : ι
⊢ i ∈ (fun i ↦ if p i then a else b) ⁻¹' {a}ᶜ → (p i ↔ q)

Tactic:
hi

Goal state after:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun i ↦ if p i then a else b) L G
i : ι
hi : i ∈ (fun i ↦ if p i then a else b) ⁻¹' {a}ᶜ
⊢ p i ↔ q
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
i : ι
⊢ i ∈ s → Measurable (g i)

Tactic:
hi

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
i : ι
hi : i ∈ s
⊢ Measurable (g i)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:

Tactic:
f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
    _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ := by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
i : ι
⊢ (p i ↔ q) → (if q then a else b) = if p i then a else b

Tactic:
hi

Goal state after:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
i : ι
hi : p i ↔ q
⊢ (if q then a else b) = if p i then a else b
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ (∑' (b : ι), ↑(f b x)).toNNReal

Tactic:
exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

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

Goal state before:
pp: case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ ∀ (i : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1)))

Tactic:
· intro n
      exact hs.inter (hf measurableSet_Ico)

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

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable l.prod μ

Tactic:
induction l with

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
this✝¹ : r * s x ≠ 0
this✝ : s x ≠ 0
this : (SimpleFunc.map c rs) x < ⨆ n, f n x
⊢ x ∈ ⋃ i, {a | c (rs x) ≤ f i a}

Tactic:
rcases lt_iSup_iff.1 this with ⟨i, hi⟩

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
this✝¹ : r * s x ≠ 0
this✝ : s x ≠ 0
this : (SimpleFunc.map c rs) x < ⨆ n, f n x
i : ℕ
hi : (SimpleFunc.map c rs) x < f i x
⊢ x ∈ ⋃ i, {a | c (rs x) ≤ f i a}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a ↦ f a), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ g a), g_1.lintegral μ

Tactic:
refine iSup₂_le fun s hfs ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : ⇑s ≤ fun a ↦ f a
⊢ ⇑(s.restrict tᶜ) ≤ fun a ↦ g a

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : ⇑s ≤ fun a ↦ f a
⊢ s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x | f' x ≤ g x} (μ.restrict s)

Tactic:
exact nullMeasurableSet_le hf'm.aemeasurable hg

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

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

Tactic:
Measure.restrict_congr_set h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
h : s =ᵐ[μ] t
⊢ ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ AEStronglyMeasurable (s.piecewise f g) μ

Tactic:
refine ⟨s.piecewise (hf.mk f) (hg.mk g),
    StronglyMeasurable.piecewise hs hf.stronglyMeasurable_mk hg.stronglyMeasurable_mk, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ s.piecewise f g =ᵐ[μ] s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ x ∈ {x | f x ≠ 0} ↔ x ∈ ⋃ n, {x | u n ≤ f x}

Tactic:
rw [mem_iUnion, mem_ofPred_eq, ← pos_iff_ne_zero]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ 0 < f x ↔ ∃ i, x ∈ {x | u i ≤ f x}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), φ x ≤ C
s : Set α
hs : μ s < (ε₂ - ε₁) / ↑C
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁ ≤ (const α ↑C).lintegral (μ.restrict s) + ε₁

Tactic:
by
      gcongr
      exact fun x ↦ ENNReal.coe_le_coe.2 (hC x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 ((fun x ↦ (f x, g x)) x))

Tactic:
rw [nhds_prod_eq]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 (f x) ×ˢ 𝓝 (g x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

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

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val ⁻¹' u)

Tactic:
exact ⟨s ∩ u, hs u (hs_m.inter hu), by simp⟩

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ (Perfect (closure[inst✝¹] (U ∩ C)) ∧ (closure[inst✝¹] (U ∩ C)).Nonempty) ∧ closure[inst✝¹] (U ∩ C) ⊆ C

pp: case h.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ ((Perfect (closure[inst✝¹] (V ∩ C)) ∧ (closure[inst✝¹] (V ∩ C)).Nonempty) ∧ closure[inst✝¹] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))

Tactic:
· refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩
    rw [hC.closed.closure_subset_iff]
    exact inter_subset_right

Goal state after:
case h.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ ((Perfect (closure[inst✝¹] (V ∩ C)) ∧ (closure[inst✝¹] (V ∩ C)).Nonempty) ∧ closure[inst✝¹] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
C : Set α
inst✝² : T1Space α
inst✝¹ : ConnectedSpace α
inst✝ : Nontrivial α
⊢ univ.Nontrivial

Tactic:
Set.nontrivial_univ_iff

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
C : Set α
inst✝² : T1Space α
inst✝¹ : ConnectedSpace α
inst✝ : Nontrivial α
⊢ Nontrivial α
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
⊢ i ∈ t → ‖f i‖ ≤ g i

Tactic:
hi

Goal state after:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : ι), f n x) atTop s

Tactic:
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
  have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos
  simp only [eventually_atTop] at *
  obtain ⟨t, ht⟩ := this
  rw [eventually_iff_exists_mem] at hfu
  obtain ⟨N, hN, HN⟩ := hfu
  refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩
  have A : Summable fun n => ‖f n x‖ := by
    apply Summable.add_compl (s := hN.toFinset) Summable.of_finite
    apply Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) _ (hu.subtype _)
    simp only [comp_apply, Subtype.forall, Set.mem_compl_iff, Finset.mem_coe]
    aesop
  rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl n, add_sub_cancel_left]
  apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
  apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
  apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
  simp only [comp_apply, Subtype.forall]
  apply fun i hi => HN i ?_ x hx
  have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
  simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
have A n : u n ∈ s := h'u (mem_range_self _)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)

Tactic:
by
  rw [glueDist_comm]; apply le_glueDist_inl_inr

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

Goal state before:
pp: case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
⊢ i < n → z i = x i

Tactic:
hi

Goal state after:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
hi : i < n
⊢ z i = x i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
⊢ i < n → z i = y i

Tactic:
hi

Goal state after:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = y i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
i : ℕ
⊢ i < n → x i = y i

Tactic:
hi

Goal state after:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
i : ℕ
hi : i < n
⊢ x i = y i
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ i₀, ∀ (i : ι), t i ≤ t i₀
ht : ∀ (i : ι), PolishSpace α
⊢ PolishSpace α

Tactic:
rcases ht₀ with ⟨i₀, hi₀⟩
  rcases CompletePseudometrizable.iInf ⟨t i₀, letI := t i₀; haveI := ht i₀; inferInstance, hi₀⟩
    fun i ↦
      letI := t i; haveI := ht i; letI := upgradeIsCompletelyMetrizable α
      ⟨inferInstance, inferInstance, inferInstance, rfl⟩
    with ⟨u, hcomp, hcount, htop⟩
  rw [← htop]
  have : @SecondCountableTopology α u.toTopologicalSpace :=
    htop.symm ▸ secondCountableTopology_iInf fun i ↦ letI := t i; (ht i).toSecondCountableTopology
  have : @T1Space α u.toTopologicalSpace :=
    htop.symm ▸ t1Space_antitone (iInf_le _ i₀) (by let := t i₀; have := ht i₀; infer_instance)
  infer_instance

Goal state after:
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 : ℕ
⊢ i < n → y i = x i

Tactic:
hi

Goal state after:
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
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
⊢ 1 / 2 < 1

Tactic:
norm_num

Goal state after: