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
E E' : L.RightExtension F
Y Y' : D
e : Y ≅ Y'
h : E.IsPointwiseRightKanExtensionAt Y'
⊢ (fun h ↦ E.isPointwiseRightKanExtensionAtOfIso' h e) ((fun h ↦ E.isPointwiseRightKanExtensionAtOfIso' h e.symm) h) = h

Tactic:
by subsingleton

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G := ⋯
⊢ L.pointwiseLeftKanExtensionUnit F ≫
      L.whiskerLeft ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α) =
    L.pointwiseLeftKanExtensionUnit F ≫ L.whiskerLeft β

Tactic:
aesop

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F := ⋯
⊢ L.whiskerLeft
        ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α) ≫
      L.pointwiseRightKanExtensionCounit F =
    L.whiskerLeft β ≫ L.pointwiseRightKanExtensionCounit F

Tactic:
aesop

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
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
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
⊢ F'.IsRightKanExtension α ↔ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)

Tactic:
let eq : (RightExtension.mk _ α).IsUniversal ≃ (RightExtension.mk _
      ((associator _ _ _).hom ≫ whiskerLeft G α)).IsUniversal :=
    (RightExtension.isUniversalPrecompEquiv L F G _).trans
    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) :=
  (RightExtension.isUniversalPrecompEquiv L F G (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.precomp L F G).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension α ↔ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)
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₁
x : StructuredArrow.IsUniversal b
⊢ (fun h ↦ isUniversalOfPrecomp₂ α hα h) ((fun h ↦ isUniversalPrecomp₂ α hα h) x) = x

Tactic:
by subsingleton

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₁
x : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
⊢ (fun h ↦ isUniversalPrecomp₂ α hα h) ((fun h ↦ isUniversalOfPrecomp₂ α hα h) x) = x

Tactic:
by subsingleton

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

Goal state before:
pp: 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
⊢ PreservesFiniteColimits lim

Tactic:
apply +allowSynthFailures preservesFiniteColimits_of_preservesHomology

Goal state after:
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.PreservesHomology

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
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y)) (uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f.unop)) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))

Tactic:
uliftYonedaEquiv_apply,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.map f.unop).app (op (unop Y)))) { down := 𝟙 (unop Y) }) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.map f.unop).app (op (unop Y)))) { down := 𝟙 (unop Y) }) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))

Tactic:
uliftYonedaEquiv_apply,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.map f.unop).app (op (unop Y)))) { down := 𝟙 (unop Y) }) =
    (hom (s.pt.map f)) ((hom ((s.ι.app (op (P.elementsMk X x))).app (op (unop X)))) { down := 𝟙 (unop X) })
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
⊢ a = default

Tactic:
have : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ a = default
Module: Mathlib.CategoryTheory.Comma.LocallySmall

Goal state before:
pp: A : Type u₁
B : Type u₂
T : Type u₃
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : LocallySmall.{w, v₁, u₁} A
inst✝ : LocallySmall.{w, v₂, u₂} B
X Y : Comma L R
x✝² x✝¹ : X ⟶ Y
x✝ : (fun g ↦ (g.left, g.right)) x✝² = (fun g ↦ (g.left, g.right)) x✝¹
⊢ x✝² = x✝¹

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app zero = s.π.app zero

Tactic:
exact w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case one
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
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one

Tactic:
exact w

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ IsSeparator (G ⨿ H) ↔ (ObjectProperty.pair G H).IsSeparating

Tactic:
by
  refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_
  convert! Iff.rfl
  ext X
  simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]
  constructor
  · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]
  · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
x : ↑A
h :
  (AddCommGrpCat.Hom.hom f)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 }) =
    (AddCommGrpCat.Hom.hom g)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 })
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
aesop

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

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

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

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

Goal state before:
pp: C : Type u
F : C → Type v
⊢ ∀ (x : (sigma F).pt), ∃ i y, (sigma F).inj i y = x

Tactic:
aesop

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

Goal state before:
pp: case hf
C : Type u
F : C → Type v
c : CofanTypes F
⊢ ∀ (j : Discrete C) (x : (Discrete.functor F).obj j), c.ι j x = fromSigma F c ((sigma F).ι j x)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Circular

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

Tactic:
by
  ext
  rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_ofPred]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ f (-c) = -f 0

Tactic:
simpa only [zero_add] using h.neg 0

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (a * b ^ n) (a * b ^ (n + 1)))

Tactic:
simp +unfoldPartialApp only [Function.onFun]
  simp_rw [Set.disjoint_iff]
  intro m n hmn x hx
  apply hmn
  have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
  have i1 := hx.1.1.trans_lt hx.2.2
  have i2 := hx.2.1.trans_lt hx.1.2
  rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
  exact le_antisymm i1 i2

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
aesop

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 : α
m : ℤ
⊢ toIocDiv hp (a + m • p) b = toIocDiv hp a b - m

Tactic:
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc _ ?_

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (f.lift g) ↔ s ∈ f.lift (map m ∘ g)

Tactic:
by
    simp only [mem_lift_sets hg, mem_lift_sets this, mem_map, Function.comp_apply]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s = (interior sᶜ)ᶜ

Tactic:
interior,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s = (⋃₀ {t | IsOpen t ∧ t ⊆ sᶜ})ᶜ
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s = (⋃₀ {t | IsOpen t ∧ t ⊆ sᶜ})ᶜ

Tactic:
closure,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = (⋃₀ {t | IsOpen t ∧ t ⊆ sᶜ})ᶜ
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s V : Set X
⊢ (∀ x ∈ s, x ∈ interior V) ↔ ∀ x ∈ s, V ∈ 𝓝 x

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Sort u_4
p : ι → Prop
s : ι → Set X
P : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (⋃ i, ⋃ (_ : p i), s i), P x) ↔ ∀ (i : ι), p i → ∀ᶠ (x : X) in 𝓝ˢ (s i), P x

Tactic:
simp only [nhdsSet_iUnion, eventually_iSup]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Sort u_4
s : ι → Set X
P : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in 𝓝ˢ (s i), P x

Tactic:
simp only [nhdsSet_iUnion, eventually_iSup]

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

Tactic:
← hg.le_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
hf : Continuous[inst✝¹, inst✝²] f
hg : Continuous[inst✝², inst✝] g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f inst✝²
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsClosed[induced f t] (f ⁻¹' s)

Tactic:
simp_rw [← isOpen_compl_iff]

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsOpen[induced f t] (f ⁻¹' s)ᶜ
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
⊢ IsOpenMap f ↔ ∀ {u : Set X}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)

Tactic:
rw [IsOpenMap, compl_surjective.forall]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (x : Set X), IsOpen[inst✝¹] xᶜ → IsOpen[inst✝] (f '' xᶜ)) ↔
    ∀ {u : Set X}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
delta ContinuousWithinAt
    simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_ofPred_eq,
      and_imp]
    exact forall_congr' fun t => forall_comm

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty

Tactic:
exact ⟨i, h2, h1⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
  rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
  · simp [and_assoc, and_left_comm]
  · rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
    let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
    exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩
  · rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
    exact ⟨i, h2, h1⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
s : Set α
⊢ s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ (preimage f ∘ fun t ↦ t) '' {i | i ∈ T ∧ f a ∈ i}

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case e'_4
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
x✝ : Set β
⊢ x✝ ∈ image2 (fun x1 x2 ↦ x1 ∩ x2) B₁ B₂ ∧ a ∈ x✝ ↔
    x✝ ∈ (fun i ↦ i.1 ∩ i.2) '' {i | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α

Tactic:
← isBounded_univ,

Goal state after:
α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ IsBounded univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u

Tactic:
rw [← inter_assoc, ← hw.2, inter_comm _ s, inter_assoc, ← preimage_inter]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' (v ∩ t') ⊆ f ⁻¹' u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
· exact fun ⟨u, ⟨h1, _⟩⟩ =>
      ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩

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

Goal state before:
pp: case e'_1
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x | ∃ a ∈ is, P a x} = ⋃ i ∈ is, P i

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
by_cases hi : i ∈ s

Goal state after:
case pos
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

case neg
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ (⋃ u ∈ s', f u).Countable

pp: case refine_2
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts = generateFrom (⋃ u ∈ s', f u)

Tactic:
· apply s'_count.biUnion
    intro u hu
    exact Finite.countable (f_fin u hu)

Goal state after:
case refine_2
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts = generateFrom (⋃ u ∈ s', f u)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hg : Surjective g
hfg : LocallyFinite (f ∘ g)
⊢ LocallyFinite f

Tactic:
simpa only [comp_def, surjInv_eq hg] using hfg.comp_injective (injective_surjInv hg)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case e'_4
ι : 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
x✝ : Set ((i : ι) × E i)
⊢ x✝ ∈ ⋃ i, (fun u ↦ Sigma.mk i '' u) '' s i ∧ a ∈ x✝ ↔
    x✝ ∈ (fun i ↦ Sigma.mk a.fst '' i) '' {i | i ∈ s a.fst ∧ a.snd ∈ i}

Tactic:
aesop

Goal state after: