Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: case e'_2.e'_6
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
e_3✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) =
    obj x₀✝
e_4✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₁✝) =
    obj x₁✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝)) =
    map e₀₁✝

pp: case e'_2.e'_7
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
e_4✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₁✝) =
    obj x₁✝
e_5✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝) =
    obj x₂✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₁₂✝)) =
    map e₁₂✝

pp: case e'_3
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝)) =
    map e₀₂✝

Tactic:
<;>

Goal state after:
case e'_2.e'_6
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
e_3✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) =
    obj x₀✝
e_4✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₁✝) =
    obj x₁✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝)) =
    map e₀₁✝

case e'_2.e'_7
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
e_4✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₁✝) =
    obj x₁✝
e_5✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝) =
    obj x₂✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₁₂✝)) =
    map e₁₂✝

case e'_3
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝)) =
    map e₀₂✝