mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift' f)

pp: case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift' f)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (⋃ b, bif b then s else t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
totallyBounded_iUnion

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ (∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded

Tactic:
·

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded

Tactic:
·

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N

pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N

Tactic:
·

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N

Tactic:
·

Goal state after:
case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s

pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ (a, seq hf U_mem (max m n)) ∈ s

Tactic:
·

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ (a, seq hf U_mem (max m n)) ∈ s

Tactic:
·

Goal state after:
case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ (a, seq hf U_mem (max m n)) ∈ s
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K → ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

pp: case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K

Tactic:
·

Goal state after:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K → ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf Hmem m, SequentiallyComplete.seq hf Hmem n) ∈ U N

pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s

Tactic:
·

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf Hmem m, SequentiallyComplete.seq hf Hmem n) ∈ U N
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K

Tactic:
·

Goal state after:
case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s

Tactic:
·

Goal state after:
case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ u ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), IsOpen[uniformSpace.toTopologicalSpace] u

pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), a ∈ v ∧ v ⊆ u

Tactic:
·

Goal state after:
case refine_1
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ u ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), IsOpen[uniformSpace.toTopologicalSpace] u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), a ∈ v ∧ v ⊆ u

Tactic:
·

Goal state after:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: case hp
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
⊢ IsClosed[inst✝³.toTopologicalSpace] {x | (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x = SeparationQuotient.mk x}

pp: case h
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
a✝ : α
⊢ (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a✝) = SeparationQuotient.mk (i a✝)

Tactic:
·

Goal state after:
case hp
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
⊢ IsClosed[inst✝³.toTopologicalSpace] {x | (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x = SeparationQuotient.mk x}
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

pp: case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
·

Goal state after:
case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
a✝ : α
⊢ (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a✝) = SeparationQuotient.mk (i a✝)

Tactic:
·

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
a✝ : α
⊢ (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a✝) = SeparationQuotient.mk (i a✝)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ ∀ (x : α), (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)) (i x) = ff x

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ Continuous[inst✝³.toTopologicalSpace, _] (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ ∀ (x : α), (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)) (i x) = ff x