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

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 ≤ 1

Tactic:
decide

Result:
no goals

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 := ⋯ }) =
    ComposableArrows.mk₁ (F.map (ev02₂ x))

Tactic:
fapply ReflPrefunctor.congr_mk₁_map

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

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

case h.«1».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 (δ 1).op x, src_eq := ⋯, tgt_eq := ⋯ } ?h.«1».hx ?h.«1».hy = ev02₂ 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) = ev0₂ x

Tactic:
unfold ev0₂ ι0₂ δ₂

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

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

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

Result:
no goals

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

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

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

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

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 := ⋯ }) =
    ComposableArrows.mk₁ (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 := ⋯ })
⊢ 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)))

Tactic:
unfold δ₂ inclusion

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 ((fullSubcategoryInclusion fun a => a.len ≤ 2).map (δ i)).op
      (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 := ⋯ })
⊢ 1 ≤ 1

Tactic:
decide

Result:
no goals

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

Tactic:
aesop

Result:
no goals

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

Tactic:
rw [← hyp]

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 := ⋯ }) =
    ComposableArrows.mk₁ (F.map (ev02₂ x))