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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2 → IsIso f

Tactic:
rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
    dsimp at hfg₁ hgf₁ hfg₂ hgf₂
    refine ⟨⟨(g₁, g₂), by aesop_cat, by aesop_cat⟩⟩

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' ↔ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
by
  constructor
  · intro h
    refine ⟨congr_arg Arrow.left h, congr_arg Arrow.right h, ?_⟩
    simpa [eqToHom_left, eqToHom_right] using! iso_w (eqToIso h.symm)
  · rintro ⟨rfl, rfl, h⟩
    simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h
    rw [h]

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
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m = P.liftConeMorphism s ≫ i.hom

Tactic:
← i.comp_inv_eq

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
F : J ⥤ C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m ≫ i.inv = P.liftConeMorphism s
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
X : Cᵒᵖ
x : (yoneda.obj Z).obj X
⊢ (ConcreteCategory.hom ((yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z))))).app X)).toFun x =
    (ConcreteCategory.hom (f.app X)).toFun x

Tactic:
have := f.naturality_apply x.op (𝟙 Z)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
X : Cᵒᵖ
x : (yoneda.obj Z).obj X
this :
  (ConcreteCategory.hom (f.app (op (unop X)))) ((ConcreteCategory.hom ((yoneda.obj Z).map (Quiver.Hom.op x))) (𝟙 Z)) =
    (ConcreteCategory.hom ((yoneda.obj W).map (Quiver.Hom.op x))) ((ConcreteCategory.hom (f.app (op Z))) (𝟙 Z))
⊢ (ConcreteCategory.hom ((yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z))))).app X)).toFun x =
    (ConcreteCategory.hom (f.app X)).toFun x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
by ext; apply this

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
by ext; apply this

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
f : c ⟶ c'
G : C ⥤ D
j : J
⊢ G.map f.hom ≫ G.map (c'.π.app j) = G.map (c.π.app j)

Tactic:
by
  simp [← map_comp]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
a✝ : HasLiftingProperty i' p
⊢ HasLiftingProperty i p

Tactic:
exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ F.map h.i ≫ F.map h.r = 𝟙 (F.obj X)

Tactic:
← F.map_comp h.i h.r,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ F.map (h.i ≫ h.r) = 𝟙 (F.obj X)
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:
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✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)

Tactic:
by
  have : HasLimit ((D ⋙ E) ⋙ F) := h
  ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; rfl

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
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
j : J
⊢ ((adj.homEquiv s.pt F).symm m).app j = ((adj.homEquiv s.pt F).symm ((adj.homEquiv s.pt F) s.π)).app j

Tactic:
simpa using! hm 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)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt
w :
  ∀ (j : Discrete β),
    m ≫
        { pt := f default,
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => eqToHom ⋯ }.π.app
          j =
      s.π.app j
⊢ m = s.π.app default

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

Tactic:
specialize w 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)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt ⟶
    s.pt
w :
  { pt := f default,
              ι :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.ι.app
        default ≫
      m =
    s.ι.app default
⊢ m = s.ι.app default
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone (pair X Y)
⊢ lift s ≫ (mk fst snd).π.app { as := left } = s.π.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone (pair X Y)
⊢ lift s ≫ (mk fst snd).π.app { as := right } = s.π.app { as := right }

Tactic:
exacts [fac_left s, fac_right s]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone (pair X Y)
⊢ (mk inl inr).ι.app { as := left } ≫ desc s = s.ι.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone (pair X Y)
⊢ (mk inl inr).ι.app { as := right } ≫ desc s = s.ι.app { as := right }

Tactic:
exacts [fac_left s, fac_right s]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.map f g ≫ prod.snd)) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))

Tactic:
prod.map_snd

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)) = prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))
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
⊢ lift (fst f g) (snd f g) ⋯ = 𝟙 (pullback f g)

Tactic:
by
  apply hom_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
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)

Tactic:
by
  apply hom_ext <;> simp

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 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''
⊢ i₂ ≫ g' ≫ j₃ = (i₂ ≫ j₂) ≫ g''

Tactic:
e₄,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ 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''
⊢ i₂ ≫ j₂ ≫ g'' = (i₂ ≫ j₂) ≫ g''
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 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''
⊢ i₁ ≫ g' ≫ j₃ = (i₁ ≫ j₁) ≫ g''

Tactic:
e₄,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ 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''
⊢ i₁ ≫ j₁ ≫ g'' = (i₁ ≫ j₁) ≫ g''
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g

Tactic:
by
  rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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 f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ ι f = (eqToIso h).hom ≫ ι f'

Tactic:
apply image.ext

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ (image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
        pullback.fst h y) ≫
      h =
    y

Tactic:
apply image.ext

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      (image.lift
            { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
              e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
          pullback.fst h y) ≫
        h =
    factorThruImage f ≫ y
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

Tactic:
by apply HasZeroObject.from_zero_ext

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cone.forget F).map ((limit.isLimit F).liftConeMorphism c))

Tactic:
suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by
      apply (Cone.forget F).map_isIso _

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((limit.isLimit F).liftConeMorphism c)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)

Tactic:
apply t.uniq_cocone_morphism

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

Goal state before:
pp: 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✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : j = j' → ¬x ≍ y
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    0

Tactic:
by_cases w : j = j'

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✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : j = j' → ¬x ≍ y
w : j = j'
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    0

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✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : j = j' → ¬x ≍ y
w : ¬j = j'
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    0
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ ∑ j, (F.mapBicone b✝).π j ≫ (F.mapBicone b✝).ι j = 𝟙 (F.mapBicone b✝).pt

Tactic:
simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ ∑ x, F.map (b✝.π x ≫ b✝.ι x) = 𝟙 (F.mapBicone b✝).pt
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
A : BinaryBicone P Q
⊢ F.map A.inl ≫ F.map A.fst = 𝟙 (F.obj P)

Tactic:
rw [← F.map_comp, A.inl_fst, F.map_id]

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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
j✝ : K
⊢ (lift x ≫ matrix m) ≫ π g j✝ = (lift fun k ↦ ∑ j, x j ≫ m j k) ≫ π g j✝

Tactic:
simp [biproduct.lift_desc]

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

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
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)

Tactic:
by
    apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]
    apply hY.eq_of_tgt

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a ∈ antidiagonal n, f ∈ map { toFun := Fin.cons a.1, inj' := ⋯ } ↑(aux d a.2)) ↔ ∑ i, f i = n

Tactic:
mem_antidiagonal,

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a, a.1 + a.2 = n ∧ f ∈ map { toFun := Fin.cons a.1, inj' := ⋯ } ↑(aux d a.2)) ↔ ∑ i, f i = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j

Tactic:
exact sizeUpTo_index_le _ _

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

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]; exact BijOn.iterate

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

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n)) s s

Tactic:
by
  simp_rw [Equiv.Perm.coe_pow]; exact BijOn.iterate

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

Goal state before:
pp: α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
⊢ f x = 1 x

Tactic:
rcases h x with hx | hx

Goal state after:
case inl
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : f x = x
⊢ f x = 1 x

case inr
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : f x = x
⊢ f x = 1 x