mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃

Tactic:
rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ ((forget Y).obj ((«exists» f).obj Z)).left ≅ ((forget Y).obj ((map f).obj Z)).left

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ Iso.hom ?m.83 ≫ ((forget Y).obj ((map f).obj Z)).hom = ((forget Y).obj ((«exists» f).obj Z)).hom

Tactic:
· apply imageMonoIsoSource (Z.arrow ≫ f)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (imageMonoIsoSource (Z.arrow ≫ f)).hom ≫ ((forget Y).obj ((map f).obj Z)).hom =
    ((forget Y).obj ((«exists» f).obj Z)).hom
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (imageMonoIsoSource (Z.arrow ≫ f)).hom ≫ ((forget Y).obj ((map f).obj Z)).hom =
    ((forget Y).obj ((«exists» f).obj Z)).hom

Tactic:
apply imageMonoIsoSource_hom_self

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃

Tactic:
zero,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.g - r ≫ 0 = S.g ≫ 𝟙 S.X₃
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : Balanced C
f : X ⟶ Y
inst✝ : Mono f
⊢ Epi f ↔ mk f = ⊤

Tactic:
← isIso_iff_mk_eq_top

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : Balanced C
f : X ⟶ Y
inst✝ : Mono f
⊢ Epi f ↔ IsIso f
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))

Tactic:
conv_lhs => rw [← coimage_image_factorisation α]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coimage.π α ≫ coimageImageComparison α ≫ image.ι α).app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X X✝ : C
⊢ IsIso ((coimageImageComparison α).app X✝)

Tactic:
rw [coimageImageComparison_app']

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X X✝ : C
⊢ IsIso ((coimageObjIso α X✝).hom ≫ coimageImageComparison (α.app X✝) ≫ (imageObjIso α X✝).inv)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case mp
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
W Z : Subobject (underlying.obj Y)
h : ⟨mk (W.arrow ≫ Y.arrow), ⋯⟩ ≤ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩
⊢ W ≤ Z

Tactic:
exact le_of_comm (((underlyingIso _).inv ≫ ofLE _ _ (Subtype.mk_le_mk.mp h) ≫
        (underlyingIso _).hom)) (by cat_disch)

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

Goal state before:
pp: case mp
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y → L'.HasPointwiseLeftKanExtensionAt F Y'

pp: case mpr
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
· intro
    exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Goal state after:
case mpr
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y
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✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ colimit.ι (G ⋙ (whiskeringRight C D E).obj F) j ≫ (colimitCompWhiskeringRightIsoColimitComp F G).hom =
    whiskerRight (colimit.ι G j) F

Tactic:
simp [colimitCompWhiskeringRightIsoColimitComp]

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

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

Tactic:
← cancel_epi (cokernel.π (kernel.ι f.unop))

Goal state after:
case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ cokernel.π (kernel.ι f.unop) ≫
      ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op).unop =
    cokernel.π (kernel.ι f.unop) ≫ (𝟙 (op (cokernel (kernel.ι f.unop)))).unop
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsCofiltered J
⊢ HasExactLimitsOfShape J C

Tactic:
have := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5StarOfSize.{w₂, w₂', v, u} C
this✝ : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsCofiltered J
this : IsCofiltered (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactLimitsOfShape J C
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 Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
hfg :
  α.app p.left ≫
      L.map p.hom ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
          ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)).app p
hg :
  α.app p.left ≫
      L.map (p.hom ≫ f) ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g) =
    ((restrictedULiftYonedaHomEquiv' A Q X).symm g).app ((CostructuredArrow.map f).obj p)
⊢ (α.app p.left ≫ L.map p.hom) ≫
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    (α.app p.left ≫ L.map p.hom) ≫
      L.map f ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g)

Tactic:
simp only [assoc, hfg, ← L.map_comp_assoc, hg,
          restrictedULiftYonedaHomEquiv'_symm_app_naturality_left]

Goal state after:
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)
⊢ HasInitial C

Tactic:
let endos := T ⟶ T
  let i := wideEqualizer.ι (id : endos → endos)
  have : Nonempty endos := ⟨𝟙 _⟩
  have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) := by
    intro X
    refine ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => ?_⟩
    let E := equalizer a (i ≫ Classical.choice (hT _))
    let e : E ⟶ wideEqualizer id := equalizer.ι _ _
    let h : T ⟶ E := Classical.choice (hT E)
    have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
      rw [Category.assoc, Category.assoc]
      apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
    rw [Category.comp_id, cancel_mono_id i] at this
    have : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
    rw [← cancel_epi e]
    apply equalizer.condition
  exact hasInitial_of_unique (wideEqualizer (id : endos → endos))

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

Goal state before:
pp: case i.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ (unop P).left ≅ (mk q).left

Tactic:
exact (Subobject.underlyingIso f.unop.left.op).unop

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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (natTrans φ).app (uliftYoneda.{max w v₂, v₁, u₁}.obj X) = (compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X

Tactic:
by
  dsimp [natTrans]
  apply (F.op.lan.obj (uliftYoneda.obj X)).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app _)
  rw [Functor.descOfIsLeftKanExtension_fac]
  apply uliftYonedaEquiv.injective
  rw [uliftYonedaEquiv_presheafHom_uliftYoneda_obj]
  exact _root_.congr_arg _ (compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id F X).symm

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

Goal state before:
pp: case snd
G H : GrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q)).2 = (p, q).2

Tactic:
· exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget GrpCat.{u}) G H) (p, q)

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

Goal state before:
pp: n : ℤ
⊢ |↑n.negOnePow| = 1

Tactic:
by
  rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : SubtractionCommMonoid α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f (c - x) = -f (-x)

Tactic:
by simpa only [sub_eq_neg_add] using h (-x)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, p x
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

Tactic:
rw [← Filter.eventually_forall_ge_atTop] at h_evtl; exact (h_evtl.comap f).filter_mono hf.le_comap

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop atTop

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop (atTop ×ˢ atTop)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ atTop.IsCountablyGenerated

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ (atTop ×ˢ atTop).IsCountablyGenerated
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g

Tactic:
simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t
⊢ ∀ x ∈ iInf f, s ∈ g x → s ∈ ⨅ i, (f i).lift g
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 : α
⊢ toIcoMod hp a (b + p) = toIcoMod hp a b

Tactic:
simpa only [one_zsmul] using toIcoMod_add_zsmul hp a b 1

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ 𝓝 x ≤ f

Tactic:
by
  rw [nhds_def]; exact iInf₂_le_of_le s ⟨h, o⟩ sf

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 : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + toIcoDiv hp a b • p

Tactic:
conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst✝]).NeBot
U : Set X
⊢ U ∈ F.lift' closure[inst✝] → U ∈ pure x

Tactic:
hU

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst✝]).NeBot
U : Set X
hU : U ∈ F.lift' closure[inst✝]
⊢ U ∈ pure x
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ⊆ s ↔ ∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s

Tactic:
by simp only [subset_def, mem_closure_iff_clusterPt]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p

Tactic:
by
  rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]
  simp [field, -Int.self_sub_floor]
  ring

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Tactic:
refine ⟨toIocDiv hp a b, ⟨lt_sub_iff_add_lt.mp hl, ?_⟩⟩

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
⊢ U ∈ n a → U ∈ 𝓝 a

Tactic:
hU

Goal state after:
case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
⊢ U ∈ 𝓝 a
Module: Mathlib.Topology.Order

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

Tactic:
nhds_nhdsAdjoint,

Goal state after:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ (∀ (x : α), 𝓝 x ≤ update pure a (pure a ⊔ f) x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Module: Mathlib.Topology.Order

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

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

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsCoinducing f
hf' : Injective f
⊢ IsOpenMap f

Tactic:
intro s hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsCoinducing f
hf' : Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (f '' s)
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
hg : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)

Tactic:
intro s hs

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
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst✝²] s
⊢ IsClosed[inst✝] (g ∘ 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
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
⊢ IsClosedMap f

Tactic:
intro s hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
⊢ IsClosed[inst✝] (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
hf : IsInducing f
h : IsClosed[inst✝] (range f)
⊢ IsClosedMap f

Tactic:
intro s hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed[inst✝] (range f)
s : Set X
hs : IsClosed[inst✝¹] s
⊢ IsClosed[inst✝] (f '' s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ 𝓟 {a} = pure a

Tactic:
principal_singleton,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ pure a = pure a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥

Tactic:
by
  simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
intro h t ht
    refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
    rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
exact IsOpen.preimage_val ht

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 : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst✝¹] s
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Tactic:
by
  simp only [continuousOn_iff_continuous_domRestrict, (h.restrictPreimage_isOpen hs).continuous_iff]
  rfl

Goal state after: