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

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

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 =
    ((X.map pt.op ≫ G.app (op { obj := [0], property := ⋯ })) x).obj 0

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

Tactic:
apply eq₀

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

Tactic:
exact h1.symm.trans <| .trans (congr_arg_heq (fun x => x.map' 0 1) (eq₁ _)) h2

Result:
no goals

Proof state:
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

Tactic:
induction' n using SimplexCategory.rec with n

Result:
case w.op.mk.h.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 : ℕ
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
⊢ HEq ((F.app (op { obj := [2], property := hn }) x).map k) ((G.app (op { obj := [2], property := hn }) x).map k)

Tactic:
let ar : ⦋1⦌₂ ⟶ ⦋2⦌₂ := mkOfLe _ _ k.le

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

Tactic:
apply eq₁

Result:
no goals