mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ ∀ W' ∈ Set.range fun i ↦ W i, W'.RespectsIso

Tactic:
by simpa

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ P.map (F ⋙ G) ≤ (P.map F).map G

Tactic:
rw [map_le_iff]
    intro X Y f hf
    exact map_mem_map _ _ _ (map_mem_map _ _ _ hf)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
⊢ P.map F = P.map G

Tactic:
by
  revert F G e
  suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
    fun F G e => le_antisymm (this e) (this e.symm)
  intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩
  exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

Tactic:
intro X Y Z e f
      simp only [monomorphisms.iff]
      intro
      apply mono_comp

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

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
intro X Y Z e f
      simp only [monomorphisms.iff]
      intro
      apply mono_comp

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))

Tactic:
by
        rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp, assoc, assoc]
        calc
        _ = (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right := by
          rw [← Functor.comp_map, ← α.naturality_assoc]
        _ = α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right) := by
          simp only [Functor.comp_map, Functor.map_preimage, ← map_obj_hom α β Y, φ.w,
            map_obj_hom α β X, assoc]
        _ = _ := by rw [← Functor.comp_map, β.naturality]

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
lift : (s : Cone F) → s ⟶ t
uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ { hom := m, w := w } = lift s

Tactic:
apply uniq

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
by apply G.map_injective; rw [G.map_comp, h]; apply ht.fac

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X : C
R : F.RepresentableBy X
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.obj X).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
intro X Y f
    ext x
    exact R.homEquiv_comp f.unop _

Goal state after:
Module: Mathlib.CategoryTheory.Thin

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
x✝¹ x✝ : D ⥤ C
α β : x✝¹ ⟶ x✝
⊢ α.app = β.app

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Thin

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁.hom = i₂.hom

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map
X : Type u
⊢ autoParam
    (∀ (X_1 Y : Discrete X) (f : X_1 ⟶ Y),
      (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).map f =
        eqToHom ⋯ ≫ (𝟭 (Discrete X)).map f ≫ eqToHom ⋯)
    ext._auto_1

Tactic:
intro X Y f
      cases f
      apply ULift.ext
      cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (Arrow C)

Tactic:
by
  let φ (f : Arrow C) : Σ (s t : C), s ⟶ t := ⟨_, _, f.hom⟩
  refine small_of_injective (f := φ) ?_
  rintro ⟨s, t, f⟩ ⟨s', t', f'⟩ h
  obtain rfl : s = s' := congr_arg Sigma.fst h
  simp only [Sigma.mk.injEq, heq_eq_eq, true_and, φ] at h
  obtain rfl : t = t' := h.1
  obtain rfl : f = f' := by simpa using h
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ ∀ (x : (X : C) → Unique (X ⟶ Y)), (fun X ↦ { default := default, uniq := ⋯ }) = x

Tactic:
subsingleton

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
j j' : J
hj : j = j'
⊢ π F j ≫ eqToHom ⋯ = π F j'

Tactic:
by
  subst hj
  simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
j j' : J
hj : j = j'
⊢ eqToHom ⋯ ≫ ι F j = ι F j'

Tactic:
by
  subst hj
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (c.π.app X)

Tactic:
by
  change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom
  infer_instance

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
j : J
⊢ limMap (α ≫ β) ≫ limit.π Z✝ j = (limMap α ≫ limMap β) ≫ limit.π Z✝ j

Tactic:
simp [assoc]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → f ≫ g ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs)) (f ≫ g)
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦ Z✝ = X → f ≫ g ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs))
          (fun h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ (f ≫ g))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ (f ≫ g))
      ⋯ ⋯ ⋯ =
    Hom.casesOn (motive := fun a a_1 x ↦
        X✝ = a → Y✝ = a_1 → f ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) f
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Y✝ = X → f ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ f)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) → Y✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Y✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ f)
        ⋯ ⋯ ⋯ ≫
      Hom.casesOn (motive := fun a a_1 x ↦
        Y✝ = a → Z✝ = a_1 → g ≍ x → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Z✝ B objs)) g
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Z✝ = X → g ≍ Hom.id X → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Z✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : Y✝ ⟶ Y) → f ≍ Hom.id Y✝ → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn Y✝ B objs)) ⋯ g)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ g)
        ⋯ ⋯ ⋯

Tactic:
by
    cases f
    · simp only [hom_id, Category.id_comp]; congr
    · cases g
      simp only [hom_id, Category.comp_id]; congr

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ default = j

Tactic:
subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ j = default

Tactic:
subsingleton

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ IsIso c.fst

Tactic:
exact
      ⟨⟨l,
          BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
            (h.hom_ext _ _),
          hl⟩⟩

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ ∀ (s : Fan K.obj) (j : J),
    hc.lift { pt := s.pt, π := { app := fun j ↦ s.proj j, naturality := ⋯ } } ≫ (Fan.mk c.pt c.π.app).proj j = s.proj j

Tactic:
subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ ∀ (s : Fan K.obj) (m : s.pt ⟶ (Fan.mk c.pt c.π.app).pt),
    (∀ (j : J), m ≫ (Fan.mk c.pt c.π.app).proj j = s.proj j) →
      m = hc.lift { pt := s.pt, π := { app := fun j ↦ s.proj j, naturality := ⋯ } }

Tactic:
subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cocone K
hc : IsColimit c
⊢ ∀ (t : Cofan K.obj) (j : J),
    (Cofan.mk c.pt c.ι.app).inj j ≫ hc.desc { pt := t.pt, ι := { app := fun j ↦ t.inj j, naturality := ⋯ } } = t.inj j

Tactic:
subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cocone K
hc : IsColimit c
⊢ ∀ (t : Cofan K.obj) (m : (Cofan.mk c.pt c.ι.app).pt ⟶ t.pt),
    (∀ (j : J), (Cofan.mk c.pt c.ι.app).inj j ≫ m = t.inj j) →
      m = hc.desc { pt := t.pt, ι := { app := fun j ↦ t.inj j, naturality := ⋯ } }

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Tactic:
by ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ lift fst snd = 𝟙 (X ⨯ Y)

Tactic:
by ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ map h k = lift (f ≫ h) (g ≫ k)

Tactic:
by ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ map f g ≫ map h k = map (f ≫ h) (g ≫ k)

Tactic:
by ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ desc inl inr = 𝟙 (X ⨿ Y)

Tactic:
by ext <;> simp

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

Goal state before:
pp: case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ inr ≫ i₁ = inr ≫ i₂

Tactic:
rw [← cancel_epi g]
      simpa using congr_arg (fun f => coprod.inr ≫ f) h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w :
  ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
dsimp at w

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = t.π.app WalkingCospan.left ≫ f
⊢ t.π.app WalkingCospan.one = t.fst ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w :
  (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
dsimp at w

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ t.ι.app WalkingSpan.left = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ = map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = 𝟙 (pullback f g)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ = map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (pushout f g)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ pullbackComparison (F ⋙ G) f g ≫ pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)

Tactic:
· rw [pullbackComparison_comp_snd]
    simp [← Functor.map_comp]

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : StructuredArrow c (Comma.fst F G)
f : X✝ ⟶ Y✝
⊢ { left := Under.mk X✝.hom, right := X✝.right.right, hom := X✝.right.hom }.left.hom ≫ (Hom.right f).left =
    { left := Under.mk Y✝.hom, right := Y✝.right.right, hom := Y✝.right.hom }.left.hom

Tactic:
simp [dsimp% f.w]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = ι f

Tactic:
convert! t₀ using 1

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = v ≫ q ≫ ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∀ (a : { as := PUnit.unit } ⟶ { as := PUnit.unit }), a = 𝟙 { as := PUnit.unit }

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
f : 0 ⟶ 0
⊢ f = 𝟙 0

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ preComp f (g ≫ h) ≫ preComp g h = eqToHom ⋯ ≫ preComp (f ≫ g) h

Tactic:
by
  apply (cancel_mono (image.ι h)).1
  simp only [preComp, Category.assoc, fac, lift_mk_comp, eqToHom]
  rw [image.lift_fac]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
Subsingleton.elim x (0 : M)

Goal state after:
R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : X ⟶ M
x : ↑X
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
subsingleton

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsZero X ∧ IsZero Y → IsIso 0

Tactic:
intro ⟨hX, hY⟩
    exact (isIsoZeroEquivIsoZero _ _).symm ⟨hX.isoZero, hY.isoZero⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ 𝟙 (⊥_ C) = 0

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) = 0

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')

Tactic:
obtain - | j := j
    · obtain - | j' := j'
      · exact {Hom.id none}
      · exact {Hom.init j'}
    · by_cases h : some j = j'
      · rw [h]
        exact {Hom.id j'}
      · exact ∅

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')

Tactic:
by
    obtain - | j := j
    · obtain - | j' := j'
      · exact {Hom.id none}
      · exact {Hom.init j'}
    · by_cases h : some j = j'
      · rw [h]
        exact {Hom.id j'}
      · exact ∅

Goal state after: