-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
lemma toNerve₂.mk_naturality_δ1i (i : Fin 3) : toNerve₂.mk.naturalityProperty F (δ₂ i)

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
i : Fin 3
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (δ₂ i ⋯ ⋯).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    ((nerveFunctor ⋙
              (whiskeringLeft (SimplexCategory.Truncated 2)ᵒᵖ SimplexCategoryᵒᵖ (Type u)).obj (inclusion 2).op).obj
          (Cat.of C)).map
      (δ₂ i ⋯ ⋯).op (mk.app F { obj := [1 + 1], property := ⋯ } x)

Tactic:
simp only [comp_obj, nerveFunctor_obj, Cat.of_α, whiskeringLeft_obj_obj, id_eq, op_obj,
  nerve_obj, oneTruncation₂_obj, ReflQuiv.of_val, Nat.reduceAdd, mk.app_two,
  Functor.comp_map, op_map, Quiver.Hom.unop_op]

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
i : Fin 3
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (δ₂ i ⋯ ⋯).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map ((inclusion 2).map (δ₂ i ⋯ ⋯)).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

Proof state:
case h.«0»
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (δ ((fun i => i) ⟨0, ⋯⟩)).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map (δ ((fun i => i) ⟨0, ⋯⟩)).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

Tactic:
simp only [Fin.zero_eta]

Result:
case h.«0»
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (δ 0).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map (δ 0).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

Proof state:
case h.«0».hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 1 ≫ δ 0).op x = X.map (δ 0 ≫ δ 2).op x

Tactic:
have := δ_comp_δ (n := 0) (i := 0) (j := 1) (by decide)

Result:
case h.«0».hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
this : δ 0 ≫ δ (Fin.succ 1) = δ 1 ≫ δ (Fin.castSucc 0)
⊢ X.map (δ 1 ≫ δ 0).op x = X.map (δ 0 ≫ δ 2).op x

Proof state:
case h.«0».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
this : δ 0 ≫ δ (Fin.succ 0) = δ 0 ≫ δ (Fin.castSucc 0)
⊢ X.map (δ 0 ≫ δ 0).op x = X.map (δ 0 ≫ δ 1).op x

Tactic:
dsimp at this

Result:
case h.«0».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
this : δ 0 ≫ δ 1 = δ 0 ≫ δ 0
⊢ X.map (δ 0 ≫ δ 0).op x = X.map (δ 0 ≫ δ 1).op x

Proof state:
case h.«1».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 0).op (X.map (δ 1).op x) = X.map (δ 0 ≫ δ 1).op x

Tactic:
simp [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
no goals

Proof state:
case h.«2».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 0).op (X.map (δ 2).op x) = ev1₂ x

Tactic:
unfold ev1₂ ι1₂ δ₂

Result:
case h.«2».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 0).op (X.map (δ 2).op x) = X.map (δ 0 ≫ δ 2).op x

Proof state:
case h.«0».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 0 ≫ δ 0).op x = X.map (δ 0 ≫ δ 1).op x

Tactic:
have := δ_comp_δ (n := 0) (i := 0) (j := 0) (by decide)

Result:
case h.«0».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
this : δ 0 ≫ δ (Fin.succ 0) = δ 0 ≫ δ (Fin.castSucc 0)
⊢ X.map (δ 0 ≫ δ 0).op x = X.map (δ 0 ≫ δ 1).op x

Proof state:
case h.«1».hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 1).op (X.map (δ 1).op x) = X.map (δ 1 ≫ δ 1).op x

Tactic:
simp [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
no goals

Proof state:
case h.«0».hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
this : δ 0 ≫ δ 1 = δ 0 ≫ δ 0
⊢ X.map (δ 0 ≫ δ 0).op x = X.map (δ 0 ≫ δ 1).op x

Tactic:
exact congrFun (congrArg X.map (congrArg Quiver.Hom.op this.symm)) x

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
i : Fin 3
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (δ i).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map ((fullSubcategoryInclusion fun a => a.len ≤ 2).map (δ i)).op
      (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

Tactic:
simp only [fullSubcategoryInclusion.map]

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
i : Fin 3
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (δ i).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map (δ i).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))