mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
⊢ ∃! g', ↑S g' ∘ₗ h = r

Tactic:
let r' : M →ₗ[R] Q := r ∘ₗ f

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
⊢ ∃! g', ↑S g' ∘ₗ h = r
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (f ⁻¹' s).sym2 = Sym2.map f ⁻¹' s.sym2

Tactic:
ext ⟨x, y⟩
  simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
Φ : Symmetrify V ⥤q V'
hΦ : of ⋙q Φ = φ
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift φ

Tactic:
subst_vars
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    cases f
    · rfl
    · exact hΦinv (Sum.inl _)

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case mp
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
X : P.FullSubcategory
e : (P.ι ⋙ F).obj X ≅ Y
⊢ P.map F Y

Tactic:
exact ⟨X.1, X.2, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
Z' : C
h : unop X ⟶ Z'
⊢ (f ≫ g).unop ≫ h = g.unop ≫ f.unop ≫ h

Tactic:
simp only [unop_comp, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).unop = inv f.unop

Tactic:
apply IsIso.eq_inv_of_hom_inv_id
  rw [← unop_comp, IsIso.inv_hom_id, unop_id]

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)

Tactic:
rw [← comp_apply, Iso.hom_inv_id, id_apply]

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (⨅ i, W i).RespectsLeft Q

Tactic:
rw [← sInf_range]
  exact sInf (by simpa)

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (⨅ i, W i).RespectsRight Q

Tactic:
rw [← sInf_range]
  exact sInf (by simpa)

Goal state after:
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
⊢ (⨅ i, W i).RespectsIso

Tactic:
rw [← sInf_range]
  exact sInf (by simpa)

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
⊢ ∀ (x y : Aut X),
    { hom := h.inv ≫ (x * y).hom ≫ h.hom, inv := h.inv ≫ (x * y).inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ } =
      { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ } *
        { hom := h.inv ≫ y.hom ≫ h.hom, inv := h.inv ≫ y.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by simp [Aut_mul_def]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)

Tactic:
rw [Equiv.eq_symm_apply, he]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ (e X Y) ((e X Y).symm g) = f ≫ g
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = f ◁ (λ_ g).hom

Tactic:
inv_hom_id_assoc

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).hom = f ◁ (λ_ g).hom
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Quiver.IsThin C
⊢ ∀ (a b : C), ⟦a⟧ ≤ ⟦b⟧ → ⟦b⟧ ≤ ⟦a⟧ → ⟦a⟧ = ⟦b⟧

Tactic:
rintro _ _ ⟨f⟩ ⟨g⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Quiver.IsThin C
a✝ b✝ : C
f : a✝ ⟶ b✝
g : b✝ ⟶ a✝
⊢ ⟦a✝⟧ = ⟦b✝⟧
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f =
    hi.inv ≫
      hl.desc { pt := c.pt, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }

Tactic:
by
    dsimp
    rw [← hl.uniq _ (hi.hom ≫ f) _]
    · simp only [Iso.inv_hom_id_assoc]
    · simp

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✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
⊢ pre (E ⋙ F) D ≫ pre F E = pre F (D ⋙ E)

Tactic:
ext j
  rw [← assoc, colimit.ι_pre, colimit.ι_pre]
  have : HasColimit ((D ⋙ E) ⋙ F) := h
  exact (colimit.ι_pre F (D ⋙ E) j).symm

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

Goal state before:
pp: case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) =
      t.inj j

Tactic:
intro t

Goal state after:
case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
⊢ ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) =
      t.inj j
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) =
      t.inj j

pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))

Tactic:
· intro t ⟨a, b⟩
    simp only [mk_pt, cofan_mk_inj, Category.assoc]
    erw [hc.fac, (hs a).fac]
    rfl

Goal state after:
case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))

Tactic:
intro t

Goal state after:
case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
⊢ ∀
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }

Tactic:
exact hd₂ _ _

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

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right }))
    (m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt),
    (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
· intro s m e₁ e₂
    apply BinaryCofan.IsColimit.hom_ext h
    · rw [← cancel_epi f]
      simpa using e₁
    · simpa

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ ∀ ⦃X Y : WalkingCospan⦄ (f : X ⟶ Y),
    (F.map f ≫ Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r) =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map f

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    F.map f ≫ (Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r).hom =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map f

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ ∀ ⦃X Y : WalkingSpan⦄ (f : X ⟶ Y),
    (F.map f ≫ Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r) =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map f

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ ∀ {X Y : WalkingSpan} (f : X ⟶ Y),
    F.map f ≫ (Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r).hom =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map f

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ f.homMk' (𝟙 f.left) = eqToHom ⋯

Tactic:
by
  simp [eqToHom_left]

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
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ f.hom ≫ Hom.right k ≫ l = (f.hom ≫ Hom.right k) ≫ m

Tactic:
a,

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ f.hom ≫ Hom.right k ≫ m = (f.hom ≫ Hom.right k) ≫ m
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y' Y'' : C
S : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ f.homMk' (g' ≫ g) = eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g

Tactic:
by
  simp [eqToHom_left]

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inr f g ≫ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = pushout.inr f g ≫ 𝟙 (pushout f g)

Tactic:
· simp [pushout.condition]

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

Goal state before:
pp: case op
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : op i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
induction j with | _ j

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
⊢ ∀ {X Y : (StructuredArrow d F)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫ (StructuredArrow.isoMk (Iso.refl (unop Y).right) ⋯).op.hom =
      (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op.hom ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ f
      obtain ⟨X, x, rfl⟩ := X.mk_surjective
      obtain ⟨Y, y, rfl⟩ := Y.mk_surjective
      exact Quiver.Hom.unop_inj (by ext; apply Quiver.Hom.op_inj (by simp))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
⊢ ∀ {X Y : (CostructuredArrow F d)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫ (CostructuredArrow.isoMk (Iso.refl (unop Y).left) ⋯).op.hom =
      (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op.hom ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ f
      obtain ⟨X, x, rfl⟩ := X.mk_surjective
      obtain ⟨Y, y, rfl⟩ := Y.mk_surjective
      exact Quiver.Hom.unop_inj (by ext; apply Quiver.Hom.op_inj (by simp))

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

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
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
by
    let em : StrongEpiMonoFactorisation (F.inv.map f) :=
      (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
    have : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
    have : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
    exact
      Nonempty.intro
        { I := F.obj em.I
          e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
          m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
          fac := by
            simp only [Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc] }

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✝ : HasZeroObject C
X Y : C
⊢ IsIso 0 ↔ IsZero X ∧ IsZero Y

Tactic:
constructor
  · intro h
    let h' := isIsoZeroEquivIsoZero _ _ h
    exact ⟨(isZero_zero _).of_iso h'.1, (isZero_zero _).of_iso h'.2⟩
  · intro ⟨hX, hY⟩
    exact (isIsoZeroEquivIsoZero _ _).symm ⟨hX.isoZero, hY.isoZero⟩

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := ⋯
l : { l // c.π ≫ l = s'.π } := ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m✝ = s.π
⊢ c.π ≫ m✝ = c.π ≫ ↑l

Tactic:
rw [Cofork.π_ofπ] at hm

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : c.π ≫ m✝ = s.π
⊢ c.π ≫ m✝ = c.π ≫ ↑l
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

Tactic:
by_cases h : some j = j'

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')

case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ ι' ≫ f = 0

Tactic:
by rw [← h, w]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : PreservesFiniteLimits X✝
⊢ PreservesFiniteLimits Y✝

Tactic:
exact preservesFiniteLimits_of_natIso e

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel f
inst✝ : Mono g
⊢ kernel.ι (f ≫ g) ≫ f = 0

Tactic:
rw [← cancel_mono g]
        simp

Goal state after: