mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr

Tactic:
dif_neg h'.symm,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ eqToHom ⋯ ≫ s.inr = s.inr
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : Rel' f g (Sum.inr ((ConcreteCategory.hom g) s)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)

Tactic:
replace hyz := hyz.symm

Goal state after:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : Rel' f g (Sum.inl z₁) (Sum.inr ((ConcreteCategory.hom g) s))
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩) =
    ⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩

pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y

Tactic:
· rw [Subtype.ext_iff]
      exact congr($(c.ι_t_ι_eq_ι_l_b_ι).app _ ⟨y, _⟩)

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ f.vertex j = g.vertex j

Tactic:
simp only [hl, ← Fin.succ_last]
      rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i ≫ δ 0).op)) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i.succ).op)) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η ((eId Cat b).toFunctor.map (𝟙 { down := { as := () } })) ≍ η

Tactic:
exact congr_arg_heq (·.toFunctor.map η) (e_comp_id (V := Cat) a b)

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

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = hComp (eqToIso ⋯).hom (𝟙 g)

Tactic:
generalize_proofs h1 h2 h3

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h1 : (f ≫ 𝟙 b✝) ≫ g = f ≫ 𝟙 b✝ ≫ g
h2 : 𝟙 b✝ ≫ g = g
h3 : f ≫ 𝟙 b✝ = f
⊢ (eqToIso h1).hom ≫ hComp (𝟙 f) (eqToIso h2).hom = hComp (eqToIso h3).hom (𝟙 g)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      (𝟙 (𝟙_ V) ▷ X'' ⟶[V] Y) ≫
        (((eHomEquiv V) f' ≫ (λ_ (X' ⟶[V] X'')).inv) ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (X ⟶[V] X') ◁ eComp V X' X'' Y ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y

Tactic:
id_whiskerRight_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      (((eHomEquiv V) f' ≫ (λ_ (X' ⟶[V] X'')).inv) ▷ X'' ⟶[V] Y) ≫
        (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
          (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (X ⟶[V] X') ◁ eComp V X' X'' Y ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ ((λ_ (𝟙_ V)).inv ≫ ((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫ eComp V Y Y' Y'') ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫ eComp V Y Y' Y'') ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫ eComp V Y Y' Y'') ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ ((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫ (X ⟶[V] Y) ◁ eComp V Y Y' Y'' ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ ((ρ_ (𝟙_ V)).hom ≫ (eHomEquiv V) g ≫ (ρ_ (Y ⟶[V] Y')).inv ≫ (Y ⟶[V] Y') ◁ (eHomEquiv V) g') ≫
          (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (ρ_ (𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ ((eHomEquiv V) g ≫ (ρ_ (Y ⟶[V] Y')).inv ≫ (Y ⟶[V] Y') ◁ (eHomEquiv V) g') ≫
            (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (ρ_ (𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ ((eHomEquiv V) g ≫ (ρ_ (Y ⟶[V] Y')).inv ≫ (Y ⟶[V] Y') ◁ (eHomEquiv V) g') ≫
            (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (ρ_ (𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Y')).inv ≫ (Y ⟶[V] Y') ◁ (eHomEquiv V) g') ≫
              (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (ρ_ (𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Y')).inv ≫ (Y ⟶[V] Y') ◁ (eHomEquiv V) g') ≫
              (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (ρ_ (𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (X ⟶[V] Y) ◁ (ρ_ (Y ⟶[V] Y')).inv ≫
              (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Functor.FunctorHom

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 : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
⊢ (fun f ↦ { app := fun x ↦ ↾fun x_1 ↦ HomObj.ofNatTrans f, naturality := ⋯ })
      ((fun f ↦
          { app := fun X ↦ ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))),
            naturality := ⋯ })
        f) =
    f

Tactic:
ext X a Y φ
    have := HomObj.congr_app (ConcreteCategory.congr_hom (f.naturality φ) PUnit.unit) Y (𝟙 Y)
    dsimp [functorHom, homObjFunctor] at this
    aesop

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = eId V X

Tactic:
by
    change _ = eId V X.obj
    rw [← eHomEquiv_id]
    rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
w✝¹ : SimplexCategoryGenRel
w✝ : z ⟶ w✝¹
m₁ : w✝¹ ⟶ mk n
he₁ : P_σ w✝
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w✝ ≫ m₁
⊢ (e ≫ f ≫ δ i) ≫ σ j = (e ≫ w✝) ≫ m₁ ≫ δ j''

Tactic:
by simp [← reassoc_of% h₁, h']

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L : List ℕ
⊢ Monotone (simplicialEvalσ L)

Tactic:
induction L <;> grind [Monotone]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i✝ : Fin (x₁.len + 1)
h : Fin.castAdd (x₂.len + 1) i✝ ≤ j
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      j

Tactic:
cases j using Fin.addCases

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : Fin.castAdd (x₂.len + 1) i✝¹ ≤ Fin.castAdd (x₂.len + 1) i✝
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝¹) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝)

case left.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₁.len + 1)
i✝ : Fin (x₂.len + 1)
h : Fin.castAdd (x₂.len + 1) i✝¹ ≤ Fin.natAdd (x₁.len + 1) i✝
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝¹) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.natAdd (x₁.len + 1) i✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i✝ : Fin (x₂.len + 1)
h : Fin.natAdd (x₁.len + 1) i✝ ≤ j
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.natAdd (x₁.len + 1) i✝) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      j

Tactic:
cases j using Fin.addCases

Goal state after:
case right.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₂.len + 1)
i✝ : Fin (x₁.len + 1)
h : Fin.natAdd (x₁.len + 1) i✝¹ ≤ Fin.castAdd (x₂.len + 1) i✝
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.natAdd (x₁.len + 1) i✝¹) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.castAdd (x₂.len + 1) i✝)

case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : Fin.natAdd (x₁.len + 1) i✝¹ ≤ Fin.natAdd (x₁.len + 1) i✝
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.natAdd (x₁.len + 1) i✝¹) ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      (Fin.natAdd (x₁.len + 1) i✝)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.left
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ i.predAbove x.succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : x ∈ P.I ∪ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
Set.mem_union

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : x ∈ P.I ∨ x ∈ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ ⋯.index hd = ⋯.index hd

Tactic:
rw [← (P.isUniquelyCodimOneFace x).index_of_iso e.symm hd]
  congr
  rw [P.ofIso_p e hA x]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
p : ℕ
⊢ hom H p (p + 1) = -∑ k, (-1) ^ ↑k • H.h k

Tactic:
by
  simp [hom]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • X.δ x_1 ≫ H.h x + -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • H.h x_1 ≫ Y.δ x +
      H.h 0 ≫ Y.δ 0

Tactic:
have h₂ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2) :
      α x = -β ⟨x.2.succ, x.1.castSucc⟩ := by
    dsimp [α, β]
    simp only [← H.h_castSucc_comp_δ_succ_of_lt x.2 x.1 hx,
      pow_add, pow_one, mul_neg, mul_one, neg_mul, neg_smul, neg_neg]
    rw [mul_comm]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • X.δ x_1 ≫ H.h x + -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • H.h x_1 ≫ Y.δ x +
      H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x, α x + -∑ x ∈ Finset.univ ×ˢ Finset.univ, β x + H.h 0 ≫ Y.δ 0

Tactic:
Finset.univ_product_univ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ (stdSimplex.face {c.index}ᶜ).image c.map = (↑c.s).subcomplex

Tactic:
rw [stdSimplex.face_singleton_compl, image_ofSimplex]
  congr 1
  exact (P.isUniquelyCodimOneFace c.s).δ_index rfl

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.obj
f : ↑(h.hom x y)
⊢ ∃ a, h.functor.mapArrow.obj a = { left := h.objEquiv x, right := h.objEquiv y, hom := h.homEquiv f }

Tactic:
exact ⟨Arrow.mk f, rfl⟩

Goal state after: