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

Goal state before:
pp: α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, y) :: s(y, x) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2))

Tactic:
2,

Goal state after:
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, x) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2))
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ {s(y, y)} + (↑(List.map (fun y_1 ↦ s(y, y_1)) xs) + ({s(x, x)} + (↑(List.map (fun y ↦ s(x, y)) xs) + ↑xs.sym2))) =
    {s(x, x)} + (↑(List.map (fun y ↦ s(x, y)) xs) + ({s(y, y)} + (↑(List.map (fun y_1 ↦ s(y, y_1)) xs) + ↑xs.sym2)))

Tactic:
simp only [add_left_comm]

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
⊢ x ∈ (↑k).toFinset → x ∈ s
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
obtain hab | hba := le_total a b

Goal state after:
case h.h.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = LinearMap.id

Tactic:
← LinearMap.cancel_left (ULift.moduleEquiv : ULift.{max v₁ v₃} N ≃ₗ[S] N).symm.injective

Goal state after:
case refine_1
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
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = ↑ULift.moduleEquiv.symm ∘ₗ LinearMap.id
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ P.isoClosure X ≤ P X

Tactic:
⟨Y, hY, ⟨e⟩⟩

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y : C
hY : P Y
e : X ≅ Y
⊢ P X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
D : Type u_3
inst✝ : Category.{u_4, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
by
  subst h
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
inst✝ : Category.{u_3, u_2} C
P : ObjectProperty C
X Y : P.FullSubcategory
h : X = Y
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
by
  subst h
  rfl

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
by
  subst h
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
F : C ⥤ E
⊢ ((whiskeringLeft D C E).obj e.inverse).map ((ofComponents (fun F ↦ (e.funInvIdAssoc F).symm) ⋯).hom.app F) ≫
      (ofComponents (fun F ↦ e.invFunIdAssoc F) ⋯).hom.app (((whiskeringLeft D C E).obj e.inverse).obj F) =
    𝟙 (((whiskeringLeft D C E).obj e.inverse).obj F)

Tactic:
ext X
    dsimp
    simp only [funInvIdAssoc_inv_app, id_obj, comp_obj, invFunIdAssoc_hom_app,
      Functor.comp_map, ← F.map_comp, unit_inverse_comp, map_id]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ p.unop ≫ l.l.unop = g.unop

Tactic:
by rw [← unop_comp, l.fac_right]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ l₁.l = l₂.l

Tactic:
← cancel_epi i

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ i ≫ l₁.l = i ≫ l₂.l
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ∀ (x : X),
    (ConcreteCategory.hom (↾f ≫ homEquiv.symm (⇑Equiv.ulift.symm ∘ g₁))) x =
      (ConcreteCategory.hom (↾f ≫ homEquiv.symm (⇑Equiv.ulift.symm ∘ g₂))) x

Tactic:
intro x

Goal state after:
case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
x : X
⊢ (ConcreteCategory.hom (↾f ≫ homEquiv.symm (⇑Equiv.ulift.symm ∘ g₁))) x =
    (ConcreteCategory.hom (↾f ≫ homEquiv.symm (⇑Equiv.ulift.symm ∘ g₂))) x
Module: Mathlib.Algebra.Category.Grp.Basic

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

Tactic:
by
    let i := asIso ((forget CommGrpCat).map f)
    let e : X ≃* Y := { i.toEquiv with map_mul' := by simp [Iso.toEquiv, i] }
    exact e.toCommGrpIso.isIso_hom

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

Tactic:
X'

Goal state after:
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 X' : C
⊢ ∀ {Y : D} (f : X ⟶ X') (g : X' ⟶ (rightAdjointOfEquiv e he).obj Y), (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g
Module: Mathlib.CategoryTheory.Category.ULift

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : AsSmall C
h : X = Y
⊢ (eqToHom h).down = eqToHom ⋯

Tactic:
by
  subst h
  rfl

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

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
⊢ ∀ (X Y : ↑(typeToCat.obj X✝)) (f : X ⟶ Y),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
      eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯

Tactic:
intro x

Goal state after:
X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
x : ↑(typeToCat.obj X✝)
⊢ ∀ (Y : ↑(typeToCat.obj X✝)) (f : x ⟶ Y),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
      eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯
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 : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }),
    { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x

Tactic:
intro x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }
⊢ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x
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
t : LimitCone F
j : J
⊢ (isoLimitCone t).hom ≫ t.cone.π.app j = π F j

Tactic:
by
  dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
  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✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).inv ≫ π F j = t.cone.π.app j

Tactic:
by
  dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
  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
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
⊢ G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G

Tactic:
colimit.ι_pre (F ⋙ G) E j,

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
⊢ G.map (ι F (E.obj j)) = ι (F ⋙ G) (E.obj j) ≫ post F G
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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
j : J
⊢ lift f fs w ≫ π arrows j = fs j

Tactic:
by
  simp only [limit.lift_π, WidePullbackShape.mkCone_π_app]

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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
⊢ lift f fs w ≫ base arrows = f

Tactic:
by
  simp only [limit.lift_π, WidePullbackShape.mkCone_π_app]

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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g = lift (g ≫ base arrows) (fun j ↦ g ≫ π arrows j) ⋯

Tactic:
by
  aesop

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
inst✝ : HasWidePushout B objs arrows
j : J
⊢ arrows j ≫ ι arrows j = head arrows

Tactic:
apply colimit.w (WidePushoutShape.wideSpan _ _ _) (WidePushoutShape.Hom.init j)

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
s : Cone (Discrete.functor f)
j : Discrete β
⊢ s.π.app default ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        j =
    s.π.app j

Tactic:
obtain rfl := Subsingleton.elim j default

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
⊢ s.π.app default ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        default =
    s.π.app default
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
l : WalkingPair
⊢ c.π.app { as := l } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := l }

Tactic:
cases l

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := left } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := right } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
l : WalkingPair
⊢ c.ι.app { as := l } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := l }

Tactic:
cases l

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := left } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := right } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := right }
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
s : Cocone (Discrete.functor f)
j : Discrete β
⊢ { pt := f default,
              ι :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.ι.app
        j ≫
      s.ι.app default =
    s.ι.app j

Tactic:
obtain rfl := Subsingleton.elim j default

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
⊢ { pt := f default,
              ι :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.ι.app
        default ≫
      s.ι.app default =
    s.ι.app default
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
h : f = g
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
by
  subst h
  rfl

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
P : Over X → Prop
⊢ (∀ (Y : Over X), P Y) ↔ ∀ (Y : T) (f : Y ⟶ X), P (mk f)

Tactic:
by
  aesop

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Under X
h : f = g
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
by
  subst h
  rfl

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
P : Under X → Prop
⊢ (∀ (Y : Under X), P Y) ↔ ∀ (Y : T) (f : X ⟶ Y), P (mk f)

Tactic:
by
  aesop

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
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
X : CostructuredArrow S T
⊢ U.map (e₁.app X.left).hom ≫ ((map₂ α' β').obj X).hom = ((map₂ α (e₂.hom.app T ≫ β')).obj X).hom

Tactic:
simp [← reassoc_of% dsimp% congr($(hα).app X.left)]

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
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift F'.ofCompIso ≫ F'.m = ((Image.monoFactorisation f).compMono g).m

Tactic:
rw [← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m),
            ← IsIso.inv_hom_id g, ← Category.assoc]
          refine congrArg (· ≫ g) ?_
          have : (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
            image.lift (MonoFactorisation.ofCompIso F') ≫
            ((MonoFactorisation.ofCompIso F').m) := by
              simp only [Category.assoc,
                MonoFactorisation.ofCompIso_m]
          rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
X : C
⊢ NatTrans.app 0 X ≫ η.app X = NatTrans.app 0 X

Tactic:
apply zero_comp

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

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

Tactic:
by
    change ((default : X ⟶ 0) ≫ default) ≫ f = (default : X ⟶ 0) ≫ default
    rw [Category.assoc]
    congr
    simp only [eq_iff_true_of_subsingleton]

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

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map (0 ≫ F.preimage 0) = 0

Tactic:
by rw [F.map_comp, F.map_preimage, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F₁ F₂ : C ⥤ D
inst✝ : F₁.PreservesZeroMorphisms
e : F₁ ≅ F₂
X Y : C
⊢ F₂.map 0 = 0

Tactic:
by simp only [← cancel_epi (e.hom.app X), ← e.hom.naturality,
    F₁.map_zero, zero_comp, comp_zero]

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
⊢ (h ≫ f) ≫ c.π = (h ≫ g) ≫ c.π

Tactic:
by
      simp only [Category.assoc]
      exact congrArg (h ≫ ·) c.condition

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toRightCancelMonoid M)

Tactic:
intro m₁ m₂ h
  apply CancelMonoid.ext
  exact congrArg (fun m : Monoid M => (letI := m; HMul.hMul : M → M → M)) <|
    congrArg (@RightCancelMonoid.toMonoid M) h

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 Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel g
w : f ≫ g = 0
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
inst✝ : HasKernel g'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ lift g f w ≫ map g g' q r h₂ = p ≫ lift g' f' w'

Tactic:
by
  ext; simp [h₁]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBiproducts F
J : Type
x✝ : Finite J
⊢ PreservesBiproductsOfShape J F

Tactic:
by let := preservesBiproducts_shrink.{0} F; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
j : J
⊢ lift g ≫ π f j = (∑ j, g j ≫ ι f j) ≫ π f j

Tactic:
simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]

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✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
j : J
⊢ ι f j ≫ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π =
    ι f j ≫ s.π

Tactic:
rw [CokernelCofork.π_ofπ, biproduct.toSubtype_fromSubtype_assoc, biproduct.ι_map_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 : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
j : J
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
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
Z : C
f g : Z ⟶ X ⊞ Y
⊢ f = g ↔ f ≫ fst = g ≫ fst ∧ f ≫ snd = g ≫ snd

Tactic:
by
  aesop

Goal state after:
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
Z : C
f g : X ⊞ Y ⟶ Z
⊢ f = g ↔ inl ≫ f = inl ≫ g ∧ inr ≫ f = inr ≫ g

Tactic:
by
  aesop

Goal state after: