-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
theorem toNerve₂.ext (F G : X ⟶ nerveFunctor₂.obj (Cat.of C))
    (hyp : SSet.oneTruncation₂.map F = SSet.oneTruncation₂.map G) : F = G

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i : Fin 3
⊢ (F.app (op { obj := [2], property := hn }) x).obj i = (G.app (op { obj := [2], property := hn }) x).obj i

Tactic:
let pt : ⦋0⦌₂ ⟶ ⦋2⦌₂ := SimplexCategory.const _ _ i

Result:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i : Fin 3
pt : { obj := [0], property := ⋯ } ⟶ { obj := [2], property := ⋯ } :=
  { obj := [0], property := ⋯ }.obj.const { obj := [2], property := ⋯ }.obj i
⊢ (F.app (op { obj := [2], property := hn }) x).obj i = (G.app (op { obj := [2], property := hn }) x).obj i

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i j : Fin 3
k : i ⟶ j
ar : { obj := [1], property := ⋯ } ⟶ { obj := [2], property := ⋯ } := mkOfLe i j ⋯
⊢ HEq ((F.app (op { obj := [2], property := hn }) x).map k) ((G.app (op { obj := [2], property := hn }) x).map k)

Tactic:
have h1 := congr_arg_heq (fun x => x.map' 0 1) (congr_fun (F.naturality (op ar)) x)

Result:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i j : Fin 3
k : i ⟶ j
ar : { obj := [1], property := ⋯ } ⟶ { obj := [2], property := ⋯ } := mkOfLe i j ⋯
h1 :
  HEq ((fun x => ComposableArrows.map' x 0 1 ⋯ ⋯) ((X.map (op ar) ≫ F.app (op { obj := [1], property := ⋯ })) x))
    ((fun x => ComposableArrows.map' x 0 1 ⋯ ⋯)
      ((F.app (op { obj := [2], property := ⋯ }) ≫ (nerveFunctor₂.obj (Cat.of C)).map (op ar)) x))
⊢ HEq ((F.app (op { obj := [2], property := hn }) x).map k) ((G.app (op { obj := [2], property := hn }) x).map k)

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i : Fin 3
pt : { obj := [0], property := ⋯ } ⟶ { obj := [2], property := ⋯ } :=
  { obj := [0], property := ⋯ }.obj.const { obj := [2], property := ⋯ }.obj i
⊢ ((X.map pt.op ≫ F.app (op { obj := [0], property := ⋯ })) x).obj 0 =
    ((X.map pt.op ≫ G.app (op { obj := [0], property := ⋯ })) x).obj 0

Tactic:
exact congr($(eq₀ _).obj 0)

Result:
no goals

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
⊢ F = G

Tactic:
have eq₁ x : F.app (op ⦋1⦌₂) x = G.app (op ⦋1⦌₂) x := congr((($hyp).map ⟨x, rfl, rfl⟩).1)

Result:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
⊢ F = G

Proof state:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i : Fin 3
pt : { obj := [0], property := ⋯ } ⟶ { obj := [2], property := ⋯ } :=
  { obj := [0], property := ⋯ }.obj.const { obj := [2], property := ⋯ }.obj i
⊢ (F.app (op { obj := [2], property := hn }) x).obj i = (G.app (op { obj := [2], property := hn }) x).obj i

Tactic:
refine congr(($(congr_fun (F.naturality pt.op) x)).obj 0).symm.trans ?_

Result:
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F G : X ⟶ nerveFunctor₂.obj (Cat.of C)
hyp : oneTruncation₂.map F = oneTruncation₂.map G
eq₀ :
  ∀ (x : X.obj (op { obj := [0], property := ⋯ })),
    F.app (op { obj := [0], property := ⋯ }) x = G.app (op { obj := [0], property := ⋯ }) x
eq₁ :
  ∀ (x : X.obj (op { obj := [1], property := ⋯ })),
    F.app (op { obj := [1], property := ⋯ }) x = G.app (op { obj := [1], property := ⋯ }) x
n : ℕ
hn : [2].len ≤ 2
x : X.obj (op { obj := [2], property := hn })
i : Fin 3
pt : { obj := [0], property := ⋯ } ⟶ { obj := [2], property := ⋯ } :=
  { obj := [0], property := ⋯ }.obj.const { obj := [2], property := ⋯ }.obj i
⊢ ((X.map pt.op ≫ F.app (op { obj := [0], property := ⋯ })) x).obj 0 =
    (G.app (op { obj := [2], property := hn }) x).obj i