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✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁

Tactic:
← cancel_mono S.f,

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
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ (S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯) ≫ S.f = 𝟙 S.X₁ ≫ S.f
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ imageSubobject S.f = kernelSubobject S.g

Tactic:
exact Subobject.eq_of_comm (asIso (imageToKernel _ _ S.zero)) (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl ≫ (opProdIsoCoprod A B).inv = prod.fst.op

Tactic:
Iso.comp_inv_eq,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl = prod.fst.op ≫ (opProdIsoCoprod A B).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr ≫ (opProdIsoCoprod A B).inv = prod.snd.op

Tactic:
Iso.comp_inv_eq,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr = prod.snd.op ≫ (opProdIsoCoprod A B).hom
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
F : C ⥤ H
Y : D
L L' : C ⥤ D
e : L ≅ L'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso (fromPUnit Y) e.symm
e' : StructuredArrow.proj Y L' ⋙ F ≅ Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F :=
  Iso.refl (StructuredArrow.proj Y L' ⋙ F)
⊢ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
exact hasLimit_of_iso e'.symm

Goal state after:
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 : 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:
constructor
  · intro
    exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e
  · intro
    exact hasPointwiseLeftKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

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
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)

Tactic:
by
  dsimp [ran, ranCounit]
  infer_instance

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' : C ⥤ D'
G : D ⥤ D'
inst✝¹ : G.IsEquivalence
f : L ⋙ G ⟶ L'
inst✝ : IsIso f
F : C ⥤ H
⊢ (RightExtension.postcomp₁ G f F).IsEquivalence

Tactic:
apply CostructuredArrow.isEquivalenceMap₂

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
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
⊢ (RightExtension.precomp L F G).IsEquivalence

Tactic:
apply CostructuredArrow.isEquivalenceMap₂

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) (YonedaCollection.snd (id p).val) =
    YonedaCollection.snd ((counitForward F s ∘ counitBackward F s) p).val

Tactic:
simp [counitBackward]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ (counitBackward F s ∘ counitForward F s) x = id x

Tactic:
simp [counitBackward]

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv = α.app i ≫ colimit.ι F' (L.obj i)

Tactic:
Iso.comp_inv_eq,

Goal state after:
C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ colimit.ι F i = (α.app i ≫ colimit.ι F' (L.obj i)) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
⊢ HasCokernel f

Tactic:
by
      have : PreservesColimits G := adj.leftAdjoint_preservesColimits
      have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by
        simpa using NatIso.naturality_1 i f
      rw [← this]
      have : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
      apply Limits.hasCokernel_epi_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✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X)) ≫
      ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y

Tactic:
ext Z ⟨f⟩
      simpa [uliftYonedaEquiv, uliftYoneda] using
        ConcreteCategory.congr_hom (CC := fun X ↦ X) (Y.hom.naturality f.op).symm (ULift.up (𝟙 _))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ IsIso f ↔ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))

Tactic:
by
  constructor
  · intro h
    rw [isIso_iff_yoneda_map_bijective] at h
    intro A _
    exact (h A).2
  · intro hf
    refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
    · exact hf A hA g
    · intro l₁ l₂ h₁ h₂
      rw [← cancel_mono f, h₁, h₂]

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
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π

Tactic:
Iso.comp_inv_eq,

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.π = s.π ≫ i.hom
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : c.pt ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝
b : β
g : f b ⟶ x✝³
⊢ g ≫ x✝¹ = g ≫ x✝

Tactic:
simpa using c.inj b ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

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

Goal state before:
pp: C : Type u
F : C → Type v
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (fun x ↦
          match j', x with
          | { as := i }, x => ⟨i, x⟩) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      fun x ↦
      match j, x with
      | { as := i }, x => ⟨i, x⟩

Tactic:
by
    rintro ⟨i⟩ ⟨j⟩ f
    obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
    rfl

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

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j' with
        | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))

Tactic:
by
    rintro ⟨i⟩ ⟨j⟩ f
    obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
    rfl

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d

Tactic:
order

Goal state after:
case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
_order_neg_goal✝ : ¬a < d
⊢ False
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ c < a

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d

Tactic:
order

Goal state after:
case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
_order_neg_goal✝ : ¬a < d
⊢ False
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ c < a

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
order

Goal state after:
case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
_order_neg_goal✝ : ¬d < c
⊢ False
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
order

Goal state after:
case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
_order_neg_goal✝ : ¬d < c
⊢ False
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a

Tactic:
order

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d

Tactic:
order

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ -f x = ↑(-1) • f x

Tactic:
Units.val_neg,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ -f x = -↑1 • f x
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ c (xs n) (ys n)

Tactic:
apply hleft

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

Goal state before:
pp: case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : φ a = φ (2 * a)
ha' : ¬a = 0
h : 2 * a = b
⊢ False

Tactic:
totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha),

Goal state after:
case neg
a b : ℕ
h✝ : a ∣ b
ha : Even a
h' : φ a = 2 * φ a
ha' : ¬a = 0
h : 2 * a = b
⊢ False
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
x : ι → X
a : X
⊢ MapClusterPt a atTop x ↔ ∀ (i : ι), a ∈ closure[inst✝³] (x '' Ici i)

Tactic:
by
  simp [MapClusterPt, (atTop_basis.map x).clusterPt_iff_forall_mem_closure]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case inr
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ y ∈ closure[inst✝¹] {x}ᶜ

Tactic:
exact subset_closure hne

Goal state after:
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 : ℤ
⊢ toIocDiv hp (a + ↑m * p) b = toIocDiv hp a b - m

Tactic:
simpa using toIocDiv_add_zsmul' hp a b m

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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ Dense s ↔ ∀ (x : X), f x ∈ closure[inst✝¹] (f '' s)

Tactic:
by
  simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
rw [← Set.biUnion_of_singleton s]

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2

Tactic:
by
  have hX := continuous_sInf_dom hX continuous_id
  have hY := continuous_sInf_dom hY continuous_id
  have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY
  exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p✝ p q : X → Prop
hpq : p = q
x : X
⊢ p x → q (id x)

Tactic:
simp [hpq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p✝ p q : X → Prop
hpq : p = q
x : X
⊢ q x → p (id x)

Tactic:
simp [hpq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ s_1 ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, IsOpen[generateFrom s] s_1

Tactic:
rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩

Goal state after:
case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : t.Finite
htb : t ⊆ s
⊢ IsOpen[generateFrom s] ((fun f ↦ ⋂₀ f) t)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsOpen[inst✝] s
h : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsOpen[inst✝] (s ∩ t)

Tactic:
by simpa using hs.isOpenMap_subtype_val _ h

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)

Tactic:
rw [← image_univ]
  exact (hf.domRestrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∃ n, accumulate s n = univ) ↔ ∃ n, s n = univ

Tactic:
refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩
  contrapose!
  intro h n
  obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n
  grind

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
s : Set ((i : ι) → X i)
x✝ : s ∈ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
t : (a : ι) → Set (X a)
ht : ∀ (a : ι), t a ∈ g a
Eq : s = univ.pi t
⊢ (∀ a ∈ Finset.univ, t a ∈ g a) ∧ s = (↑Finset.univ).pi t

Tactic:
by simp [ht, Eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
x : n → X
⊢ 𝓝 x = comap (fun x ↦ x ∘ f) (𝓝 (x ∘ f))

Tactic:
simp only [nhds_pi, Filter.pi, Filter.comap_iInf, ← hf.iInf_congr, Filter.comap_comap,
    Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun x ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
rw [tendsto_smallSets_iff]

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb
Module: Mathlib.Topology.Compactness.Compact

Goal state before:

Tactic:
f ⊓ (comap g (cocompact Y))
    _ ≤ f ⊓ Filter.cocompact X := inf_le_inf_left f (Filter.comap_cocompact_le hg)
    _ = ⊥ := disjoint_iff.mp hf

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S

Tactic:
rw [specializes_iff_forall_closed]
  push Not
  rfl

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S

Tactic:
by
  rw [specializes_iff_forall_closed]
  push Not
  rfl

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f cofinite (cocompact Y)

Tactic:
convert! hf

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X