mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ (limit.cone (StructuredArrow.proj X L ⋙ F)).π.app j =
    (Iso.refl (limit.cone (StructuredArrow.proj X L ⋙ F)).pt).hom ≫
      ((RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F)).coneAt X).π.app j

Tactic:
by
    dsimp
    simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]
    congr
    rw [comp_id, ← StructuredArrow.eq_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

Tactic:
letI (y : (L ⋙ L').LeftExtension F₀) :
      Unique ((precomp₂ L' α).obj b ⟶ y) := by
    let u : L'.LeftExtension F₁ :=
      mk y.right <|
        hα.desc <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom
    refine
      ⟨⟨StructuredArrow.homMk (hb.desc u) <| by
          ext x
          have hb_fac_app := congr_app (hb.fac u) (L.obj x)
          have hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
          dsimp at hα_fac_app hb_fac_app
          simp [hb_fac_app, u, hα_fac_app]⟩, fun a => ?_⟩
    dsimp
    ext1
    apply hb.hom_ext
    apply hα.hom_ext
    ext t
    dsimp
    have a_w_t := congr_app a.w t
    have hb_fac_app := congr_app (hb.fac u) (L.obj t)
    have hα_fac_app :=
      congr_app
        (hα.fac <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom) t
    dsimp at hb_fac_app hα_fac_app
    simp only [whiskeringLeft_obj_obj, comp_obj,
      precomp₂_obj_right, whiskeringLeft_obj_map, NatTrans.comp_app,
      precomp₂_obj_hom_app, whiskerLeft_app, assoc] at a_w_t
    simp [← a_w_t, hb_fac_app, u, hα_fac_app]

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
this : (y : (L ⋙ L').LeftExtension F₀) → Unique ((precomp₂ L' α).obj b ⟶ y) :=
  fun y ↦
    let u :=
      mk (StructuredArrow.right y)
        (hα.desc
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)));
    { default := StructuredArrow.homMk (hb.desc u) ⋯, uniq := ⋯ }
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
let _ := Encodable.ofCountable J

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
x✝ : Encodable J := Encodable.ofCountable J
⊢ HasExactColimitsOfShape (Discrete J) C
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
⊢ HasExactLimitsOfShape (Discrete J) C

Tactic:
let _ := Encodable.ofCountable J

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
x✝ : Encodable J := Encodable.ofCountable J
⊢ HasExactLimitsOfShape (Discrete J) C
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCountableProducts C
inst✝² : HasFiniteColimits C
inst✝¹ : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
⊢ ∀ [inst : Countable J], HasExactLimitsOfShape (Discrete J) C

Tactic:
by
    by_cases h : Finite J
    · infer_instance
    · have : Infinite J := ⟨h⟩
      let _ := Encodable.ofCountable J
      let _ := Denumerable.ofEncodableOfInfinite J
      exact hasExactLimitsOfShape_of_initial C (Discrete.equivalence (Denumerable.eqv J)).inverse

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.Additive

Tactic:
exact additive_of_preservesBinaryBiproducts _

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
← assoc,

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ (m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j)) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.Additive

Tactic:
exact additive_of_preservesBinaryBiproducts _

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv (p ≫ presheafHom φ P ≫ F.op.whiskerLeft (G.map f)) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })

Tactic:
← assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv ((p ≫ presheafHom φ P) ≫ F.op.whiskerLeft (G.map f)) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
f : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).obj u₁
⊢ (ConcreteCategory.hom
          (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).map g ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₂).snd)).toFun
      f =
    (ConcreteCategory.hom
          ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₁).snd) ≫
            ((const F.Elementsᵒᵖ).obj (F.obj X)).map g)).toFun
      f

Tactic:
obtain ⟨f, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective f

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
f : unop ((CategoryOfElements.π F).op.obj u₁) ⟶ X
⊢ (ConcreteCategory.hom
          (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).map g ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₂).snd)).toFun
      (shrinkYonedaObjObjEquiv.symm f) =
    (ConcreteCategory.hom
          ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₁).snd) ≫
            ((const F.Elementsᵒᵖ).obj (F.obj X)).map g)).toFun
      (shrinkYonedaObjObjEquiv.symm f)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : GrpCat} {Y : CommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ CommGrpCat GrpCat).obj Y),
    ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm (f ≫ g) =
      abelianize.map f ≫
        ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g

Tactic:
by
        intros
        ext
        simp +instances only
        apply Eq.symm
        apply Abelianization.lift_unique
        intros
        apply Abelianization.lift_apply_of

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
obtain (rfl | c0) := c.eq_zero_or_pos

Goal state after:
case inl
d d' : ℕ
hn : 2 * (0 ^ 2 + d + 1) ≤ 2 * (0 ^ 2 + d + 1) + d'
⊢ 0 ^ (2 * (0 ^ 2 + d + 1) + d') < (2 * (0 ^ 2 + d + 1) + d' - d)!

case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) + x₁ ≤ toIocMod hp 0 (x₃ - x₁) + x₁ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
add_le_add_iff_right,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (x₃ - x₁) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
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 : ℤ
⊢ toIocMod hp (↑m * p + a) b = ↑m * p + toIocMod hp a b

Tactic:
by
  rw [add_comm, toIocMod_add_intCast_mul', add_comm]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case inr
α : Type u_1
s : Set (Set α)
t✝ : Set α
ht : GenerateOpen s t✝
t : Set α
h : t ∈ s
⊢ IsOpen[generateFrom s] t

Tactic:
exact isOpen_generateFrom_of_mem h

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
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ coinduced g (coinduced f inst✝²) ≤ coinduced g inst✝¹

Tactic:
hf.coinduced_le

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
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ coinduced g inst✝¹ ≤ coinduced g inst✝¹
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f

Tactic:
by
  refine ⟨?_, fun hf => hf.comp h.isOpenMap⟩
  intro hf
  rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc]
  exact hf.comp h.symm.isOpenMap

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 : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (⨆ i ∈ s, 𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})

Tactic:
map_iSup,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ ⨆ i ∈ s, map f (𝓝ˢ {i}) = ⨆ i ∈ s, 𝓝ˢ (f '' {i})
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
⊢ IsCoinducing f ∧ Surjective f

Tactic:
refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, surj⟩

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
s : Set Y
⊢ IsOpen[inst✝¹] (f ⁻¹' s) ↔ IsOpen[inst✝] s
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
by simp [inter_comm s t, inter_assoc]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
inf_assoc,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t))
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 → Z
g : Y → W
x : X
y : Y
⊢ ContinuousAt (Prod.map f g) (x, y) ↔ ContinuousAt f x ∧ ContinuousAt g y

Tactic:
simp [ContinuousAt, nhds_prod_eq, tendsto_iff_comap, comap_prodMap_prod]

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
← nhdsWithin_subtype_eq_bot_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ 𝓝[≠] x = ⊥ ↔ 𝓝[S ↓∩ {↑x}ᶜ] x = ⊥
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
interior_inter,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsOpen[inst✝¹] s
⊢ interior s ∩ interior (f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case refine_2
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
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g

Tactic:
· rw [(isOpenQuotientMap_snd (X := X)).isOpenMap_iff]
    exact isOpenMap_snd.comp 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 γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) {b | (a, b) ∈ s}

Tactic:
simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_left]; rfl

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:

Tactic:
f n y = f (N x + 1) y := hN _ _ hn _ hy
    _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
    _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)

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
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
by
  constructor
  · exact fun h ↦ h.image hf.continuous
  · rintro ⟨L, hcomp, hcov⟩
    -- Suppose f(s) is σ-compact; we want to show s is σ-compact.
    -- Write f(s) as a union of compact sets L n, so s = ⋃ K n with K n := f⁻¹(L n) ∩ s.
    -- Since f is inducing, each K n is compact iff L n is.
    refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
    · intro n
      have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
        rw [image_preimage_inter, inter_eq_left.mpr]
        exact (subset_iUnion _ n).trans hcov.le
      apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))
    · calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
⊢ Continuous[inst✝, _] fun x ↦ x ∈ s ∩ t ∪ s' \ t

Tactic:
convert!
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x✝
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
⊢ ∃ t, closure[inst✝¹] {x} ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨{i}, fun y hy ↦ ?_⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ∈ closure[inst✝¹] {x}
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case neg
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
· use Sᶜ
        refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
        rw [compl_compl]
        exact hne

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
⊢ codiscreteWithin U₁ ≤ codiscreteWithin U

Tactic:
refine (biSup_mono hU).trans <| iSup₂_mono fun _ _ ↦ ?_

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
x✝¹ : X
x✝ : x✝¹ ∈ U
⊢ 𝓝[U₁ \ {x✝¹}] x✝¹ ≤ 𝓝[U \ {x✝¹}] x✝¹
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 (update f x y) s z

Tactic:
rw [continuousWithinAt_update_of_ne hzx]

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
⊢ ContinuousWithinAt f s z
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: 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:
constructor <;> intro hfg
  · obtain ⟨Uf, Ug, h₁U, h₂U, h₃U, h₄U, h₅U⟩ := t2_separation hfg
    rw [Set.disjoint_iff_inter_eq_empty] at h₅U
    filter_upwards [inter_mem
      (hf.preimage_mem_nhds (IsOpen.mem_nhds h₁U h₃U))
      (hg.preimage_mem_nhds (IsOpen.mem_nhds h₂U h₄U))]
    intro x hx
    simp only [Set.mem_inter_iff, Set.mem_preimage] at hx
    by_contra H
    rw [H] at hx
    have : g x ∈ Uf ∩ Ug := hx
    simp [h₅U] at this
  · obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hfg
    exact h₁t x h₃t

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : y ∈ closure[inst✝¹] K
⊢ ∃ x ∈ K, Inseparable x y

Tactic:
contrapose! hy

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
⊢ y ∉ closure[inst✝¹] K
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
split_ifs <;> simp [*]

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y

Tactic:
rw [connectedComponentIn_eq hy]

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y