mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a b a' b' : α
h : Rel α (a, b) (a', b')
hx : a' = b'
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ hx = a'

Tactic:
cases hx
    cases h <;> rfl

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₂ : Path b b
hq : nil.length = q₂.length
h : p₁.comp nil = p₂.comp q₂
⊢ p₁ = p₂ ∧ nil = q₂

Tactic:
| nil =>

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

Goal state before:
pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ f₂ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₁.comp q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : (q₁.cons f₁).length = (q₁.cons f₂).length
h : b✝ = b✝ ∧ p₁.comp q₁ ≍ p₁.comp q₁ ∧ f₁ ≍ f₂
⊢ p₁ = p₁ ∧ q₁.cons f₂ = q₁.cons f₂

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a b : V
n : ℕ
hp : nil.length = n + 1
⊢ ∃ c f q x, nil = f.toPath.comp q

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
⊢ (p.comp nil).reverse = nil.reverse.comp p.reverse

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
⊢ nil.reverse.reverse = nil

Tactic:
| nil =>

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

Goal state before:
pp: case refine_1.nil
V : Type u_1
inst✝ : Quiver V
a : V
h : nil.length ≠ 0
⊢ ∃ c p' e, nil = p'.cons e

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u₁
inst✝² : Quiver V
W : Type u₂
inst✝¹ : Quiver W
F : V ⥤q W
U : Type u₃
inst✝ : Quiver U
G : W ⥤q U
a b : V
⊢ (F ⋙q G).mapPath Path.nil = G.mapPath (F.mapPath Path.nil)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P Q : ObjectProperty C
F : C ⥤ D
⊢ ∀ {X Y : D} (x : X ≅ Y), P.map F X → P.map F Y

Tactic:
by
    rintro _ _ e ⟨X, hX, ⟨e'⟩⟩
    exact ⟨X, hX, ⟨e' ≪≫ e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom ⋯)

Tactic:
rw [α.naturality_assoc]
  simp [eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.unop ≫ g.unop = h.unop ≫ f.unop

Tactic:
by simp only [← unop_comp, p.w]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget SemiRingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toSemiRingCatIso.isIso_hom

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = coconeOfHom h (homOfCocone h s)

Tactic:
apply (coconeOfHom_fac _ _).symm

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 : D ⥤ C
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 : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (e X Y') (f ≫ g) = (e X Y) f ≫ (rightAdjointOfEquiv e he).map g

Tactic:
intro X Y Y' g h
        simp [← he, reassoc_of% (he'' e)]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app (op X))) (e.homEquiv (f ≫ g)) =
    (ConcreteCategory.hom (F'.map f.op)) ((ConcreteCategory.hom (e'.hom.app (op X'))) (e.homEquiv g))

Tactic:
e.homEquiv_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app (op X))) ((ConcreteCategory.hom (F.map f.op)) (e.homEquiv g)) =
    (ConcreteCategory.hom (F'.map f.op)) ((ConcreteCategory.hom (e'.hom.app (op X'))) (e.homEquiv g))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : C ⥤ Type v
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app Y')) (e.homEquiv (f ≫ g)) =
    (ConcreteCategory.hom (F'.map g)) ((ConcreteCategory.hom (e'.hom.app Y)) (e.homEquiv f))

Tactic:
e.homEquiv_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : C ⥤ Type v
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app Y')) ((ConcreteCategory.hom (F.map g)) (e.homEquiv f)) =
    (ConcreteCategory.hom (F'.map g)) ((ConcreteCategory.hom (e'.hom.app Y)) (e.homEquiv f))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
| e.homEquiv (f ≫ 𝟙 Y)

Tactic:
e.homEquiv_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
| (ConcreteCategory.hom (F.map f.op)) (e.homEquiv (𝟙 Y))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
| e.homEquiv (𝟙 X ≫ f)

Tactic:
e.homEquiv_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
| (ConcreteCategory.hom (F.map f)) (e.homEquiv (𝟙 X))
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
k : c ⟶ d
⊢ η.hom ▷ h ▷ k ≫ η.inv ▷ h ▷ k = 𝟙 ((f ≫ h) ≫ k)

Tactic:
by
  simp [← comp_whiskerRight]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
k : c ⟶ d
⊢ η.inv ▷ h ▷ k ≫ η.hom ▷ h ▷ k = 𝟙 ((g ≫ h) ≫ k)

Tactic:
by
  simp [← comp_whiskerRight]

Goal state after:
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
⊢ (ρ_ (𝟙 a)).hom ▷ f ▷ g ≫ (α_ (𝟙 a) f g).hom = (α_ (𝟙 a ≫ 𝟙 a) f g).hom ≫ (ρ_ (𝟙 a)).hom ▷ (f ≫ g)

Tactic:
associator_naturality_left

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ (𝟙 a ≫ 𝟙 a) f g).hom ≫ (ρ_ (𝟙 a)).hom ▷ (f ≫ g) = (α_ (𝟙 a ≫ 𝟙 a) f g).hom ≫ (ρ_ (𝟙 a)).hom ▷ (f ≫ g)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv.symm x ≫ f = yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op X))) x)

Tactic:
by
  apply yonedaEquiv.injective
  simp [yonedaEquiv_comp]

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k ≫ s.π.app none = l ≫ s.π.app none

Tactic:
exact hbase

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
a : α
b : β a
⊢ π a b ≫ c.inj a ≫ hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) = t.inj ⟨a, b⟩

Tactic:
erw [hc.fac, (hs a).fac]

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
a : α
b : β a
⊢ (mk t.pt fun b ↦ t.inj ⟨{ as := a }.as, b⟩).ι.app { as := 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
h :
  ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        m =
      t.inj j
x✝¹ : Discrete α
a : α
x✝ : Discrete (β a)
b : β a
⊢ (mk (X a) (π a)).ι.app { as := b } ≫ c.ι.app { as := a } ≫ m =
    (mk (X a) (π a)).ι.app { as := b } ≫
      c.ι.app { as := a } ≫ hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))

Tactic:
erw [hc.fac, (hs a).fac]

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
h :
  ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        m =
      t.inj j
x✝¹ : Discrete α
a : α
x✝ : Discrete (β a)
b : β a
⊢ (mk (X a) (π a)).ι.app { as := b } ≫ c.ι.app { as := a } ≫ m =
    (mk t.pt fun b ↦ t.inj ⟨{ as := a }.as, b⟩).ι.app { as := b }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X Y : C
s : BinaryFan X Y
⊢ snd ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)) =
    (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)).pt).hom ≫ (map F s).snd

Tactic:
by simp [snd]

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

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
inst✝¹ : T.Full
inst✝ : T.Faithful
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι.app j ≫ m = c.ι.app j
⊢ m.right = (homMk (T.preimage c.pt.hom) ⋯).right

Tactic:
apply T.map_injective
      simpa only [homMk_right, T.map_preimage, ← w m] using! (Category.id_comp _).symm

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
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
x✝³ x✝² : StructuredArrow S F
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (post S F G).map x✝¹ = (post S F G).map x✝
⊢ x✝¹ = x✝

Tactic:
simpa [ext_iff] using h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ g₁ ≫ 𝟙 Z = 𝟙 Y ≫ g₂

Tactic:
simp [h₂]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁

Tactic:
simp [h₂]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ g₁ ≫ 𝟙 Z = 𝟙 X ≫ g₂

Tactic:
simp [h₂]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁

Tactic:
simp [h₂]

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 T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
x✝³ x✝² : CostructuredArrow F S
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (post F G S).map x✝¹ = (post F G S).map x✝
⊢ x✝¹ = x✝

Tactic:
simpa [ext_iff] using h

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

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ Z✝ : Arrow (J ⥤ C)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) ⋯),
      naturality := ⋯ } =
    { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯),
        naturality := ⋯ } ≫
      { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯),
        naturality := ⋯ }

Tactic:
ext j
    dsimp
    rw [← data.mapZ_comp]
    congr 1

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✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ f = image.ι f

Tactic:
by
  simp only [← imageMonoIsoSource_inv_ι f]
  rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasTerminal C
inst✝¹ : HasTerminal D
inst✝ : PreservesLimit (Functor.empty C) G
⊢ IsIso (terminalComparison G)

Tactic:
rw [← PreservesTerminal.iso_hom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasTerminal C
inst✝¹ : HasTerminal D
inst✝ : PreservesLimit (Functor.empty C) G
⊢ IsIso (PreservesTerminal.iso G).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
⊢ c.snd ≫ h ≫ f = c.snd ≫ h ≫ g

Tactic:
← c.condition_assoc,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
⊢ c.fst ≫ s.ι ≫ f = c.snd ≫ h ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
⊢ c.fst ≫ s.ι ≫ f = c.snd ≫ h ≫ g

Tactic:
← c.condition_assoc,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
⊢ c.fst ≫ s.ι ≫ f = c.fst ≫ s.ι ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case toFun
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ ∀ (a : (X ≅ 0) × (Y ≅ 0)), 𝟙 X = 0 ∧ 𝟙 Y = 0

Tactic:
rintro ⟨eX, eY⟩

Goal state after:
case toFun
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3✝ : L.obj c.pt = (L.mapCocone c).pt
e_4✝ : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ α.app (K.obj j) ≫ L'.map (c.ι.app j) =
    L.map (c.ι.app j) ≫ (isColimitOfPreserves L hc).map (L'.mapCocone c) (K.whiskerLeft α)

Tactic:
refine (((isColimitOfPreserves L hc).ι_map (L'.mapCocone c) (whiskerLeft K α) j).trans ?_).symm

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3✝ : L.obj c.pt = (L.mapCocone c).pt
e_4✝ : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ (K.whiskerLeft α).app j ≫ (L'.mapCocone c).ι.app j = α.app (K.obj j) ≫ L'.map (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ coequalizer.π f 0 ≫ map f f' p q h₁ ≫ desc f' g' w' = coequalizer.π f 0 ≫ desc f g w ≫ r

Tactic:
simp [h₂]

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
⊢ (if h : g k = g k' then eqToHom ⋯ else 0) = if h : k = k' then eqToHom ⋯ else 0

Tactic:
split_ifs with h h' h'

Goal state after:
case pos
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : g k = g k'
h' : k = k'
⊢ eqToHom ⋯ = eqToHom ⋯

case neg
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : g k = g k'
h' : ¬k = k'
⊢ eqToHom ⋯ = 0

case pos
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : ¬g k = g k'
h' : k = k'
⊢ 0 = eqToHom ⋯

case neg
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : ¬g k = g k'
h' : ¬k = k'
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁸ : Category.{uC', uC} C✝
inst✝⁷ : HasZeroMorphisms C✝
D : Type uD
inst✝⁶ : Category.{uD', uD} D
inst✝⁵ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
j✝¹ j✝ : J
⊢ ι f j✝ ≫ map p ≫ π g j✝¹ = ι f j✝ ≫ ((isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv) ≫ π g j✝¹

Tactic:
simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc, ι_π_assoc]

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁸ : Category.{uC', uC} C✝
inst✝⁷ : HasZeroMorphisms C✝
D : Type uD
inst✝⁶ : Category.{uD', uD} D
inst✝⁵ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
j✝¹ j✝ : J
⊢ (if h : j✝ = j✝¹ then eqToHom ⋯ else 0) ≫ p j✝¹ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝¹
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.toCocone.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
dsimp at m
      have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
      have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : Y ⟶ T, hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₁'
      rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
⊢ (addRightEmbedding fun t ↦ if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t ↦ if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t ↦ if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Tactic:
have := hg i

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
this : ¬g i = 0 → i ∈ s
⊢ (addRightEmbedding fun t ↦ if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t ↦ if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t ↦ if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g : Perm α
⊢ f.Disjoint g⁻¹ ↔ f.Disjoint g

Tactic:
by
  rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case nil
α : Type u_1
f : Perm α
h : ∀ g ∈ [], f.Disjoint g
⊢ f.Disjoint [].prod

Tactic:
| nil =>

Goal state after: