mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : c.pt ⟶ X), h ≫ f_1 = h ≫ g) → f_1 = g

Tactic:
refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
huv : ∀ (h : c.pt ⟶ x✝⁴), h ≫ x✝² = h ≫ x✝¹
x✝ : C
h : ObjectProperty.ofObj f x✝
g : x✝ ⟶ x✝⁴
⊢ g ≫ x✝² = g ≫ x✝¹
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g

Tactic:
refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
huv : ∀ (h : x✝³ ⟶ c.pt), x✝² ≫ h = x✝¹ ≫ h
x✝ : C
h : ObjectProperty.ofObj f x✝
g : x✝³ ⟶ x✝
⊢ x✝² ≫ g = x✝¹ ≫ g
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
by
    apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse
    apply IsTerminal.ofIso this
    refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm
    apply HasColimit.isoOfNatIso
    exact Functor.isoWhiskerLeft _
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow c.pt).isoCompInverse

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)

Tactic:
exact Over.isoMk (hc.coconePointUniqueUpToIso isc) (hc.hom_ext fun i => by simp)

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
by
    simp_rw [lt_iff_le_not_ge]
    grind

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
a : ↥(AddSubgroup.zmultiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
hf : Periodic f c
x : α
m : ℤ
⊢ f (⟨(fun x ↦ x • c) m, ⋯⟩ +ᵥ x) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
a : ↥(AddSubmonoid.multiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
x : α
m : ℕ
⊢ f (⟨(fun i ↦ i • c) m, ⋯⟩ +ᵥ x) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k) • c) = ↑(2 * k).negOnePow • f x

pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k + 1) • c) = ↑(2 * k + 1).negOnePow • f x

Tactic:
· rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k + 1) • c) = ↑(2 * k + 1).negOnePow • f x
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∃ a, ∀ (b : ℕ), a ≤ b → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → p b

Tactic:
choose! N hN using hp

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → p b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr
m n : ℕ
⊢ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)

Tactic:
← totient_eq_one_iff

Goal state after:
case mpr
m n : ℕ
⊢ φ m = 1 ∨ φ n = 1 → (φ m).Coprime (φ n)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + m • p) b = m • p + toIocMod hp a b

Tactic:
toIocMod_add_zsmul',

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a b + m • p = m • p + toIocMod hp a b
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∉ closure[inst✝] s ↔ 𝓝[s] x = ⊥

Tactic:
mem_closure_iff_nhdsWithin_neBot,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ ¬(𝓝[s] x).NeBot ↔ 𝓝[s] x = ⊥
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p x ∈ U

Tactic:
rw [← hg ((congr_fun h y).trans e')]

Goal state after:
case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p y ∈ U
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X → Y
he : IsHomeomorph e
f : Y → Z
s : Set Z
⊢ f ∘ e '' closure[inst✝¹] (f ∘ e ⁻¹' s) = f '' closure[inst✝] (f ⁻¹' s)

Tactic:
by
  simp only [Set.preimage_comp, Set.image_comp, he.image_closure,
    Set.image_preimage_eq _ he.surjective]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝] (s ∩ range f)

Tactic:
inter_eq_self_of_subset_left hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝] s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : x ∉ closure[inst✝¹] s
⊢ ContinuousWithinAt f s x

Tactic:
mem_closure_iff_nhdsWithin_neBot,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : ¬(𝓝[s] x).NeBot
⊢ ContinuousWithinAt f s x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ a ∈ closure[inst✝¹] s ∧ b ∈ closure[inst✝] t

Tactic:
mem_closure_iff_nhdsWithin_neBot,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (𝓝[s ×ˢ t] (a, b)).NeBot ↔ (𝓝[s] a).NeBot ∧ (𝓝[t] b).NeBot
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2

Tactic:
rw [← x.eta]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 ↦ f ((x.1, x.2).1, x_1)) {b | ((x.1, x.2).1, b) ∈ s} (x.1, x.2).2
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1

Tactic:
rw [← x.eta]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 ↦ f (x_1, (x.1, x.2).2)) {a | (a, (x.1, x.2).2) ∈ s} (x.1, x.2).1
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
⊢ ∃ t_1 ⊆ (↑i).pi t, IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] t_1 ∧ f ∈ t_1

Tactic:
choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)

Goal state after:
case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ ∃ t_1 ⊆ (↑i).pi t, IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] t_1 ∧ f ∈ t_1
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
mem_closure_iff_nhdsWithin_neBot,

Goal state after:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : ¬(𝓝[f i] x).NeBot
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
this : IsOpen[inst✝] (⋃ i, f ↑i)ᶜ
⊢ IsOpen[inst✝] (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)

Tactic:
compl_iUnion,

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
this : IsOpen[inst✝] (⋂ i, (f ↑i)ᶜ)
⊢ IsOpen[inst✝] (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
x : X
⊢ ⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x

Tactic:
by
  refine IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)
  suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
    rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
  exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ n, L n) ∩ s

Tactic:
rw [preimage_iUnion, iUnion_inter]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ s ∩ ⋂ i, ⋂ i_1 ∈ i, t i_1 = ∅

Tactic:
by rwa [← iInter_eq_iInter_finset]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋃ i, U i)ᶜ
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
compl_iUnion,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋂ i, (U i)ᶜ)
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B C : Set α
hB : B ⊆ A
hC : C ⊆ A
h : A ↓∩ B = A ↓∩ C
⊢ B = C

Tactic:
simp only [← inter_eq_right] at hB hC
  simp only [Subtype.preimage_val_eq_preimage_val_iff, hB, hC] at h
  exact h

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
⊢ x ∈ s

Tactic:
obtain ⟨a, has, hax⟩ := h.prop
    rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨆ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp [iSup]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

Tactic:
by
  rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_sdiff]

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 s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t] t
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
nhdsSetWithin_self,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓟 t
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s] s ×ˢ 𝓝ˢ[t'] t
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
nhdsSetWithin_self,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓟 s ×ˢ 𝓝ˢ[t'] t
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x

Tactic:
by
  simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_sdiff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
h₂a : a = x
⊢ a ∈ (U \ s)ᶜ

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
h₂a : ¬a = x
⊢ a ∈ (U \ s)ᶜ

Tactic:
· tauto_set

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
h₂a : ¬a = x
⊢ a ∈ (U \ s)ᶜ
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h.right
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s

Tactic:
· tauto_set

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
g : T2Quotient X → Y
hfg : g ∘ mk = f
⊢ g = lift hf

Tactic:
apply surjective_mk X |>.right_cancellable |>.mp <| funext _

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
g : T2Quotient X → Y
hfg : g ∘ mk = f
⊢ ∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ IsClopen (s ∩ (s ∩ a))

Tactic:
refine isClopen_inter_of_disjoint_cover_clopen h ?_ (h.2.inter ha) (h.2.inter hb) ?_

Goal state after:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ⊆ s ∩ a ∪ s ∩ b

case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr.superset
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s s✝ t✝ : Set α
a✝ : CountableGenerateSets g s✝
st : s✝ ⊆ t✝
ih : s✝ ∈ f
⊢ t✝ ∈ f

Tactic:
| superset _ st ih =>

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr.sInter
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S✝ : Set (Set α)
Sct : S✝.Countable
a✝ : ∀ s ∈ S✝, CountableGenerateSets g s
ih : ∀ s ∈ S✝, s ∈ f
⊢ ⋂₀ S✝ ∈ f

Tactic:
| sInter Sct _ ih =>

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsClosed[inst✝] tᶜ
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
rw [isClosed_compl_iff, h] at ht

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∉ tᶜ
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ IsPreconnected (Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s)

Tactic:
exact (ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
      ⟨a₁, ha₁, rfl⟩ (hs.image _ (Continuous.prodMk_left _).continuousOn)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋃ i, U i)ᶜ
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
compl_iUnion,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : Disjoint s (⋂ i, (U i)ᶜ)
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ IsPreconnected ∅

Tactic:
· exact isPreconnected_empty

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩
⊢ s ⊆ connectedComponentIn F x

Tactic:
rw [connectedComponentIn_eq_image (hsF hxs)]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩
⊢ s ⊆ Subtype.val '' connectedComponent ⟨x, ⋯⟩
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst✝¹] (f i)
⊢ ⋂ i, f i = ⋂₀ range f

Tactic:
by rw [sInter_range]

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝] t
hd : ∀ t ∈ s, Dense t
⊢ Dense (⋂₀ s)

Tactic:
by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp [sInter_empty]
  | insert ha hsf ih =>
    simp only [sInter_insert, forall_mem_insert] at hd ⊢
    refine hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))
    exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)

Goal state after: