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

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

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

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 := ⋯ }) =
    SimplicialObject.δ (nerve C) 0 (ComposableArrows.mk₂ (F.map (ev01₂ x)) (F.map (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₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ 0 ≤ 0

Tactic:
decide

Result:
no goals

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) = ev0₂ x

Tactic:
unfold ev0₂ ι0₂ δ₂

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

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

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

Tactic:
fapply ReflPrefunctor.congr_mk₁_map

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

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

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 := ⋯ } ?h.«2».hx ?h.«2».hy = ev01₂ 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 := ⋯ })
this : δ 1 ≫ δ 2 = δ 1 ≫ δ 1
⊢ X.map (δ 1 ≫ δ 2).op x = X.map (δ 1 ≫ δ 1).op x

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

Result:
no goals

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) = ev2₂ x

Tactic:
unfold ev2₂ ι2₂ δ₂

Result:
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

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

Tactic:
simp only [types_comp_apply, mk.app_two, ComposableArrows.mk₂]

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

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

Tactic:
dsimp at this

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