-- 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 })
⊢ F.app (op { obj := [2], property := hn }) x = G.app (op { obj := [2], property := hn }) x

Tactic:
apply Functor.hext (fun i : Fin 3 => ?_) (fun (i j : Fin 3) k => ?_)

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
⊢ (F.app (op { obj := [2], property := hn }) x).obj i = (G.app (op { obj := [2], property := hn }) x).obj i

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
⊢ 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
⊢ F = G

Tactic:
have eq₀ x : F.app (op ⦋0⦌₂) x = G.app (op ⦋0⦌₂) x := congr(($hyp).obj 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
⊢ 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
⊢ F = G

Tactic:
ext ⟨⟨n, hn⟩⟩ x

Result:
case w.op.mk.h
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 : SimplexCategory
hn : n.len ≤ 2
x : X.obj (op { obj := n, property := hn })
⊢ F.app (op { obj := n, property := hn }) x = G.app (op { obj := n, property := hn }) x

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 ⋯
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)

Tactic:
have h2 := congr_arg_heq (fun x => x.map' 0 1) (congr_fun (G.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))
h2 :
  HEq ((fun x => ComposableArrows.map' x 0 1 ⋯ ⋯) ((X.map (op ar) ≫ G.app (op { obj := [1], property := ⋯ })) x))
    ((fun x => ComposableArrows.map' x 0 1 ⋯ ⋯)
      ((G.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)