mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
constructor

Goal state after:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ (∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔
    (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

Tactic:
constructor

Goal state after:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ →
    (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂ →
    (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 0] ∧ stdSimplex.face {0, 2} ≤ Λ[2, 0]

Tactic:
constructor

Goal state after:
case a.left
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 0]

case a.right
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 0]
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: ⊢ innerHornInclusions = ⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι

Tactic:
ext

Goal state after:
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
⊢ innerHornInclusions f✝ ↔ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1] ∧ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
constructor

Goal state after:
case a.left
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1]

case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 2] ∧ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
constructor

Goal state after:
case a.left
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 2]

case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 2]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.inr
X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton d ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
· exact le_trans (le_trans (by rfl) (le_iSup _ x)) le_sup_right

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1) ∧ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)

Tactic:
constructor

Goal state after:
case a.left
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1)

case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₂.simplex
⊢ c₁ = c₂

Tactic:
ext

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₂.simplex
⊢ c₁.simplex = c₂.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (0 + 1) x).interval 1 0 ⋯

Tactic:
ext

Goal state after:
case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ (X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x)).vertex 0 =
    ((X.spine (0 + 1) x).interval 1 0 ⋯).vertex 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case zero
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋0⦌
⊢ spineToSimplex h (X.spine 0 s) = s

Tactic:
simp [spineToSimplex_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Hom.base (hComp (𝟙 (𝟙 a)) η) = Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Hom.base (hComp η (𝟙 (𝟙 b))) = Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ Hom.base (hComp (hComp η θ) κ) = Hom.base (eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯)
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
A A' : C ⥤ Type w
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (f.app Δ')) ((ConcreteCategory.hom (A'.map φ)) a)) =
    x.app Δ ((ConcreteCategory.hom (f.app Δ)) a) ≫ G.map φ

Tactic:
← x.naturality φ (f.app Δ a),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : C ⥤ Type w
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (f.app Δ')) ((ConcreteCategory.hom (A'.map φ)) a)) =
    F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (A.map φ)) ((ConcreteCategory.hom (f.app Δ)) a))
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
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
⊢ x.app = y.app

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
x✝¹ : C
x✝ : (Opposite.unop (coyoneda.rightOp.obj X)).obj x✝¹
⊢ x.app x✝¹ x✝ = y.app x✝¹ x✝
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
A : C ⥤ Type (max u v v')
x : F.HomObj G A
X Y : C
f : X ⟶ Y
⊢ (A.map f ≫ ↾fun a ↦ { app := fun Y_1 f ↦ x.app Y_1 ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ }) =
    (↾fun a ↦ { app := fun Y f ↦ x.app Y ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ }) ≫
      (F.functorHom G).map f

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type (max u v v')
x : F.HomObj G A
X Y : C
f : X ⟶ Y
x✝ : A.obj X
Y✝ : C
f✝ : Y ⟶ Y✝
⊢ ((ConcreteCategory.hom
              (A.map f ≫
                ↾fun a ↦ { app := fun Y_1 f ↦ x.app Y_1 ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ })).toFun
          x✝).app
      Y✝ f✝ =
    ((ConcreteCategory.hom
              ((↾fun a ↦ { app := fun Y f ↦ x.app Y ((ConcreteCategory.hom (A.map f)) a), naturality := ⋯ }) ≫
                (F.functorHom G).map f)).toFun
          x✝).app
      Y✝ f✝
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
⊢ (𝟭 (C ⥤ Type (max w v u))).map f ≫ (functorHomEquiv F H ((tensorLeft F).obj H)).invFun (𝟙 (F ⊗ H)) =
    (functorHomEquiv F G ((tensorLeft F).obj G)).invFun (𝟙 (F ⊗ G)) ≫ (tensorLeft F ⋙ rightAdj F).map f

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝¹ : C
x✝ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝¹
⊢ (ConcreteCategory.hom
          (((𝟭 (C ⥤ Type (max w v u))).map f ≫ (functorHomEquiv F H ((tensorLeft F).obj H)).invFun (𝟙 (F ⊗ H))).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((functorHomEquiv F G ((tensorLeft F).obj G)).invFun (𝟙 (F ⊗ G)) ≫ (tensorLeft F ⋙ rightAdj F).map f).app
            x✝¹)).toFun
      x✝
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝¹ : C
x✝ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝¹
⊢ (ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝¹)) x✝ =
    (ConcreteCategory.hom (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝¹)) x✝

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝⁴ : C
x✝³ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝⁴
x✝² : C
x✝¹ : (coyoneda.obj (Opposite.op x✝⁴)).obj x✝²
x✝ : F.obj x✝²
⊢ (ConcreteCategory.hom
          (((ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝⁴)) x✝³).app x✝²
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((ConcreteCategory.hom (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝⁴))
                x✝³).app
            x✝² x✝¹)).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: x✝² : SSet
x✝¹ : x✝² ⟶ Δ[0]
n : SimplexCategory
x✝ : x✝².obj (Opposite.op n)
⊢ objEquiv ((ConcreteCategory.hom (x✝¹.app (Opposite.op n))).toFun x✝) =
    objEquiv ((ConcreteCategory.hom ((SSet.const (obj₀Equiv.symm 0)).app (Opposite.op n))).toFun x✝)

Tactic:
ext

Goal state after:
x✝³ : SSet
x✝² : x✝³ ⟶ Δ[0]
n : SimplexCategory
x✝¹ : x✝³.obj (Opposite.op n)
x✝ : Fin ((Opposite.unop (Opposite.op n)).len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom (objEquiv ((ConcreteCategory.hom (x✝².app (Opposite.op n))).toFun x✝¹))) x✝) =
    ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv ((ConcreteCategory.hom ((SSet.const (obj₀Equiv.symm 0)).app (Opposite.op n))).toFun x✝¹)))
        x✝)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = { out := β }.out.app X
⊢ α = β

Tactic:
ext

Goal state after:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = { out := β }.out.app X
x✝ : ForgetEnrichment V C
⊢ α.app x✝ = β.app x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m ↔ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

Tactic:
constructor

Goal state after:
case mp
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m → (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

case mpr
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m → (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Center C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ tensorHom f✝ g✝ = whiskerRight f✝ X₂✝ ≫ Y₁✝.whiskerLeft g✝

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Center C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (tensorHom f✝ g✝).f = (whiskerRight f✝ X₂✝ ≫ Y₁✝.whiskerLeft g✝).f
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F G : FreeRefl V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
⊢ (quotientFunctor V ⋙ F).obj = (quotientFunctor V ⋙ G).obj

Tactic:
ext

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F G : FreeRefl V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
x✝ : Paths V
⊢ (quotientFunctor V ⋙ F).obj x✝ = (quotientFunctor V ⋙ G).obj x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
i : Fin n
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)

Tactic:
fin_cases x

Goal state after:
case «0»
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩)) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
i : Fin n
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)

Tactic:
fin_cases x

Goal state after:
case «0»
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩)) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        ((fun i ↦ i)
          ⟨(unop
                ((inclusion 2).op.obj
                  (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                      SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len,
            ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ Truncated.Edge.map (𝟙rq x) f = 𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)

Tactic:
ext

Goal state after:
S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ (Truncated.Edge.map (𝟙rq x) f).edge =
    (𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ morphismPropertyHomMk V f ↔ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f

Tactic:
constructor

Goal state after:
case mp
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ morphismPropertyHomMk V f → (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f

case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f → morphismPropertyHomMk V f
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
x✝¹ x✝ : C₁
g : x✝¹ ⟶ x✝
⊢ X✝.flip₂₃.map g ≫ { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝¹).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } ≫ Y✝.flip₂₃.map g

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
x✝³ x✝² : C₁
g : x✝³ ⟶ x✝²
x✝¹ : C₃
x✝ : C₂
⊢ ((X✝.flip₂₃.map g ≫
              { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝²).app Z).app Y, naturality := ⋯ }, naturality := ⋯ }).app
          x✝¹).app
      x✝ =
    (({ app := fun Y ↦ { app := fun Z ↦ ((f.app x✝³).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } ≫
              Y✝.flip₂₃.map g).app
          x✝¹).app
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: x y : OneTruncation₂ ((truncation 2).obj Δ[0])
x✝ : x ⟶ y
this : Subsingleton (((truncation 2).obj Δ[0]).obj (op { obj := ⦋1⦌, property := ⋯ })) :=
  SSet.instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk._proof_1
⊢ x✝ = ⋯ ▸ ⋯ ▸ 𝟙rq default

Tactic:
ext

Goal state after:
x y : OneTruncation₂ ((truncation 2).obj Δ[0])
x✝ : x ⟶ y
this : Subsingleton (((truncation 2).obj Δ[0]).obj (op { obj := ⦋1⦌, property := ⋯ })) :=
  SSet.instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk._proof_1
⊢ x✝.edge = (⋯ ▸ ⋯ ▸ 𝟙rq default).edge