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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ h ≫ f = 0

Tactic:
← Subobject.factorThru_arrow _ _ w,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ ((kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow) ≫ f = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case insert.inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
a✝ : i✝ ∉ s✝
⊢ (P i✝).Factors (P i✝ ⊓ s✝.inf P).arrow

Tactic:
rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : ↑(Set.Iic Y)
⊢ (underlyingIso ((↑Z).ofLE Y ⋯)).hom ≫ (↑Z).arrow = ((fun Z ↦ mk ((↑Z).ofLE Y ⋯)) Z).arrow ≫ Y.arrow

Tactic:
simp [← Iso.eq_inv_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
⊢ (limit.cone (liftToFinsetObj (Discrete.functor f))).π.app S =
    ((liftToFinsetLimitCone (Discrete.functor f)).isLimit.conePointUniqueUpToIso
          (limit.isLimit (Discrete.functor f))).hom ≫
      (finiteSubproductsCone f).π.app S

Tactic:
simp only [limit.cone_x, Functor.const_obj_obj, liftToFinsetObj_obj, Discrete.functor_obj_eq_as,
      limit.cone_π, finiteSubproductsCone_pt, finiteSubproductsCone_π_app]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
⊢ limit.π (liftToFinsetObj (Discrete.functor f)) S =
    ((liftToFinsetLimitCone (Discrete.functor f)).isLimit.conePointUniqueUpToIso
          (limit.isLimit (Discrete.functor f))).hom ≫
      Pi.lift fun s ↦ Pi.π f (↑s).as
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 : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ

Tactic:
(h Y₁).fac_assoc (coconeAt G Y₁) X

Goal state after:
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 : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ
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).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
let β : L.pointwiseLeftKanExtension F ⟶ G :=
    { app := fun Y ↦ colimit.desc _ (costructuredArrowMapCocone L F G α Y) }

Goal state after:
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 :=
  { app := fun Y ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)
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 :=
  { app := fun Y ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
h : (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
exact NatTrans.congr_app h Y

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 :=
  { app := fun Y ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
h : (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
exact NatTrans.congr_app h Y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ (limitCompWhiskeringRightIsoLimitComp F G).hom ≫ whiskerRight (limit.π G j) F =
    limit.π (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
simp [← Iso.eq_inv_comp]

Goal state after:
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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
⊢ (restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g) =
    (restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g

Tactic:
by
        have := @IsColimit.homEquiv_symm_naturality (h :=
          Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)
        dsimp at this
        apply (restrictedULiftYonedaHomEquiv L α P Y).symm.injective
        apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext
        intro
        simp [restrictedULiftYonedaHomEquiv,
          restrictedULiftYonedaHomEquiv'_symm_naturality_right, this]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
⊢ (F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
      ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).leftKanExtensionUnique (uliftYonedaMap F Y)
          (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj Y))
          (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).hom =
    ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).leftKanExtensionUnique (uliftYonedaMap F X)
          (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
          (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).hom ≫
      (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f

Tactic:
apply uliftYonedaEquiv.injective
      have eq₁ := ConcreteCategory.congr_hom
        ((uliftYoneda.{max w v₁}.obj (F.obj Y)).descOfIsLeftKanExtension_fac_app
        (uliftYonedaMap F Y) (F.op.lan.obj (uliftYoneda.obj Y))
          (F.op.lanUnit.app (uliftYoneda.obj Y)) _) ⟨f⟩
      have eq₂ := ConcreteCategory.congr_hom
        (((uliftYoneda.{max w v₁}.obj (F.obj X)).descOfIsLeftKanExtension_fac_app
        (uliftYonedaMap F X) (F.op.lan.obj (uliftYoneda.obj X))
          (F.op.lanUnit.app (uliftYoneda.obj X))) _) ⟨𝟙 _⟩
      have eq₃ := ConcreteCategory.congr_hom (congr_app (F.op.lanUnit.naturality
        (uliftYoneda.{max w v₂}.map f)) _) ⟨𝟙 _⟩
      dsimp [uliftYoneda, uliftYonedaMap, uliftYonedaEquiv,
        Functor.leftKanExtensionUnique] at eq₁ eq₂ eq₃ ⊢
      simp only [Functor.map_id] at eq₂
      simp only [id_comp] at eq₃
      simp [eq₁, eq₂, eq₃]

Goal state after:
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
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ ι s ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one

Tactic:
s.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
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ s.π.app one = s.π.app one
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
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
⊢ (parallelFamily f).map (line (Classical.arbitrary J)) ≫ π s = s.ι.app zero

Tactic:
s.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
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
⊢ s.ι.app zero = s.ι.app zero
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 : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f g : Subobject.underlying.obj ⊥ ⟶ A
⊢ ⊥.ofLEMk (equalizer.ι f g ≫ ⊥.arrow) ⋯ ≫ equalizer.ι f g = 𝟙 (Subobject.underlying.obj ⊥)

Tactic:
by
      ext
      simp

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

Goal state before:
pp: C : Type u
F : C → Type v
c : Cofan F
⊢ Functor.CoconeTypes.IsColimit c.cofanTypes ↔ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes)

Tactic:
CofanTypes.isColimit_iff_bijective_fromSigma

Goal state after:
C : Type u
F : C → Type v
c : Cofan F
⊢ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes) ↔ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes)
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ↑(ExtensionOfMaxAdjoin.fst i a) + ExtensionOfMaxAdjoin.snd i a • y +
      (↑(ExtensionOfMaxAdjoin.fst i b) + ExtensionOfMaxAdjoin.snd i b • y) =
    ↑(ExtensionOfMaxAdjoin.fst i a) + ↑(ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a • y + ExtensionOfMaxAdjoin.snd i b • y)

Tactic:
ac_rfl

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

Goal state before:
pp: p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1

Tactic:
exact Nat.le_sub_one_of_lt (Nat.totient_lt p hp)

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun n ↦ x (ns (ms n))) atTop f

Tactic:
obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq

Goal state after:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), x (y n) ∉ s
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun n ↦ x (ns (ms n))) atTop f
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 : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ toIcoMod hp a b = b - toIcoDiv hp a b • p

Tactic:
toIcoMod

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ b - toIcoDiv hp a b • p = b - toIcoDiv hp a b • p
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: α : Type u_1
F : Filter α
inst✝ : TopologicalSpace α
a : α
⊢ MapClusterPt a F id ↔ ClusterPt a F

Tactic:
rw [MapClusterPt, map_id]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥

Tactic:
← sup_principal,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 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
hf : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (f '' ⋃ x ∈ s, {x})

Tactic:
image_iUnion,

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
⊢ map f (𝓝ˢ (⋃ x ∈ s, {x})) = 𝓝ˢ (⋃ 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
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
hf.isOpen_iff_image_isOpen,

Goal state after:
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 '' f ⁻¹' s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
⊢ 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a

Tactic:
rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

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

Tactic:
nhdsWithin_union,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[{a}] a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s s' : Set α
t t' : Set β
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) ≤ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t

Tactic:
by
  simpa [nhdsSetWithin, ← prod_inf_prod] using inf_le_of_left_le <| nhdsSet_prod_le _ _

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
⊢ (t ∩ v).Nonempty

Tactic:
refine nonempty_of_nonempty_preimage (f := (Subtype.val : s → X)) (hud (Subtype.val ⁻¹' t) ?_ ?_)

Goal state after:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
⊢ IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)

case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
⊢ (s ↓∩ t).Nonempty
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (inl '' univ) (inr '' univ)

Tactic:
exact disjoint_image_inl_image_inr

Goal state after:
Module: Mathlib.Topology.ContinuousOn

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

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

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ Dense (invFun f '' s)

Tactic:
simp_rw [h'.dense_iff, mem_closure_iff]

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ ∀ (x : α) (o : Set β), IsOpen[inst✝¹] o → f x ∈ o → (o ∩ f '' invFun f '' s).Nonempty
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case pos
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u : Set β
h : u ∈ 𝓝ˢ s
⊢ f ⁻¹' u ∈ 𝓝ˢ (f ⁻¹' s)

Tactic:
simpa [h] using hf.preimage_mem_nhdsSetWithin (s := s) (u := u) (s' := univ)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟

Tactic:
simp [Function.comp_def, map_bind, bind_map]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : IsSigmaCompact t
hs : IsClosed[inst✝] s
h : s ⊆ t
⊢ IsSigmaCompact s

Tactic:
rcases ht with ⟨K, hcompact, hcov⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ IsSigmaCompact s
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s✝ t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
K : X → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : ⋃ x ∈ s, K x = univ
⊢ SigmaCompactSpace X

Tactic:
refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_

Goal state after:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s✝ t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
K : X → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : ⋃ x ∈ s, K x = univ
⊢ ⋃₀ (K '' s) = univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
⊢ IsCompact (s ∩ t)

Tactic:
intro f

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
f : Filter X
⊢ ∀ [f.NeBot], f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝 x ⊓ 𝓟 s ⊓ comap f l

Tactic:
ac_rfl

Goal state after: