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

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map
    (e.counitInv.app (e.functor.obj (e.inverse.obj Y)) ≫
      e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

Tactic:
map_comp

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)
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.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫ (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X) =
    𝟙 (e.functor.op.obj X)

Tactic:
apply Quiver.Hom.unop_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.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫
        (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X)).unop =
    (𝟙 (e.functor.op.obj X)).unop
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
hi : Q x✝¹
x✝ : Y✝ ⟶ Z✝
hf : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝¹ ≫ x✝)

Tactic:
rw [sInf_iff] at hf ⊢

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
hi : Q x✝¹
x✝ : Y✝ ⟶ Z✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝¹ ≫ x✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
rw [← sInf_range]

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsLeft Q
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝ ≫ x✝¹)

Tactic:
rw [sInf_iff] at hf ⊢

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝ ≫ x✝¹)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
rw [← sInf_range]

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsRight Q
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
rw [← sInf_range]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsIso
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : Arrow C
f : X ⟶ Y
⊢ F.map (Arrow.Hom.left f) ≫ (Arrow.mk (F.map Y.hom)).hom = (Arrow.mk (F.map X.hom)).hom ≫ F.map (Arrow.Hom.right f)

Tactic:
by simp [← Functor.map_comp]

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

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
⊢ Epi (↾f) → Function.Surjective f

pp: case mpr
X Y : Type u
f : X → Y
⊢ Function.Surjective f → Epi (↾f)

Tactic:
· rintro ⟨H⟩
    refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_
    rw [← Equiv.ulift.{u}.symm.injective.comp_left.eq_iff]
    apply TypeCat.homEquiv.symm.injective
    apply H
    apply ConcreteCategory.hom_ext
    intro x
    simp [dsimp% congrFun hg x]

Goal state after:
case mpr
X Y : Type u
f : X → Y
⊢ Function.Surjective f → Epi (↾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
F G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
⊢ ∀ (Y : D),
    (adj.unit ≫ whiskerRight iso.hom H).app (H.obj Y) ≫ H.map ((H.whiskerLeft iso.inv ≫ adj.counit).app Y) = 𝟙 (H.obj Y)

Tactic:
by simp [← Functor.map_comp]

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 : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ f.hom.op ≫ X.op.π.app j = Y.op.π.app j

Tactic:
apply Quiver.Hom.unop_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 : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ (f.hom.op ≫ X.op.π.app j).unop = (Y.op.π.app j).unop
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct

Tactic:
exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ Unique (x ⟶ y)

Tactic:
let f : x ⟶ y := by
      have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert! h.unit.app x
      have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert! h.unitInv.app y
      exact hx ≫ hy

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ Unique (x ⟶ y)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
j : Discrete WalkingPair
⊢ c.π.app j = e.hom ≫ c'.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := left } = e.hom ≫ c'.π.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := right } = e.hom ≫ c'.π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
j : Discrete WalkingPair
⊢ c.ι.app j ≫ e.hom = c'.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := left } ≫ e.hom = c'.ι.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := right } ≫ e.hom = c'.ι.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✝ : HasProducts C
X : C
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (yoneda.obj X ⋙ (piConst.obj X).rightOp).map x✝ ≫ (Pi.lift id).op = (Pi.lift id).op ≫ (𝟭 Cᵒᵖ).map x✝

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : C
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((yoneda.obj X ⋙ (piConst.obj X).rightOp).map x✝ ≫ (Pi.lift id).op).unop = ((Pi.lift id).op ≫ (𝟭 Cᵒᵖ).map x✝).unop
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✝ : HasProducts C
X : C
x✝ : Type v
⊢ (piConst.obj X).rightOp.map ({ app := fun n ↦ ↾fun i ↦ Pi.π (fun x ↦ X) i, naturality := ⋯ }.app x✝) ≫
      { app := fun Y ↦ (Pi.lift id).op, naturality := ⋯ }.app ((piConst.obj X).rightOp.obj x✝) =
    𝟙 ((piConst.obj X).rightOp.obj x✝)

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : C
x✝ : Type v
⊢ ((piConst.obj X).rightOp.map ({ app := fun n ↦ ↾fun i ↦ Pi.π (fun x ↦ X) i, naturality := ⋯ }.app x✝) ≫
        { app := fun Y ↦ (Pi.lift id).op, naturality := ⋯ }.app ((piConst.obj X).rightOp.obj x✝)).unop =
    (𝟙 ((piConst.obj X).rightOp.obj x✝)).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: 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)
j : Discrete WalkingPair
⊢ lift s ≫ (mk fst snd).π.app j = s.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
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 }

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 }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: 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)
j : Discrete WalkingPair
⊢ (mk inl inr).ι.app j ≫ desc s = s.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
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 }

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 }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : 𝟙 s.pt ≫ s.π.app one = s.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none

Tactic:
simp only [Category.id_comp] at h₁

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none
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✝ Y✝ : StructuredArrow S F
f : X✝ ⟶ Y✝
⊢ (mk (G.map X✝.hom)).hom ≫ (F ⋙ G).map (Hom.right f) = (mk (G.map Y✝.hom)).hom

Tactic:
by simp [← Functor.map_comp]

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

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x✝ : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x✝ = t.ι.app j
⊢ x✝ = homMk (hc.desc ((forget X).mapCocone t)) ⋯

Tactic:
ext
    refine hc.hom_ext (fun j ↦ ?_)
    simp [dsimp% hc.fac ((forget X).mapCocone t) j, ← hm]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
⊢ Mono t.snd

Tactic:
refine ⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩
  rw [← cancel_mono f, Category.assoc, Category.assoc, condition]
  apply reassoc_of% i

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:
rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
val✝ : Z ⟶ (mk (𝟙 X) (𝟙 X) ⋯).pt
eq : (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst) ≫ f = (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd) ≫ f
⊢ val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst = val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g

Tactic:
apply pullback.condition

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
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono m

Tactic:
rw [hm]; infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
f : X ⟶ Y
⊢ IsIso (pushout.inl (h ≫ f) h)

Tactic:
convert!
    (congrArg IsIso
          (show pushout.inl _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp f (𝟙 _) h⟩
              WalkingSpan.left)).mp
      inferInstance

Goal state after:
case e'_4.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
f : X ⟶ Y
⊢ h = h ≫ 𝟙 X

case e'_5.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
f : X ⟶ Y
e_3✝ : Y = (span (h ≫ f) (h ≫ 𝟙 X)).obj WalkingSpan.left
e_4✝ : pushout (h ≫ f) h = colimit (span (h ≫ f) (h ≫ 𝟙 X))
⊢ h = h ≫ 𝟙 X
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
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
x✝¹ x✝ : CostructuredArrow (snd L R) b
f : x✝¹ ⟶ x✝
⊢ (𝟭 (CostructuredArrow (snd L R) b)).map f ≫
      CostructuredArrow.homMk { left := 𝟙 x✝.left.left, right := x✝.hom, w := ⋯ } ⋯ =
    CostructuredArrow.homMk { left := 𝟙 x✝¹.left.left, right := x✝¹.hom, w := ⋯ } ⋯ ≫
      (costructuredArrowSndProj L R b ⋙ costructuredArrowSndInclusion L R b).map f

Tactic:
have := CostructuredArrow.w f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
x✝¹ x✝ : CostructuredArrow (snd L R) b
f : x✝¹ ⟶ x✝
this : (snd L R).map f.left ≫ x✝.hom = x✝¹.hom
⊢ (𝟭 (CostructuredArrow (snd L R) b)).map f ≫
      CostructuredArrow.homMk { left := 𝟙 x✝.left.left, right := x✝.hom, w := ⋯ } ⋯ =
    CostructuredArrow.homMk { left := 𝟙 x✝¹.left.left, right := x✝¹.hom, w := ⋯ } ⋯ ≫
      (costructuredArrowSndProj L R b ⋙ costructuredArrowSndInclusion L R b).map f
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
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ ∀ (j : WalkingParallelPair), k ≫ t.π.app j = s.π.app j

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app zero = s.π.app zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one
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 : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ ∀ (j : WalkingParallelPair), s.ι.app j ≫ k = t.ι.app j

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app zero ≫ k = t.ι.app zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WalkingParallelPair
⊢ x ∈ [zero, one].toFinset

Tactic:
by cases x <;> 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
x : WalkingPair
⊢ x ∈ {WalkingPair.left, WalkingPair.right}

Tactic:
by cases x <;> simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsLimitsOfShape J F

Tactic:
have := reflectsSmallestLimits_of_reflectsLimits F

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsLimitsOfShape J F
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
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      j =
    (Iso.refl
          ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      { as := WalkingPair.left } =
    (Iso.refl
          ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.left }

case right
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
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      { as := WalkingPair.right } =
    (Iso.refl
          ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.right }