mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
⊢ ∀ (i : P ≅ Q), i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op

Tactic:
i

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
⊢ i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (fun x ↦
          match j', x with
          | { as := i }, x => ⟨i, x⟩) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      fun x ↦
      match j, x with
      | { as := i }, x => ⟨i, x⟩

Tactic:
rintro ⟨i⟩ ⟨j⟩ f
    obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j' with
        | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))

Tactic:
rintro ⟨i⟩ ⟨j⟩ f
    obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr
X : Type u
⊢ IsEmpty X → Nonempty (IsInitial X)

Tactic:
intro h
    exact ⟨IsInitial.ofIso Types.isInitialPEmpty <| Equiv.toIso <| Equiv.equivOfIsEmpty PEmpty X⟩

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
⊢ n✝ • Exists.choose ⋯ = a

Tactic:
generalize_proofs h1

Goal state after:
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
h1 : ∃ a_1 ∈ ↑⊤, ((DistribMulAction.toAddMonoidEnd ℤ A) n✝) a_1 = a
⊢ n✝ • h1.choose = a
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x

Tactic:
by
  rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

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⟩
  simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
x y : ↥i.range
eq1 : i (Exists.choose ⋯ + Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)

Tactic:
← Fact.out (p := Function.Injective i) eq1,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
x y : ↥i.range
eq1 : i (Exists.choose ⋯ + Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯ + Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯) = r • f (Exists.choose ⋯)

Tactic:
← Fact.out (p := Function.Injective i) eq1,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (r • Exists.choose ⋯) = r • f (Exists.choose ⋯)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = #({k ∈ range (d * x) | (d * x).gcd k = d})

Tactic:
rw [Nat.mul_div_cancel_left x hd0]

Goal state after:
case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Goal state after:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atBot (atBot ×ˢ atBot)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Goal state after:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ atBot.IsCountablyGenerated

Tactic:
rw [← prod_atBot_atBot_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ (atBot ×ˢ atBot).IsCountablyGenerated
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
by
  simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]
  push Not; rfl

Goal state after:
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 : α
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

Tactic:
rw [add_comm, toIcoDiv_add_right']

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
⊢ IsOpen[inst✝] s ↔ ∀ (i : α), IsOpen[inst✝] (f i ∩ s)

Tactic:
refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
  rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]
  exact isOpen_iUnion fun i ↦ h i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

Tactic:
inf_eq_iInf,

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (⨅ b, bif b then f else g).lift' s = f.lift' s ⊓ g.lift' s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (⨅ b, bif b then f else g).lift' s = f.lift' s ⊓ g.lift' s

Tactic:
inf_eq_iInf,

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (⨅ b, bif b then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
⊢ (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ

Tactic:
congr! 2

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
x✝ : X
⊢ x✝ ≠ x ∧ x✝ ∈ C ↔ x✝ ∈ C ∧ x✝ ∈ {x}ᶜ
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocDiv hp (a - ↑m * p) b = toIocDiv hp a b + m

Tactic:
by
  simpa using toIocDiv_sub_zsmul' hp a b m

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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ inst✝¹ = induced (g ∘ f) inst✝

Tactic:
h.eq_induced

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ induced (g ∘ f) inst✝ = induced (g ∘ f) inst✝
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ 𝓟 ∅ = ⊥

Tactic:
principal_empty,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ ⊥ = ⊥
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
⊢ 𝓝[I₁ ∪ I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
nhdsWithin_union

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
⊢ 𝓝[I₁] b ⊔ 𝓝[I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝[I₁ ∪ I₂] b

Tactic:
nhdsWithin_union

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝[I₁] b ⊔ 𝓝[I₂] b
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
x : α
⊢ 𝓝[Iio x ∪ Ioi x] x = 𝓝[<] x ⊔ 𝓝[>] x

Tactic:
nhdsWithin_union

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
x : α
⊢ 𝓝[<] x ⊔ 𝓝[>] x = 𝓝[<] x ⊔ 𝓝[>] x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[≠] ↑x ⊓ 𝓟 S = ⊥

Tactic:
rw [← nhdsWithin_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
    Subtype.coe_injective.preimage_image]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst✝²] (inl ⁻¹' Z) ∧ IsClosed[inst✝¹] (inr ⁻¹' Z)
⊢ IsClosed[inst✝] (f '' Z)

Tactic:
convert! (h.1 _ hZ.1).union (h.2 _ hZ.2)

Goal state after:
X : Type u
Y : Type v
Z✝ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst✝²] (inl ⁻¹' Z) ∧ IsClosed[inst✝¹] (inr ⁻¹' Z)
⊢ f '' Z = (fun a ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun b ↦ f (inr b)) '' inr ⁻¹' Z
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)

Tactic:
· have A : g ∘ f =ᶠ[𝓝[g '' s] g x] id :=
      h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin
    refine le_map_of_right_inverse A ?_
    simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf✝ : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ↥I) → ↑(c ↑i)
hf : g ⟨I, f⟩ ∈ (↑I).pi u
⊢ (o ∩ range g).Nonempty

Tactic:
exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi] at hs

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ Filter.pi fun i ↦ 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g

Tactic:
by
  refine ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩
  set g : Filter (sᶜ : Set α) := comap (↑) f
  have : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_ofPred])
  simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]

Goal state after:
α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : x ∈ ⋃ a ∈ s u, a
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ ∃ v_1, (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩

Goal state after:
case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : x ∈ ⋃ a ∈ s u, a
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ w ⊆ v
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ IsTopologicalBasis (⋃ i, (fun u ↦ Sigma.mk i '' u) '' s i)

Tactic:
refine .of_hasBasis_nhds fun a ↦ ?_

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (𝓝 a).HasBasis (fun t ↦ t ∈ ⋃ i, (fun u ↦ Sigma.mk i '' u) '' s i ∧ a ∈ t) id
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
⊢ {i | y ∈ s i} ⊆ {i | x ∈ s i}

Tactic:
i

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
i : ι
⊢ i ∈ {i | y ∈ s i} → i ∈ {i | x ∈ s i}
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
by
  have : Countable ↑s := countable_coe_iff.mpr hc
  rw [biUnion_eq_iUnion]
  exact isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
⊢ s.Finite

Tactic:
by
  have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
  rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, _, hst⟩
  simp only [← t.set_biUnion_coe, biUnion_of_singleton] at hst
  exact t.finite_toSet.subset hst

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact univ

Tactic:
rw [hf.isInducing.isCompact_iff, image_univ]; exact hf.isClosed_range.isCompact

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology ↑S ↔ ∀ y ∈ S, ∃ U, IsOpen[inst✝] U ∧ U ∩ S = {y}

Tactic:
simp [discreteTopology_iff_isOpen_singleton, isOpen_induced_iff, Set.ext_iff]

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ (∀ a ∈ S, ∃ t, IsOpen[inst✝] t ∧ ∀ a_1 ∈ S, a_1 ∈ t ↔ a_1 = a) ↔
    ∀ y ∈ S, ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Y), x ∈ U ∧ x ∈ S ↔ x = y
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
⊢ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
i

Goal state after:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
⊢ False

Tactic:
have : s ∩ U = s := hmin (s ∩ U) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen[inst✝¹] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst✝¹] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst✝¹] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
this : s ∩ U = s
⊢ False
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ContinuousOn f (s \ {x})
z : X
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt f s z

Tactic:
refine (H z ⟨hzs, hzx⟩).mono_of_mem_nhdsWithin (inter_mem_nhdsWithin _ ?_)

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ContinuousOn f (s \ {x})
z : X
hzx : z ≠ x
hzs : z ∈ s
⊢ (fun a ↦ a ∈ {x} → False) ∈ 𝓝 z
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T1Space (SeparationQuotient X) ↔ Std.Symm Specializes

Tactic:
((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Std.Symm Specializes
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ IsOpen[inst✝] S ∧ IsDiscrete Sᶜ

Tactic:
by
  rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]

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

Goal state before:
pp: case refine_2
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
⊢ f y ∈ s

Tactic:
by_contra hys
    exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, notMem_subset interior_subset hys⟩)

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

Goal state before:
pp: case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
have h : s ⊆ range Sum.inl :=
        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩

Goal state after:
case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝¹] (s i)

Tactic:
rw [← isOpen_compl_iff, compl_eq_univ_sdiff, ← h_Union, iUnion_sdiff]

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (⋃ i_1, s i_1 \ s i)