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

Goal state before:
pp: case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2

pp: case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (y✝, x✝).1 (y✝, x✝).2

pp: case swap.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (y✝¹, x✝¹).1 (y✝¹, x✝¹).2 (x✝, y✝).1 (x✝, y✝).2

pp: case swap.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ ↑f (x✝¹, y✝¹).1 (x✝¹, y✝¹).2 (x✝, y✝).1 (x✝, y✝).2 = ↑f (y✝¹, x✝¹).1 (y✝¹, x✝¹).2 (y✝, x✝).1 (y✝, x✝).2

Tactic:
exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = ∅
x y : α
⊢ r x y ↔ ⊥ x y

Tactic:
simpa [h] using fromRel_prop (sym := sym)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = Set.univ
x y : α
⊢ r x y ↔ ⊤ x y

Tactic:
simpa [h] using fromRel_prop (sym := sym)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
⊢ #z.toFinset = if z.IsDiag then 1 else 2

Tactic:
simp [card_toFinset_of_not_isDiag z h, h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
⊢ Nonempty F.FullyFaithful

Tactic:
by
    have : F.Faithful := ⟨fun h ↦ (hF _ _).injective h⟩
    have : F.Full := ⟨(hF _ _).surjective⟩
    exact ⟨.ofFullyFaithful _⟩

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

Goal state before:
pp: C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
FC : C✝ → C✝ → Type u_1
CC : C✝ → Type w
inst✝⁴ : (X Y : C✝) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C✝ FC
C : Type u
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
f : C → D
X✝ Y✝ : InducedCategory D f
x✝ : X✝ ⟶ Y✝
⊢ homMk (ofHom (hom x✝.hom)) = x✝

Tactic:
by ext; simp [ofHom_hom]

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

Goal state before:
pp: C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁴ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝³ : ConcreteCategory C✝ FC✝
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
P : ObjectProperty C
X✝ Y✝ : P.FullSubcategory
x✝ : X✝ ⟶ Y✝
⊢ homMk (ofHom (hom x✝.hom)) = x✝

Tactic:
by ext; simp [ofHom_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
      (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X) =
    𝟙 (e.functor.unop.obj X)

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ (e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
        (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X)).op =
    (𝟙 (e.functor.unop.obj X)).op
Module: Mathlib.CategoryTheory.Comma.Arrow

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

Tactic:
rintro ⟨rfl, rfl, h⟩

Goal state after:
case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯
⊢ mk f = mk f'
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f g

Tactic:
rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ P (f ≫ e)

Tactic:
refine hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf
    simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx1 : f0x1 ≫ fx11 = fx01 ≫ f1x1
inst✝ : Mono f11x
⊢ f0x0 ≫ fx10 = fx00 ≫ f1x0

Tactic:
← cancel_mono f11x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx1 : f0x1 ≫ fx11 = fx01 ≫ f1x1
inst✝ : Mono f11x
⊢ (f0x0 ≫ fx10) ≫ f11x = (fx00 ≫ f1x0) ≫ f11x
Module: Mathlib.Algebra.Category.Grp.Basic

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

Tactic:
let i := asIso ((forget GrpCat).map f)

Goal state after:
X Y : GrpCat
f : X ⟶ Y
x✝ : IsIso ((forget GrpCat).map f)
i : (forget GrpCat).obj X ≅ (forget GrpCat).obj Y := asIso ((forget GrpCat).map f)
⊢ IsIso f
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
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj.counit.app X) = (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj'.counit.app X)

Tactic:
Adjunction.homEquiv_unit,

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
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj'.counit.app X)
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
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj'.counit.app X)

Tactic:
Adjunction.homEquiv_unit,

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
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
Module: Mathlib.CategoryTheory.Limits.IsLimit

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

Tactic:
apply G.map_comp

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.cones.RepresentableBy X
s : Cone F
⊢ coneOfHom h (homOfCone h s) = s

Tactic:
dsimp [coneOfHom, homOfCone]
  match s with
  | .mk s_pt s_π =>
    congr
    exact h.homEquiv.apply_symm_apply s_π

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom

Tactic:
by
  rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
      rightUnitor_comp, rightUnitor_naturality]

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:
by rw [← F.map_comp h.i h.r, h.retract, F.map_id]

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

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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ (unop X).unop.ι.app j ≫ f.unop.hom.unop = (unop Y).unop.ι.app j

Tactic:
apply Quiver.Hom.op_inj

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 : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ ((unop X).unop.ι.app j ≫ f.unop.hom.unop).op = ((unop Y).unop.ι.app j).op
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:
erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j

Tactic:
dsimp
      intro j
      rw [← w]
      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
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ ∀ (j : J), t.ι.app j ≫ m.unop = s.unop.ι.app j

Tactic:
dsimp
      intro j
      rw [← w]
      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
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = s.op.π.app j

Tactic:
dsimp
      intro j
      rw [← w]
      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
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = s.op.ι.app j

Tactic:
dsimp
      intro j
      rw [← w]
      rfl

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
f g : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono ((Discrete.natTrans fun X ↦ p X.as).app j)

Tactic:
by dsimp; infer_instance

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
f g : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi ((Discrete.natTrans fun X ↦ p X.as).app j)

Tactic:
by dsimp; infer_instance

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

Goal state before:
pp: β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b ↦ G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b ↦ G.obj (f b)) j =
    (Pi.lift fun j ↦ G.map (g j)) ≫ Pi.π (fun b ↦ G.obj (f b)) j

Tactic:
simp only [Category.assoc, piComparison_comp_π, ← G.map_comp,
    limit.lift_π, Fan.mk_π_app]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
⊢ g = h

Tactic:
by
    rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl

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
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ i.hom ≫ t.ι = t.ι

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ t.ι = t.ι
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
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫ ((𝟭 C).mapCone c).π.app j = s.π.app j

Tactic:
cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j

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
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone initialIsInitial
  apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

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✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    ((𝟭 C).mapCocone c).ι.app j ≫ h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } = s.ι.app j

Tactic:
cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j

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✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫ c.π.app j = s.π.app j

Tactic:
cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j

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✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (j : J),
    c.ι.app j ≫ h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } = s.ι.app j

Tactic:
cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j' (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
        if h : some j' = j then ⋯.mpr {Hom.id j} else ∅

Tactic:
by
    rintro (_ | _)
    · cases j <;> simp
    · simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j (Option.casesOn j' {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
        if h : some j = j' then ⋯.mpr {Hom.id j'} else ∅

Tactic:
by
    rintro (_ | _)
    · cases j <;> simp
    · simp

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
⊢ kernelZeroIsoSource.inv = kernel.lift 0 (𝟙 X) ⋯

Tactic:
by
  ext
  simp [kernelZeroIsoSource]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j ↦ G.obj (f j)
i : IsIso (piComparison G f)
⊢ PreservesLimit (Discrete.functor f) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (productIsProduct f)
  apply (isLimitMapConeFanMkEquiv _ _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _
    (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j ↦ G.obj (f j)
i : IsIso (piComparison G f)
⊢ PreservesLimit (Discrete.functor f) G

Tactic:
by
  apply preservesLimit_of_preserves_limit_cone (productIsProduct f)
  apply (isLimitMapConeFanMkEquiv _ _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _
    (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

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

Tactic:
A.inr_snd,

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
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
A : BinaryBicone P Q
⊢ F.map (𝟙 Q) = 𝟙 (F.obj Q)
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 : Fork (π f i) 0
⊢ (s.ι ≫ toSubtype f fun j ↦ j ≠ i) ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι

Tactic:
apply biproduct.hom_ext; intro j
      rw [KernelFork.ι_ofι, Category.assoc, Category.assoc,
        biproduct.toSubtype_fromSubtype_assoc, biproduct.map_π]
      rcases Classical.em (i = j) with (rfl | h)
      · rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
      · rw [if_pos (Ne.symm h), Category.comp_id]

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
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.fst = BinaryCofan.IsColimit.desc ht (𝟙 X) 0

Tactic:
apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)
  rintro ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _

Goal state after:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : inv inl ≫ inl ≫ fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono (map f g)

Tactic:
by
  rw [show biprod.map f g = (biprod.isoProd _ _).hom ≫ prod.map f g ≫
    (biprod.isoProd _ _).inv by aesop]
  infer_instance

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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ ι f j ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv ≫ b.toCone.π.app j' =
    (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp,

Goal state after:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ ι f j ≫ (bicone f).toCone.π.app j' = (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'