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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
ι : limit (F.op ⋙ yoneda.obj pt)
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsCofiltered C ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
rw [IsCofiltered.iff_cone_nonempty.{v}]
  refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
  · obtain ⟨c⟩ := h F
    exact ⟨c.pt, ⟨(limitCompCoyonedaIsoCone F c.pt).inv c.π⟩⟩
  · obtain ⟨pt, ⟨π⟩⟩ := h F
    exact ⟨⟨pt, (limitCompCoyonedaIsoCone F pt).hom π⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯)) ≫ f.arrow = smallCoproductDesc s

Tactic:
· ext
      dsimp [smallCoproductDesc]
      simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : C
⊢ (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))

Tactic:
simpa using leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom L F
    (L.obj X) (CostructuredArrow.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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
t : C
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.hom y)).app t

Tactic:
have := congr_app u.w t

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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right u)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.hom y)).app t
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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
t : C
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right default)).app
      t

Tactic:
have := congr_app u.w t

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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right u)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right default)).app
      t
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
⊢ PreservesLimit H colim

Tactic:
by
    have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
    have : PreservesColimitsOfSize.{v', u'} F := adj.leftAdjoint_preservesColimits
    let e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
      isoWhiskerLeft _ (preservesColimitNatIso F) ≪≫ (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (whiskeringRightObjCompIso G F) _ ≪≫
        isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) _ ≪≫
        isoWhiskerRight whiskeringRightObjIdIso _ ≪≫ colim.leftUnitor
    exact preservesLimit_of_natIso _ e

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)
⊢ s.π.app (L.obj j) ≫ α.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
IsLimit.fac,

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)
⊢ s.π.app (L.obj j) ≫ α.app j = { pt := s.1, π := L.whiskerLeft s.π ≫ α }.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π = s.π ≫ i.hom

Tactic:
w

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π = t.π
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app j ≫ S.X₃.map e₁)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
← NatTrans.naturality,

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.X₂.map e₁ ≫ S.g.app k)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ lim.PreservesEpimorphisms

Tactic:
exact {
    preserves {X Y} f hf := by
      let iX : limit X ≅ AddCommGrpCat.of ((i : J) → X.obj ⟨i⟩) := (Pi.isoLimit X).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) := (Pi.isoLimit Y).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
        simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit,
          IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
          Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
          IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv, Functor.mapIso_hom,
          IsLimit.uniqueUpToIso_hom, lim_map, Iso.trans_hom, Iso.symm_hom,
          AddCommGrpCat.HasLimit.lift, Category.assoc, limit.lift_map_assoc, iX, iY]
        ext g j
        change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π,
          Fan.mk_π_app, Pi.map_apply]
        change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
        simp
      suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
      suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance
      rw [AddCommGrpCat.epi_iff_surjective, ← this]
      simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf
      refine fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩
      funext i
      exact (hf ⟨i⟩ (b i)).choose_spec }

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ x✝ ∈ cIoo b a

Tactic:
Set.mem_cIoo,

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ sbtw b x✝ a
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : 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

Tactic:
simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]

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

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ a, ∃ (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b

Tactic:
· simp only [mem_filter, mem_range, exists_prop, and_imp]
    intro b hb1 hb2
    have : d ∣ b := by
      rw [← hb2]
      apply gcd_dvd_right
    rcases this with ⟨q, rfl⟩
    refine ⟨q, ⟨⟨(mul_lt_mul_iff_right₀ hd0).1 hb1, ?_⟩, rfl⟩⟩
    rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2

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

Goal state before:
pp: case neg
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

case neg
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : ¬b = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ 𝓟 (closure ∅) = ⊥

Tactic:
closure_empty,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ 𝓟 ∅ = ⊥
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ Dense sᶜ

Tactic:
rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint (interior s) (frontier s)

Tactic:
by
  rw [disjoint_iff_inter_eq_empty, ← closure_sdiff_interior, sdiff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝

Tactic:
@isOpen_iff_nhds _ _ _,

Goal state after:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ (∀ x ∈ x✝, 𝓝 x ≤ 𝓟 x✝) ↔ ∀ x ∈ x✝, 𝓝 x ≤ 𝓟 x✝
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ ¬(𝓝[s] x).NeBot ↔ 𝓝[s] x = ⊥

Tactic:
not_neBot

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝[s] x = ⊥ ↔ 𝓝[s] 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 : ℤ
⊢ toIcoDiv hp a (b - ↑m * p) = toIcoDiv hp a b - m

Tactic:
simpa using toIcoDiv_sub_zsmul hp a b m

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ⨅ s ∈ {s | a ∈ s ∧ IsOpen[generateFrom g] s}, 𝓟 s = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Tactic:
refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_

Goal state after:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ∀ i ∈ {s | a ∈ s ∧ IsOpen[generateFrom g] s}, ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 i
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : x ∈ (fun n ↦ u₀ n) n
⊢ x ∈ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)

Tactic:
simp only [mem_iUnion]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : x ∈ (fun n ↦ u₀ n) n
⊢ ∃ i, x ∈ u₀ i \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ i), v₀ m)
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
m_gt_n : ¬n ≤ m
⊢ False

Tactic:
exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)

Tactic:
by
  rw [induced_generateFrom_eq]
  apply le_generateFrom
  simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]
  exact h

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
⊢ (∀ (s : Set Y), IsClosed[inst✝¹] (f ⁻¹' s) ↔ IsClosed[inst✝] s) ∧ Surjective f ↔
    Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
and_comm,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝¹] (f ⁻¹' s) ↔ IsClosed[inst✝] s) ↔
    Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : ¬(𝓝[s] x).NeBot
⊢ ContinuousWithinAt f s x

Tactic:
not_neBot

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsClosedEmbedding f
hg : IsClosedEmbedding g
h : Injective (Sum.elim f g)
⊢ IsClosedEmbedding (Sum.elim f g)

Tactic:
by
  rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
  exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
by
  simp_rw [Pi.induced_domRestrict, iInf_sUnion]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : 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)
⊢ IsTopologicalBasis (⋃ i, image Subtype.val '' b i)

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_

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)
u : Set α
hu : u ∈ ⋃ i, image Subtype.val '' b i
⊢ IsOpen[t] u

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 α), a ∈ u → IsOpen[t] u → ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u
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 α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
⊢ MapsTo (fun b ↦ (a, b)) sβ (sα ×ˢ sβ)

Tactic:
by grind [Set.MapsTo]

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 α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
⊢ MapsTo (fun a ↦ (a, b)) sα (sα ×ˢ sβ)

Tactic:
by grind [Set.MapsTo]

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

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ ((IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) →
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

pp: case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g)) →
    (IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
· intro ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, f_ne_g⟩⟩
    exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩

Goal state after:
case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g)) →
    (IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b