mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
⊢ (k : C) → IsColimit (((evaluation C D).obj k).mapCocone (((whiskeringLeft C E D).obj F).mapCocone c))

Tactic:
intro Y

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
Y : C
⊢ IsColimit (((evaluation C D).obj Y).mapCocone (((whiskeringLeft C E D).obj F).mapCocone c))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : P G
i : G ⟶ Y
⊢ i ≫ g = i ≫ h

Tactic:
obtain ⟨t, rfl, -⟩ := hf G hG i

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : P G
t : G ⟶ X
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
⊢ HasInitial C

Tactic:
by
    exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
rw [← isIso_op_iff]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case negSucc
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)

Tactic:
· simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hnm : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case h₂
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ n % a ≤ a

Tactic:
exact le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ Dense sᶜᶜ

Tactic:
by rwa [compl_compl]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ s ∩ frontier s = ∅

Tactic:
hs.frontier_eq,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ s ∩ (closure s \ s) = ∅
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Tactic:
AccPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Tactic:
by
  rw [insert_eq, nhdsSet_union, nhdsSet_singleton]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)

Tactic:
sSup_eq_iSup',

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

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']

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
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsQuotientMap f

Tactic:
rw [isQuotientMap_iff]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsCoinducing f ∧ Surjective f
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✝¹] (f ⁻¹' s)

Tactic:
by
  rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]

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
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ IsClosedEmbedding f

Tactic:
refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃
  refine h₁.le_induced.antisymm fun s hs => ?_
  refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
  rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a

Tactic:
delta nhdsWithin

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a

Tactic:
delta nhdsWithin

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t

Tactic:
delta nhdsWithin

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1

Tactic:
refine le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_
  rcases x with ⟨x, y⟩
  rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
  rcases hs with ⟨u, hu, v, hv, H⟩
  simp only [prod_subset_iff, mem_singleton_iff, mem_ofPred_eq, mem_preimage] at H
  exact mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
rw [continuousOn_iff']

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔
    ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : ↑s
⊢ Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a

Tactic:
by
  rw [← map_nhds_subtype_val, mem_map]

Goal state after:
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
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Prod.map f g)

Tactic:
isOpenMap_iff_nhds_le

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
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)
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
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)) ≤ map (Prod.map f g) (𝓝 (a, b))

Tactic:
rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_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
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : s =ᶠ[𝓝 x] t
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
by
  simp only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq.mpr h]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] y
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
by
  subst hy; exact hg.comp_of_mem_nhdsWithin_image hf hs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ 𝓝 (Pi.map f x) ≤ map (Pi.map f) (𝓝 x)

Tactic:
rw [nhds_pi, nhds_pi, map_piMap_pi hsurj]

Goal state after:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ (Filter.pi fun i ↦ 𝓝 (Pi.map f x i)) ≤ Filter.pi fun i ↦ map (f i) (𝓝 (x i))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 ↦ Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))

Tactic:
rcases eq_or_ne j i with (rfl | hj)

Goal state after:
case inl
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
j : ι
g : Y → A j
xi : A j
hg : Tendsto g l (𝓝 xi)
⊢ Tendsto (fun i ↦ Function.update (f i) j (g i) j) l (𝓝 (Function.update x j xi j))

case inr
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
hj : j ≠ i
⊢ Tendsto (fun i_1 ↦ Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : ∃ i, ∃ x ∈ b i, Subtype.val '' x = u
⊢ IsOpen[t] u

Tactic:
rcases hu with ⟨i, s, sb, rfl⟩

Goal state after:
case refine_1
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen[t] (Subtype.val '' s)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
i : ι
hi : a ∈ U i
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u

Tactic:
lift a to ↥(U i) using hi

Goal state after:
case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen[t] u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, ↑a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s

Tactic:
rw [continuousOn_iff']

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ (∀ (t_1 : Set β), IsOpen[inst✝] t_1 → ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) ↔
    ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥

Tactic:
by rwa [compl_compl]

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f

Tactic:
rw [range_comp]; exact image_mem_of_mem_comap large₀ large₁

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen[instTopologicalSpaceSigma] (⋃ i ∈ s, range (Sigma.mk i))

Tactic:
exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.map f)

Tactic:
change Continuous (ULift.up ∘ f ∘ ULift.down)
  fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact univ

Tactic:
Subtype.isSigmaCompact_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
⊢ ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
by
  choose V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
  refine (hs.elim_nhds_subcover' V V_nhds).imp fun t ht =>
    subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)
  simpa [← iUnion_inter, ← iUnion_coe_set]

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t✝ : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t✝ i)
hst : s ∩ ⋂ i, t✝ i = ∅
hdt : Directed (fun x1 x2 ↦ x1 ⊇ x2) t✝
t : ι
ht : s ⊆ (compl ∘ t✝) t
⊢ s ∩ t✝ t = ∅

Tactic:
simpa only [subset_def, not_forall, eq_empty_iff_forall_notMem, mem_iUnion, exists_prop,
      mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using! ht

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
⊢ s.sdiff t = s ↔ Disjoint (↑s) t

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i

Tactic:
exact mem_iUnion

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
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : s ×ˢ t ⊆ n
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

Tactic:
← hn.mem_nhdsSet,

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
i : ι
⊢ eval i ⁻¹' s i ∈ ↑f

Tactic:
exact mem_of_superset hfs fun x hx => hx i

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ {Z} ⊆ irreducibleComponents X

Tactic:
Set.singleton_subset_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ Z ∈ irreducibleComponents X
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
⊢ mk x = mk y

Tactic:
have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy

Goal state after:
case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
⊢ mk x = mk y
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
⊢ ∃ i, p i ∧ t i ∩ s = {x}

Tactic:
rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hs hx) with
    ⟨i, hi, hix⟩
  exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
a : α
⊢ a ∈ upperBounds (closure[inst✝²] s) ↔ a ∈ upperBounds s

Tactic:
by simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot

Tactic:
· simp only [IsBot, not_forall]
    rintro ⟨b, hb⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
    exact isClosed_Iic.isOpen_compl.mem_nhds hb

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen[inst✝²] (Ioi a)

Tactic:
by
  rw [← compl_Iic]
  exact isClosed_Iic.isOpen_compl

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure[inst✝] {b | f b ≤ g b}ᶜ
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ

Tactic:
simp only [not_le.symm]

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure[inst✝] {b | f b ≤ g b}ᶜ
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderClosedTopology (α i)
⊢ OrderClosedTopology ((i : ι) → α i)

Tactic:
constructor
  simp only [Pi.le_def, ofPred_forall]
  exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

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

Goal state before:
pp: case pos
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∈ K
⊢ IsPreconnected (connectedComponentIn (t i) (x i))

Tactic:
exact isPreconnected_connectedComponentIn

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

Goal state before:
pp: case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x✝ y : α
hx✝ : x✝ ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
x : α
hx : x ∈ s
⊢ ∀ᶠ (y : { x // x ∈ s }) in 𝓝 ⟨x, hx⟩, Q ⟨x, hx⟩ y ∧ Q y ⟨x, hx⟩

Tactic:
have Z := h x hx

Goal state after:
case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x✝ y : α
hx✝ : x✝ ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
this : PreconnectedSpace ↑s
x : α
hx : x ∈ s
Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
⊢ ∀ᶠ (y : { x // x ∈ s }) in 𝓝 ⟨x, hx⟩, Q ⟨x, hx⟩ y ∧ Q y ⟨x, hx⟩