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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
congr

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ map✝¹ = map✝
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
⊢ F.map f ≫ F.map g ≍ G.map f ≫ G.map g

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : F.map f ≍ G.map f
⊢ H.map (F.map f) ≍ H.map (G.map f)

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
inst✝ : IsIso α
⊢ whiskerRight (inv α) F = inv (whiskerRight α F)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
inst✝ : IsIso α
⊢ whiskerRight (inv α) F ≫ whiskerRight α F = 𝟙 (H ⋙ F)
Module: Mathlib.CategoryTheory.Whiskering

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
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
inst✝ : IsIso α
⊢ F.whiskerLeft (inv α) = inv (F.whiskerLeft α)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Goal state after:
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 : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
inst✝ : IsIso α
⊢ F.whiskerLeft (inv α) ≫ F.whiskerLeft α = 𝟙 (F ⋙ H)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: 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'

Tactic:
simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h

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

Goal state before:
pp: case mk.mk
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
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ { lift := lift✝¹, fac := fac✝¹, uniq := uniq✝¹ } = { lift := lift✝, fac := fac✝, uniq := uniq✝ }

Tactic:
congr

Goal state after:
case mk.mk
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
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ lift✝¹ = lift✝
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
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ h.lift { pt := W, π := { app := fun b ↦ f ≫ t.π.app b, naturality := ⋯ } } =
    h.lift { pt := W, π := { app := fun b ↦ f' ≫ t.π.app b, naturality := ⋯ } }

Tactic:
congr

Goal state after:
case e_8
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b ↦ f ≫ t.π.app b) = fun b ↦ f' ≫ t.π.app b
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 : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)

Tactic:
rw [← adj.homEquiv_unit, ← (adj.homEquiv _ _).eq_symm_apply, adj.homEquiv_counit]

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 : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.counit.app Y = F.map (𝟙 (G.obj Y)) ≫ adj.counit.app Y
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 : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ (adj.homEquiv X Y).symm f =
    F.map f ≫ { app := fun Y ↦ (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y)), naturality := ⋯ }.app Y

Tactic:
simp [← adj.homEquiv_naturality_left_symm]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ (adj.homEquiv X Y).symm f =
    F.map f ≫ { app := fun Y ↦ (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y)), naturality := ⋯ }.app Y

Tactic:
by simp [← adj.homEquiv_naturality_left_symm]

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
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ { pt := { pt := s_pt, π := s_π }.pt, π := h.homEquiv (h.homEquiv.symm { pt := s_pt, π := s_π }.π) } =
    { pt := s_pt, π := s_π }

Tactic:
congr

Goal state after:
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
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.homEquiv (h.homEquiv.symm { pt := s_pt, π := s_π }.π) = s_π
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
Y : C
f : Y ⟶ X
⊢ { pt := Y, π := h.homEquiv f } = { pt := Y, π := (const J).map f ≫ h.homEquiv (𝟙 X) }

Tactic:
congr

Goal state after:
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
Y : C
f : Y ⟶ X
⊢ h.homEquiv f = (const J).map f ≫ h.homEquiv (𝟙 X)
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
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ homOfCone h (coneOfHom h m) = homOfCone h s

Tactic:
congr

Goal state after:
case e_8
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
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ coneOfHom h m = s
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ { pt := { pt := s_pt, ι := s_ι }.pt, ι := h.homEquiv (h.homEquiv.symm { pt := s_pt, ι := s_ι }.ι) } =
    { pt := s_pt, ι := s_ι }

Tactic:
congr

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ h.homEquiv (h.homEquiv.symm { pt := s_pt, ι := s_ι }.ι) = s_ι
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ { pt := Y, ι := h.homEquiv f } = { pt := Y, ι := h.homEquiv (𝟙 X) ≫ (const J).map f }

Tactic:
congr

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ h.homEquiv f = h.homEquiv (𝟙 X) ≫ (const J).map f
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ homOfCocone h (coconeOfHom h m) = homOfCocone h s

Tactic:
congr

Goal state after:
case e_8
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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ coconeOfHom h m = s
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                uliftFunctor.{u₁, max v₁ w}).map
          f

Tactic:
intros Y Z f
      ext F g
      rw [← ULift.down_inj]
      simpa using (uliftYonedaEquiv_naturality _ _).symm

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

Goal state before:
pp: 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 ⋯

Tactic:
y

Goal state after:
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 ⋯
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: case mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), hom✝¹ ≫ c'.π.app j = c.π.app j
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), hom✝ ≫ c'.π.app j = c.π.app j
w : { hom := hom✝¹, w := w✝¹ }.hom = { hom := hom✝, w := w✝ }.hom
⊢ { hom := hom✝¹, w := w✝¹ } = { hom := hom✝, w := w✝ }

Tactic:
congr

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

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePullbackShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
by
    cases f
    · exact g
    cases g
    apply Hom.term _

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Z✝ : WidePushoutShape J
g : X✝ ⟶ Z✝
⊢ Hom.rec (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → 𝟙 X✝ ≫ g ≍ x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
      (fun X h ↦
        Eq.rec (motive := fun x x_1 ↦
          Z✝ = x → 𝟙 X✝ ≫ g ≍ 𝟙 x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun h ↦
            Eq.rec (motive := fun x x_1 ↦
              (f : X✝ ⟶ x) → f ≍ 𝟙 X✝ → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ objs val) X✝)) ⋯ (𝟙 X✝ ≫ g))
          h)
      (fun j h ↦
        Eq.rec (motive := fun x x_1 ↦
          (f : x ⟶ Z✝) →
            Z✝ = some j → f ≍ Hom.init j → (Option.rec B (fun val ↦ objs val) x ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun f h ↦
            Eq.rec (motive := fun x x_1 ↦ (f : none ⟶ x) → f ≍ Hom.init j → (B ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ (𝟙 X✝ ≫ g))
      (𝟙 X✝ ≫ g) ⋯ ⋯ ⋯ =
    Hom.rec (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → g ≍ x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
      (fun X h ↦
        Eq.rec (motive := fun x x_1 ↦
          Z✝ = x → g ≍ 𝟙 x → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun h ↦
            Eq.rec (motive := fun x x_1 ↦
              (f : X✝ ⟶ x) → f ≍ 𝟙 X✝ → (Option.rec B (fun val ↦ objs val) X✝ ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ objs val) X✝)) ⋯ g)
          h)
      (fun j h ↦
        Eq.rec (motive := fun x x_1 ↦
          (f : x ⟶ Z✝) →
            Z✝ = some j → f ≍ Hom.init j → (Option.rec B (fun val ↦ objs val) x ⟶ Option.rec B (fun val ↦ objs val) Z✝))
          (fun f h ↦
            Eq.rec (motive := fun x x_1 ↦ (f : none ⟶ x) → f ≍ Hom.init j → (B ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ g)
      g ⋯ ⋯ ⋯

Tactic:
congr

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

Goal state before:
pp: case init.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j✝ : J
⊢ Hom.rec (motive := fun a a_1 x ↦ none = a → some j✝ = a_1 → Hom.init j✝ ≫ 𝟙 (some j✝) ≍ x → (B ⟶ objs j✝))
      (fun X h ↦
        Eq.rec (motive := fun x x_1 ↦ some j✝ = x → Hom.init j✝ ≫ 𝟙 (some j✝) ≍ 𝟙 x → (B ⟶ objs j✝))
          (fun h ↦
            Eq.rec (motive := fun x x_1 ↦ (f : none ⟶ x) → f ≍ 𝟙 none → (B ⟶ Option.rec B (fun val ↦ objs val) x))
              (fun f h ↦ 𝟙 B) ⋯ (Hom.init j✝ ≫ 𝟙 (some j✝)))
          h)
      (fun j h h_1 ↦
        Eq.rec (motive := fun x x_1 ↦ (f : none ⟶ x) → f ≍ Hom.init j → (B ⟶ Option.rec B (fun val ↦ objs val) x))
          (fun f h ↦ arrows j) ⋯ (Hom.init j✝ ≫ 𝟙 (some j✝)))
      (Hom.init j✝ ≫ 𝟙 (some j✝)) ⋯ ⋯ ⋯ =
    arrows j✝

Tactic:
congr

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

Goal state before:
pp: case none
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
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app none =
    (WidePullbackShape.mkCone f fs w).π.app none

Tactic:
apply h2

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

Goal state before:
pp: case none
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
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none

Tactic:
apply h2

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

Goal state before:
pp: case none
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
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app none ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app none

Tactic:
apply h2

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

Goal state before:
pp: case none
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
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g2

Tactic:
apply h2

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
⊢ G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j ↦ G.map (g j)

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

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
x✝ : Discrete β
j : β
⊢ f default = f j

Tactic:
congr

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ default = j
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
x✝ : Discrete β
j : β
⊢ f j = f default

Tactic:
congr

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ j = default
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ i₁ ≫ fst = i₂ ≫ fst

Tactic:
rw [← cancel_mono f]

Goal state after:
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ (i₁ ≫ fst) ≫ f = (i₂ ≫ fst) ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

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
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
have w := t.π.naturality WalkingCospan.Hom.inl

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w :
  ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ t.π.app WalkingCospan.one = t.fst ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl

Tactic:
congr

Goal state after:
case e_a
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app WalkingCospan.left = s.π.app WalkingCospan.left
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : Hom.left { left := left✝¹, right := b, w := w✝¹ } = Hom.left { left := left✝, right := e, w := w✝ }
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }

Tactic:
congr

Goal state after:
case e_right
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : Hom.left { left := left✝¹, right := b, w := w✝¹ } = Hom.left { left := left✝, right := e, w := w✝ }
⊢ b = e