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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) (μ.sigmaFiniteSetWRT ν)ᶜ = 0
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 ↦ 0) atTop (𝓝 0)

Tactic:
]

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.Topology.Perfect

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure[inst✝¹] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure[inst✝¹] C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst✝ : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ ¬μ t = 0 → μ t = ∞

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst✝ : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ ¬μ t = 0 → μ t = ∞
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
⊢ ∃ x ∈ C, x ≠ y

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
⊢ ∃ x ∈ C, x ≠ y
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ μ (s ∩ μ.sigmaFiniteSetᶜ) = ∞

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ μ (s ∩ μ.sigmaFiniteSetᶜ) = ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT μ))

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT μ))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2.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
n : ℕ
⊢ μ (T n ∩ ⋃ b, T b) < ∞

Tactic:
]

Goal state after:
case refine_2.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
n : ℕ
⊢ μ (T n ∩ ⋃ b, T b) < ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2.refine_2
α : 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
⊢ tᶜ ∪ ⋃ i, T i = univ

Tactic:
]

Goal state after:
case refine_2.refine_2
α : 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
⊢ tᶜ ∪ ⋃ i, T i = univ
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

Tactic:
]

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

Goal state before:
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:
]

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.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MulZeroClass β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f * g) μ

Tactic:
refine
    ⟨fun n => hf.approx n * hg.approx n, ?_, fun x =>
      (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩
  intro n
  exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)

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)
⊢ U ∩ C ⊆ C

Tactic:
]

Goal state after:
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)
⊢ U ∩ C ⊆ C
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.right.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)
⊢ V ∩ C ⊆ C

Tactic:
]

Goal state after:
case h.right.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)
⊢ V ∩ C ⊆ C
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : SubtractionMonoid β
inst✝ : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support ⇑(hf.approx n)) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : SubtractionMonoid β
inst✝ : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support ⇑(hf.approx n)) < ∞
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝¹] t →
      IsClosed[inst✝¹] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝¹] t →
      IsClosed[inst✝¹] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁴ : TopologicalSpace β
𝕜 : Type u_5
inst✝³ : TopologicalSpace 𝕜
inst✝² : Zero β
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support (c • ⇑(hf.approx n))) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁴ : TopologicalSpace β
𝕜 : Type u_5
inst✝³ : TopologicalSpace 𝕜
inst✝² : Zero β
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support (c • ⇑(hf.approx n))) < ∞
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : AccPt x (𝓟 U)
⊢ AccPt x (𝓟 U)
Module: Mathlib.Topology.Perfect

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

Tactic:
]

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
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b ∈ t, f b ∈ ball 0 i) ↔
    ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b ∈ t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b ∈ t, f b ∈ ball 0 i) ↔
    ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b ∈ t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ ∀ x ∈ D, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ D, y ≠ x

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ ∀ x ∈ D, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ D, y ≠ x
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
⊢ (∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε) ↔
    ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun i ↦ U i x) atTop (𝓝 (u x.1 x.2))

Tactic:
]

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun i ↦ U i x) atTop (𝓝 (u x.1 x.2))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ C = C

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ≠ ∅

Tactic:
]

Goal state after:
case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ≠ ∅
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Tactic:
]

Goal state after:
case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
V : Set α
hunc : ¬V.Countable
D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Tactic:
]

Goal state after:
case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
V : Set α
hunc : ¬V.Countable
D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D

Tactic:
]

Goal state after:
case right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D
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
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x // x ∉ t }), u ↑a < ε
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ t }), f (↑x_1) x‖ < ε

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x // x ∉ t }), u ↑a < ε
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ t }), f (↑x_1) x‖ < ε
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
ε : ℝ
hε : ε > 0
N n : ℕ
hg : ‖∑ k ∈ Ico N n, g k‖ < ε
hn : n ≥ N
⊢ ‖∑ k ∈ Ico N n, f k‖ < ε

Tactic:
]

Goal state after:
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
ε : ℝ
hε : ε > 0
N n : ℕ
hg : ‖∑ k ∈ Ico N n, g k‖ < ε
hn : n ≥ N
⊢ ‖∑ k ∈ Ico N n, f k‖ < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
this : (fun p ↦ u (↑p.1) p.2) = (fun p ↦ u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable fun p ↦ u (↑p.2) p.1

Tactic:
]

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
this : (fun p ↦ u (↑p.1) p.2) = (fun p ↦ u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable fun p ↦ u (↑p.2) p.1
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s ↦ ∑ b ∈ s, f b

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s ↦ ∑ b ∈ s, f b
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 : ∃ v ∈ cofinite, ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
]

Goal state after:
β : 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 : ∃ v ∈ cofinite, ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε