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

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).op (X.map (δ 0).op x) = X.map (δ 0 ≫ δ 1).op x

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

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 := ⋯ })
⊢ X.map (δ 0 ≫ δ 0).op x = X.map (δ 0 ≫ δ 1).op x

Proof state:
case h.«2».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 ≫ δ 2).op x = X.map (δ 1 ≫ δ 1).op x

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

Result:
case h.«2».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 : δ 1 ≫ δ (Fin.succ 1) = δ 1 ≫ δ (Fin.castSucc 1)
⊢ X.map (δ 1 ≫ δ 2).op x = X.map (δ 1 ≫ δ 1).op x

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 (δ i).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

Tactic:
fin_cases i

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 (δ ((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)))

case h.«1»
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) ⟨1, ⋯⟩)).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map (δ ((fun i => i) ⟨1, ⋯⟩)).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

case h.«2»
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) ⟨2, ⋯⟩)).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map (δ ((fun i => i) ⟨2, ⋯⟩)).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 (δ 0).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    ComposableArrows.mk₁ (F.map (ev12₂ x))

Tactic:
fapply ReflPrefunctor.congr_mk₁_map

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 := ⋯ })
⊢ X.map (δ 1).op (X.map (δ 0).op x) = ev1₂ x

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).op (X.map (δ 0).op x) = ev2₂ x

case h.«0».hfg
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 := ⋯ })
⊢ Quiver.homOfEq { edge := X.map (δ 0).op x, src_eq := ⋯, tgt_eq := ⋯ } ?h.«0».hx ?h.«0».hy = ev12₂ x

Proof state:
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
⊢ mk.naturalityProperty F (δ₂ i ⋯ ⋯)

Tactic:
ext x

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 := ⋯ })
⊢ (X.map (δ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [1], property := ⋯ })) x =
    ((fun n => mk.app F (unop n)) (op { obj := [1 + 1], property := ⋯ }) ≫
        (nerveFunctor₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op)
      x

Proof state:
case h.«2»
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 (δ 2).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    SimplicialObject.δ (nerve C) 2 (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ x)))

Tactic:
rw [nerve.δ₂_mk₂_eq]

Result:
case h.«2»
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 (δ 2).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    ComposableArrows.mk₁ (F.map (ev01₂ x))

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₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op (mk.app F { obj := [1 + 1], property := ⋯ } x)

Tactic:
unfold nerveFunctor₂ truncation SimplicialObject.truncation

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 := ⋯ }) =
    ((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)