awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) ((⋂ K ∈ s, K.faces) ∩ {t : Finset ι | t.Nonempty}) x
hx : Membership.mem (γ := Set (Finset ι)) (⋂ K ∈ s, K.faces) x
hn : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | t.Nonempty} x
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄,
      b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) ((⋂ K ∈ s, K.faces) ∩ {t : Finset ι | t.Nonempty}) b

Tactic:
grind [IsRelLowerSet.mem_of_le, PreAbstractSimplicialComplex.isRelLowerSet_faces,
          mem_iInter]

Premises used: IsRelLowerSet.mem_of_le, Set.mem_iInter, PreAbstractSimplicialComplex.isRelLowerSet_faces
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
v : ι
⊢ Membership.mem (γ := Set (Finset ι)) ((⋂ K ∈ s, K.faces) ∩ {t : Finset ι | t.Nonempty}) {v}

Tactic:
grind [Set.mem_iInter, Finset.singleton_nonempty, singleton_mem]

Premises used: Finset.singleton_nonempty, Set.mem_iInter, AbstractSimplicialComplex.singleton_mem
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
⊢ Eq.{u_1 + 1} (α := PreAbstractSimplicialComplex ι) (toPreAbstractSimplicialComplex ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
left : x.Nonempty
right :
  ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
left : Finset.Nonempty (α := ι) {v}
⊢ x.Nonempty

Tactic:
rw [hv]
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ Finset.Nonempty (α := ι) {v}

Tactic:
Finset.singleton_nonempty _

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ Finset.Nonempty (α := ι) {v}

Tactic:
exact Finset.singleton_nonempty _

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = ∅
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
(ht.ne_empty h).elim

Premises used: False.elim, Finset.Nonempty.ne_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = ∅
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
exact (ht.ne_empty h).elim

Premises used: False.elim, Finset.Nonempty.ne_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = {v}
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
⟨v, h⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = {v}
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
exact ⟨v, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
⊢ t = ∅ ∨ t = {v}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
          | inl h => exact (ht.ne_empty h).elim
          | inr h => exact ⟨v, h⟩

Premises used: Iff.mp, Finset.subset_singleton_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
left : sSup x ∈ upperBounds x
right : sSup x ∈ lowerBounds (upperBounds x)
⊢ IsLUB x (sSup x)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x
left :
  ∀ ⦃a : Finset ι⦄,
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) a →
      Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a
⊢ K ≤ sSup x

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a

Tactic:
Or.inl (Set.mem_biUnion hK ht)

Premises used: Set.union, Set.Mem, setOf, Set.mem_biUnion, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a

Tactic:
exact Or.inl (Set.mem_biUnion hK ht)

Premises used: Set.mem_biUnion, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
right :
  ∀ ⦃a : Finset ι⦄,
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a →
      Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
⊢ sSup x ≤ L

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) (⋃ K ∈ x, K.faces) a
⊢ ∃ (i : AbstractSimplicialComplex ι) (_ : i ∈ x), a ∈ i.faces

Tactic:
simp only [Set.mem_iUnion] at ht

Premises used: Set.mem_iUnion
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : ∃ (i : AbstractSimplicialComplex ι) (_ : i ∈ x), a ∈ i.faces
right :
  ∀ (K : AbstractSimplicialComplex ι) (hK : K ∈ x) (htK : a ∈ K.faces),
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
obtain ⟨K, hK, htK⟩ := ht
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
K : AbstractSimplicialComplex ι
hK : K ∈ x
htK : a ∈ K.faces
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
hL hK htK
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
K : AbstractSimplicialComplex ι
hK : K ∈ x
htK : a ∈ K.faces
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
exact hL hK htK
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} a
right :
  ∀ (v : ι) (hv : a = {v}), Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
obtain ⟨v, hv⟩ := ht
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
v : ι
hv : a = {v}
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
hv ▸ L.singleton_mem v

Premises used: Eq.rec, AbstractSimplicialComplex.singleton_mem, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
v : ι
hv : a = {v}
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
exact hv ▸ L.singleton_mem v
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a
right :
  ∀ (ht : Membership.mem (γ := Set (Finset ι)) (⋃ K ∈ x, K.faces) a),
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
right₁ :
  ∀ (ht : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} a),
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a

Tactic:
cases ht with
      | inl ht =>
        simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK
      | inr ht =>
        obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v

Premises used: Set.mem_iUnion
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : AbstractSimplicialComplex ι
x : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) ⊥) x
obtain :
  ∀ (v : ι) (hv : x = {v}), Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) x
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) x

Tactic:
obtain ⟨v, hv⟩ := ht
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : AbstractSimplicialComplex ι
x : Finset ι
v : ι
hv : x = {v}
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) x

Tactic:
hv ▸ K.singleton_mem v

Premises used: Eq.rec, AbstractSimplicialComplex.singleton_mem, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : AbstractSimplicialComplex ι
x : Finset ι
v : ι
hv : x = {v}
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) x

Tactic:
exact hv ▸ K.singleton_mem v
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j : J
f : Path i j
⊢ i ≤ j

Tactic:
f.left_le _ f.right

Premises used: CategoryTheory.SimplicialThickening.Path.right, CategoryTheory.SimplicialThickening.Path.left_le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ i.as ≤ l

Tactic:
(f.left_le l h)

Premises used: CategoryTheory.SimplicialThickening.Path.left_le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ g.I
⊢ i.as ≤ l

Tactic:
(Path.le f).trans (g.left_le l h)

Premises used: CategoryTheory.SimplicialThickening.Path.left_le, LE.le.trans, CategoryTheory.SimplicialThickening.Path.le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ i.as ≤ l

Tactic:
exacts [(f.left_le l h), (Path.le f).trans (g.left_le l h)]

Premises used: CategoryTheory.SimplicialThickening.Path.left_le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ l ≤ k.as

Tactic:
(f.le_right _ h).trans (Path.le g)

Premises used: LE.le.trans, CategoryTheory.SimplicialThickening.Path.le_right, CategoryTheory.SimplicialThickening.Path.le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ g.I
⊢ l ≤ k.as

Tactic:
(g.le_right l h)

Premises used: CategoryTheory.SimplicialThickening.Path.le_right
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ l ≤ k.as

Tactic:
exacts [(f.le_right _ h).trans (Path.le g), (g.le_right l h)]

Premises used: LE.le.trans, CategoryTheory.SimplicialThickening.Path.le_right, CategoryTheory.SimplicialThickening.Path.le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
I : x.I = y.I
⊢ x = y

Tactic:
apply Path.ext

Premises used: CategoryTheory.SimplicialThickening.Path.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h I : ∀ (x_1 : J), x_1 ∈ x.I ↔ x_1 ∈ y.I
⊢ x.I = y.I

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
x_1 : J
⊢ x_1 ∈ x.I ↔ x_1 ∈ y.I

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
X Y : SimplicialThickening J
f : X ⟶ Y
h : ∀ (t : J), t ∈ (𝟙 X ≫ f).I ↔ t ∈ f.I
⊢ 𝟙 X ≫ f = f

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
X Y : SimplicialThickening J
f : X ⟶ Y
t : J
⊢ t ∈ (𝟙 X ≫ f).I ↔ t ∈ f.I

Tactic:
simpa using fun h ↦ h ▸ f.left
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
X Y : SimplicialThickening J
f : X ⟶ Y
h : ∀ (t : J), t ∈ (f ≫ 𝟙 Y).I ↔ t ∈ f.I
⊢ f ≫ 𝟙 Y = f

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
X Y : SimplicialThickening J
f : X ⟶ Y
t : J
⊢ t ∈ (f ≫ 𝟙 Y).I ↔ t ∈ f.I

Tactic:
simpa using fun h ↦ h ▸ f.right
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
x : SimplicialThickening J
x_1 x_2 : SimplexCategoryᵒᵖ
x_3 : x_1 ⟶ x_2
⊢ Eq (α := (𝟙_ (Type u_1)) (𝒞 := types) ⟶ ComposableArrows (x ⟶ x) (Opposite.unop x_2).len)
    (↾fun (x_4 : (𝟙_ (Type u_1)) (𝒞 := types)) ↦ Functor.obj (Functor.const (Fin ((Opposite.unop x_2).len + 1))) (𝟙 x))
    ((↾fun (x_4 : (𝟙_ (Type u_1)) (𝒞 := types)) ↦
        Functor.obj (Functor.const (Fin ((Opposite.unop x_1).len + 1))) (𝟙 x)) ≫
      (nerve (x ⟶ x)).map x_3)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J : Type u_1
inst : LinearOrder J
i j k : SimplicialThickening J
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
⊢ Eq (α :=
    ComposableArrows (i ⟶ j) (Opposite.unop x).len × ComposableArrows (j ⟶ k) (Opposite.unop x).len ⟶
      ComposableArrows (i ⟶ k) (Opposite.unop x_1).len)
    (((nerve (i ⟶ j)).map x_2 ⊗ₘ (nerve (j ⟶ k)).map x_2) ≫
      ↾fun (x : ComposableArrows (i ⟶ j) (Opposite.unop x_1).len × ComposableArrows (j ⟶ k) (Opposite.unop x_1).len) ↦
        Functor.prod' x.1 x.2 ⋙ i.compFunctor j k)
    ((↾fun (x_3 : ComposableArrows (i ⟶ j) (Opposite.unop x).len × ComposableArrows (j ⟶ k) (Opposite.unop x).len) ↦
        Functor.prod' x_3.1 x_3.2 ⋙ i.compFunctor j k) ≫
      (nerve (i ⟶ k)).map x_2)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ LE.le (α := K) (as { as := (f : (a : J) → K) i.as } : K) ((f : (a : J) → K) k : K)

Tactic:
f.monotone (I.left_le k hk)

Premises used: OrderHom.monotone, CategoryTheory.SimplicialThickening.Path.left_le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ LE.le (α := K) (as { as := (f : (a : J) → K) i.as } : K) ((f : (a : J) → K) k : K)

Tactic:
exact f.monotone (I.left_le k hk)

Premises used: OrderHom.monotone, CategoryTheory.SimplicialThickening.Path.left_le
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ LE.le (α := K) ((f : (a : J) → K) k : K) (as { as := (f : (a : J) → K) j.as } : K)

Tactic:
f.monotone (I.le_right k hk)

Premises used: OrderHom.monotone, CategoryTheory.SimplicialThickening.Path.le_right
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ LE.le (α := K) ((f : (a : J) → K) k : K) (as { as := (f : (a : J) → K) j.as } : K)

Tactic:
exact f.monotone (I.le_right k hk)

Premises used: OrderHom.monotone, CategoryTheory.SimplicialThickening.Path.le_right
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i : SimplicialThickening J
w :
  ∀ (n : SimplexCategoryᵒᵖ) (x : (𝟙_ SSet) (𝒞 := Functor.category).obj n),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((eId SSet i ≫ nerveMap (functorMap f i i)).app n)).toFun x =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (NatTrans.app (eId SSet { as := (f : (a : J) → K) i.as }) n))
        x
⊢ eId SSet i ≫ nerveMap (functorMap f i i) = eId SSet { as := (f : (a : J) → K) i.as }

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i : SimplicialThickening J
n : SimplexCategoryᵒᵖ
x : (𝟙_ SSet) (𝒞 := Functor.category).obj n
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({
              app := fun (x : SimplexCategoryᵒᵖ) ↦
                ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj x) ↦
                  Functor.obj (Functor.const (Fin ((Opposite.unop x).len + 1))) (𝟙 i),
              naturality := ⋯ : NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) (nerve (i ⟶ i)) } ≫
            nerveMap (functorMap f i i))
          n))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : (𝟙_ SSet) (𝒞 := Functor.category).obj n) ↦
          Functor.obj (Functor.const (Fin ((Opposite.unop n).len + 1)))
            (𝟙 { as := (f : (a : J) → K) i.as : SimplicialThickening K })))
      x

Tactic:
exact Functor.ext (by cat_disch)

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
w :
  ∀ (n : SimplexCategoryᵒᵖ)
    (x :
      Functor.obj
        (tensorObj (𝒞 := Functor.category) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
          (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ j k))
        n),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((eComp SSet i j k ≫ nerveMap (functorMap f i k)).app n)).toFun x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
              eComp SSet { as := (f : (a : J) → K) i.as : SimplicialThickening K }
                { as := (f : (a : J) → K) j.as : SimplicialThickening K }
                { as := (f : (a : J) → K) k.as : SimplicialThickening K })
            n))
        x
⊢ eComp SSet i j k ≫ nerveMap (functorMap f i k) =
    (nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
      eComp SSet { as := (f : (a : J) → K) i.as } { as := (f : (a : J) → K) j.as } { as := (f : (a : J) → K) k.as }

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialNerve
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
n : SimplexCategoryᵒᵖ
x :
  Functor.obj
    (tensorObj (𝒞 := Functor.category) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
      (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ j k))
    n
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({
              app := fun (x : SimplexCategoryᵒᵖ) ↦
                ↾fun (x_1 : (tensorObj (𝒞 := Functor.category) (nerve (i ⟶ j)) (nerve (j ⟶ k))).obj x) ↦
                  Functor.prod' x_1.1 x_1.2 ⋙ i.compFunctor j k,
              naturality := ⋯ :
              NatTrans (tensorObj (𝒞 := Functor.category) (nerve (i ⟶ j)) (nerve (j ⟶ k))) (nerve (i ⟶ k)) } ≫
            nerveMap (functorMap f i k))
          n))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
            {
              app := fun (x : SimplexCategoryᵒᵖ) ↦
                ↾fun
                    (x_1 :
                      (tensorObj (𝒞 := Functor.category)
                            (nerve
                              (Quiver.Hom (V := SimplicialThickening K)
                                ({ as := (f : (a : J) → K) i.as } : SimplicialThickening K)
                                ({ as := (f : (a : J) → K) j.as } : SimplicialThickening K)))
                            (nerve
                              (Quiver.Hom (V := SimplicialThickening K)
                                ({ as := (f : (a : J) → K) j.as } : SimplicialThickening K)
                                ({ as := (f : (a : J) → K) k.as } : SimplicialThickening K)))).obj
                        x) ↦
                  Functor.prod' x_1.1 x_1.2 ⋙
                    compFunctor { as := (f : (a : J) → K) i.as : SimplicialThickening K }
                      { as := (f : (a : J) → K) j.as : SimplicialThickening K }
                      { as := (f : (a : J) → K) k.as : SimplicialThickening K },
              naturality := ⋯ :
              NatTrans
                (tensorObj (𝒞 := Functor.category)
                  (nerve
                    (Quiver.Hom (V := SimplicialThickening K)
                      ({ as := (f : (a : J) → K) i.as } : SimplicialThickening K)
                      ({ as := (f : (a : J) → K) j.as } : SimplicialThickening K)))
                  (nerve
                    (Quiver.Hom (V := SimplicialThickening K)
                      ({ as := (f : (a : J) → K) j.as } : SimplicialThickening K)
                      ({ as := (f : (a : J) → K) k.as } : SimplicialThickening K))))
                (nerve
                  (Quiver.Hom (V := SimplicialThickening K) ({ as := (f : (a : J) → K) i.as } : SimplicialThickening K)
                    ({ as := (f : (a : J) → K) k.as } : SimplicialThickening K))) })
          n))
      x

Tactic:
exact Functor.ext (by cat_disch)

Premises used: CategoryTheory.Functor.ext