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

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

Tactic:
show _ = (nerve C).δ 1 _

Result:
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 (δ 1).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    SimplicialObject.δ (nerve C) 1 (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ 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 := ⋯ })
⊢ mk.app F { obj := [1], property := ⋯ } (X.map (δ₂ i ⋯ ⋯).op x) =
    (nerveFunctor₂.obj (Cat.of C)).map (δ₂ i ⋯ ⋯).op (mk.app F { obj := [1 + 1], property := ⋯ } x)

Tactic:
rw [toNerve₂.mk.app_one]

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

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

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

Proof state:
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)))

Tactic:
simp only [Fin.mk_one]

Result:
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 (δ 1).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    (nerve C).map (δ 1).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).op (X.map (δ 0).op x) = ev1₂ x

Tactic:
unfold ev1₂ ι1₂ δ₂

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

Proof state:
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 := ⋯ } ⋯ ⋯ = ev12₂ x

Tactic:
aesop

Result:
no goals

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

Tactic:
simp only [Fin.reduceFinMk]

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 := ⋯ }) =
    (nerve C).map (δ 2).op (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (ev12₂ 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).op (X.map (δ 0).op x) = ev2₂ x

Tactic:
unfold ev2₂ ι2₂ δ₂

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

Proof state:
case h.«2».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 (δ 2).op x, src_eq := ⋯, tgt_eq := ⋯ } ⋯ ⋯ = ev01₂ x

Tactic:
aesop

Result:
no goals

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

Tactic:
dsimp at this

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