-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
lemma toNerve₂.mk_naturality_σ00 : toNerve₂.mk.naturalityProperty F (σ₂ (n := 0) 0)

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
⊢ (X.map (σ₂ 0 ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ })) x =
    ComposableArrows.mk₁ (𝟙 (F.obj x))

Tactic:
have := ReflPrefunctor.map_id F x

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙rq (F.obj x)
⊢ (X.map (σ₂ 0 ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ })) x =
    ComposableArrows.mk₁ (𝟙 (F.obj x))

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙rq (F.obj x)
⊢ (X.map (σ₂ 0 ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ })) x =
    ComposableArrows.mk₁ (𝟙 (F.obj x))

Tactic:
dsimp at this ⊢

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (σ₂ 0 ⋯ ⋯).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    ComposableArrows.mk₁ (𝟙 (F.obj x))

Proof state:
case h.hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ X.map (δ₂ 1 ⋯ ⋯).op (𝟙rq x).edge = x

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

Result:
no goals

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
⊢ mk.naturalityProperty F (σ₂ 0 ⋯ ⋯)

Tactic:
ext x

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
⊢ (X.map (σ₂ 0 ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ })) x =
    ((fun n => mk.app F (unop n)) (op { obj := [0], property := ⋯ }) ≫ (nerveFunctor₂.obj (Cat.of C)).map (σ₂ 0 ⋯ ⋯).op)
      x

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ ComposableArrows.mk₁ (F.map { edge := X.map (σ₂ 0 ⋯ ⋯).op x, src_eq := ⋯, tgt_eq := ⋯ }) =
    ComposableArrows.mk₁ (𝟙 (F.obj x))

Tactic:
rw [← this, ← OneTruncation₂.id_edge x]

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ ComposableArrows.mk₁ (F.map { edge := (𝟙rq x).edge, src_eq := ⋯, tgt_eq := ⋯ }) = ComposableArrows.mk₁ (F.map (𝟙rq x))

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
⊢ (X.map (σ₂ 0 ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ })) x =
    ((fun n => mk.app F (unop n)) (op { obj := [0], property := ⋯ }) ≫ (nerveFunctor₂.obj (Cat.of C)).map (σ₂ 0 ⋯ ⋯).op)
      x

Tactic:
refine Eq.trans ?_ (nerve.σ₀_mk₀_eq (C := C) (F.obj x)).symm

Result:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
⊢ (X.map (σ₂ 0 ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [0 + 1], property := ⋯ })) x =
    ComposableArrows.mk₁ (𝟙 (F.obj x))

Proof state:
case h
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ ComposableArrows.mk₁ (F.map { edge := (𝟙rq x).edge, src_eq := ⋯, tgt_eq := ⋯ }) = ComposableArrows.mk₁ (F.map (𝟙rq x))

Tactic:
fapply ReflPrefunctor.congr_mk₁_map

Result:
case h.hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ X.map (δ₂ 1 ⋯ ⋯).op (𝟙rq x).edge = x

case h.hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ X.map (δ₂ 0 ⋯ ⋯).op (𝟙rq x).edge = x

case h.hfg
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ Quiver.homOfEq { edge := (𝟙rq x).edge, src_eq := ⋯, tgt_eq := ⋯ } ?h.hx ?h.hy = 𝟙rq x

Proof state:
case h.hfg
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ Quiver.homOfEq { edge := (𝟙rq x).edge, src_eq := ⋯, tgt_eq := ⋯ } ⋯ ⋯ = 𝟙rq x

Tactic:
aesop

Result:
no goals

Proof state:
case h.hy
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
x : X.obj (op { obj := [0], property := ⋯ })
this : F.map (𝟙rq x) = 𝟙 (F.obj x)
⊢ X.map (δ₂ 0 ⋯ ⋯).op (𝟙rq x).edge = x

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

Result:
no goals