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

Proof state:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (δ₂ 2 ⋯ ⋯ ≫ σ₂ ((fun i => i) ⟨1, ⋯⟩) ⋯ ⋯)

Tactic:
dsimp only [Fin.mk_one]

Result:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (δ₂ 2 ⋯ ⋯ ≫ σ₂ 1 ⋯ ⋯)

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

Tactic:
change toNerve₂.mk.naturalityProperty F (δ₂ 2 ≫ σ₂ i)

Result:
case e_f
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 2
⊢ mk.naturalityProperty F (δ₂ 2 ⋯ ⋯ ≫ σ₂ i ⋯ ⋯)

Proof state:
case e_g.«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₂ φ)
⊢ mk.naturalityProperty F (δ₂ 0 ⋯ ⋯ ≫ σ₂ 1 ⋯ ⋯)

Tactic:
rw [δ₂_zero_comp_σ₂_one]

Result:
case e_g.«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₂ φ)
⊢ mk.naturalityProperty F (σ₂ 0 ⋯ ⋯ ≫ δ₂ 0 ⋯ ⋯)

Proof state:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (σ₂ 0 ⋯ ⋯ ≫ δ₂ 1 ⋯ ⋯)

Tactic:
exact (toNerve₂.mk.naturalityProperty F).comp_mem _ _
  (toNerve₂.mk_naturality_σ00 F) (toNerve₂.mk_naturality_δ0i F _)

Result:
no goals

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

Tactic:
simp only [nerve₂.seagull, prod.comp_lift, assoc]

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

Proof state:
case e_g
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 2
⊢ X.map (δ₂ 0 ⋯ ⋯ ≫ σ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [1], property := ⋯ }) =
    mk.app F { obj := [1], property := ⋯ } ≫
      (nerveFunctor₂.obj (Cat.of C)).map (δ₂ 0 δ0₂.proof_2 δ0₂.proof_3 ≫ σ₂ i ⋯ ⋯).op

Tactic:
change toNerve₂.mk.naturalityProperty F (δ₂ 0 ≫ σ₂ i)

Result:
case e_g
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 2
⊢ mk.naturalityProperty F (δ₂ 0 ⋯ ⋯ ≫ σ₂ i ⋯ ⋯)

Proof state:
case e_f
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 2
⊢ X.map (σ₂ i ⋯ ⋯).op ≫
      mk.app F { obj := [1 + 1], property := ⋯ } ≫
        (nerveFunctor₂.obj (Cat.of C)).map (δ₂ 2 δ2₂.proof_2 δ2₂.proof_3).op =
    mk.app F { obj := [1], property := ⋯ } ≫
      (nerveFunctor₂.obj (Cat.of C)).map (δ₂ 2 δ2₂.proof_2 δ2₂.proof_3 ≫ σ₂ i ⋯ ⋯).op

Tactic:
rw [← toNerve₂.mk_naturality_δ1i F hyp, ← assoc, ← map_comp, ← op_comp]

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

Proof state:
case e_g.«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₂ φ)
⊢ mk.naturalityProperty F (𝟙 { obj := [1], property := ⋯ })

Tactic:
exact (toNerve₂.mk.naturalityProperty F).id_mem _

Result:
no goals

Proof state:
case e_g.«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₂ φ)
⊢ mk.naturalityProperty F (δ₂ 0 ⋯ ⋯ ≫ σ₂ 0 ⋯ ⋯)

Tactic:
rw [δ₂_zero_comp_σ₂_zero]

Result:
case e_g.«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₂ φ)
⊢ mk.naturalityProperty F (𝟙 { obj := [1], property := ⋯ })

Proof state:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (δ₂ 2 ⋯ ⋯ ≫ σ₂ 1 ⋯ ⋯)

Tactic:
rw [δ₂_two_comp_σ₂_one]

Result:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (𝟙 { obj := [1], property := ⋯ })

Proof state:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (δ₂ 2 ⋯ ⋯ ≫ σ₂ 0 ⋯ ⋯)

Tactic:
rw [δ₂_two_comp_σ₂_zero]

Result:
case e_f.«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₂ φ)
⊢ mk.naturalityProperty F (σ₂ 0 ⋯ ⋯ ≫ δ₂ 1 ⋯ ⋯)