mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p

Tactic:
rw [← add_lt_add_iff_right p, add_assoc, add_comm b, ← sub_lt_iff_lt_add, add_comm (_ * _), ←
    sub_lt_iff_lt_add]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b - ↑⌊(a + p - b) / p⌋ * p < p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + toIcoDiv hp a b • p + p

Tactic:
convert! sub_lt_iff_lt_add.mp hr using 1

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.coinduced f (⨆ a, ↑a) = ⨆ a, TopologicalSpace.coinduced f ↑a

Tactic:
coinduced_iSup

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
⊢ ⨆ i, TopologicalSpace.coinduced f ↑i = ⨆ a, TopologicalSpace.coinduced f ↑a
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Continuous[inst✝⁴, inst✝⁵] g

Tactic:
by convert! f.symm.continuous

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsOpen[inst✝] (⇑h '' s) ↔ IsOpen[inst✝¹] s

Tactic:
← preimage_symm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsOpen[inst✝] (⇑h.symm ⁻¹' s) ↔ IsOpen[inst✝¹] s
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsClosed[inst✝] (⇑h '' s) ↔ IsClosed[inst✝¹] s

Tactic:
← preimage_symm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsClosed[inst✝] (⇑h.symm ⁻¹' s) ↔ IsClosed[inst✝¹] s
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h '' closure[inst✝¹] s = closure[inst✝] (⇑h '' s)

Tactic:
← preimage_symm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h.symm ⁻¹' closure[inst✝¹] s = closure[inst✝] (⇑h.symm ⁻¹' s)
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h '' interior s = interior (⇑h '' s)

Tactic:
← preimage_symm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h.symm ⁻¹' interior s = interior (⇑h.symm ⁻¹' s)
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h '' frontier s = frontier (⇑h '' s)

Tactic:
← preimage_symm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h.symm ⁻¹' frontier s = frontier (⇑h.symm ⁻¹' s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsEmbedding f ∧ IsClosed[inst✝] (g '' range f) ↔ IsEmbedding f ∧ IsClosed[inst✝¹] (range f)

Tactic:
← hg.isClosed_iff_image_isClosed

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ range f = g ⁻¹' range (g ∘ f)

Tactic:
range_comp,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ range f = g ⁻¹' g '' range f
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 (x, y)).HasBasis (fun i ↦ px i.1 ∧ py i.2) fun i ↦ sx i.1 ×ˢ sy i.2

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun i ↦ px i.1 ∧ py i.2) fun i ↦ sx i.1 ×ˢ sy i.2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 (y, x))

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 y ×ˢ 𝓝 x)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c ↦ (mx c, my c)) f (𝓝 (x, y))

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c ↦ (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 (y, w))

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
nhds_generateFrom,

Goal state after:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (⨅ s ∈ {s | a ∈ s ∧ s ∈ b}, 𝓟 s).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ range (Sum.elim f g ∘ inl) ⊆ C

Tactic:
range_comp,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ Sum.elim f g '' range inl ⊆ C
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ ⨅ i ∈ ⋃₀ 𝔖, induced (eval i) (T i) = ⨅ S ∈ 𝔖, ⨅ i ∈ S, induced (eval i) (T i)

Tactic:
iInf_sUnion

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' t ⊆ w

Tactic:
exact (inter_comm _ _).trans_subset <| (inter_subset_inter_left _ <| preimage_mono hv.2.1).trans
      (hw.2.trans_subset inter_subset_left)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 (x, y)).IsCountablyGenerated

Tactic:
nhds_prod_eq

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ 𝓝 ⟨i, x⟩ = comap f (𝓝 (f ⟨i, x⟩))

Tactic:
rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]

Goal state after:
case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ range (Sigma.mk i) ∈ comap f (𝓝 (f ⟨i, x⟩))
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
S : Set (Set α)
H : ∀ s ∈ S, IsOpen[t] s
⊢ ∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Tactic:
simpa only [and_left_comm, sUnion_eq_biUnion] using! isOpen_biUnion_countable S id H

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
rcases countable_cover_nhds this with ⟨t, htc, htU⟩

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ a_1 ∈ (fun x ↦ a ↑x) '' T, a_1

Tactic:
rw [biUnion_image, hT]

Goal state after:
case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ i, a ↑i
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, s i = ⋃ i, ⋃ n, K i n

Tactic:
by simp_rw [hcov]

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

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = f <$> s <*> t

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃ i ∈ S, i = ⋃ a ∈ S, A ↓∩ a

Tactic:
preimage_iUnion

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ici a) = Ici (f a)

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ioi a) = Ioi (f a)

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ↑(upperClosure s) = ⋃ a ∈ s, Ici a

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ⨅ a ∈ s, Ici a = upperClosure s

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ upperClosure {a} = UpperSet.Ici a

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

Tactic:
by
  refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩
  rw [← h]
  exact (UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ map (OrderIso.refl α) = OrderIso.refl (UpperSet α)

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ a ∈ s, ⨆ b ∈ t, 𝓝 (a, b) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y

Tactic:
nhds_prod_eq

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
⊢ (map g) ((map f) s) = (map (f.trans g)) s

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) s x

Tactic:
· rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢
    rcases hx with hx | hx
    · apply ContinuousWithinAt.union
      · exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
      · have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
    · apply ContinuousWithinAt.union
      · have : x ∉ closure { a | p a } := fun h =>
          hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
      · exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x y : X
e : flip (fun x1 x2 ↦ x1 ⤳ x2) (f y) (f x)
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
exact ⟨_, hf.specializes_iff.mp e, rfl⟩

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x y : X
e : f y ⤳ f x
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
exact ⟨_, hf.specializes_iff.mp e, rfl⟩

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 (x, y)

Tactic:
nhds_prod_eq

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (mk x) ×ˢ 𝓝 (mk y) = 𝓝 (mk x, mk y)

Tactic:
nhds_prod_eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (mk x) ×ˢ 𝓝 (mk y) = 𝓝 (mk x) ×ˢ 𝓝 (mk y)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
← map_prod_map_mk_nhds,

Goal state after:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y))) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y) ⊓ 𝓟 s) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
← map_prod_map_mk_nhds,

Goal state after:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y)) ⊓ 𝓟 s) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous[inst✝¹, inst✝] f ↔ Continuous[inst✝¹, inst✝] g

Tactic:
by
  simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]
  exact continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
E : Set X
h : ∀ x ∈ E, ¬AccPt x (𝓟 E)
⊢ DiscreteTopology ↑E

Tactic:
by
  simpa [discreteTopology_subtype_iff, AccPt] using h

Goal state after:
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case a.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst✝¹] ↑t
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}

Tactic:
rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩

Goal state after:
case a.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst✝¹] ↑t
x : X
hxt : x ∈ ↑t
hxo : IsOpen[inst✝¹] {x}
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
intro hfg

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x