awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋n⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.arrow i.castSucc

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.castSucc).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.castSucc
rw₁ rw₂ : f.arrow i.castSucc = f.arrow i.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.castSucc

Tactic:
rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]

Premises used: SimplexCategory.mkOfSucc_δ_lt, SSet.StrictSegal.spineToSimplex_arrow
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋n⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.arrow i.succ
⊢ (X.spine n
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (sx.spineToSimplex f))).arrow
      i =
    f.arrow i.succ

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Premises used: SSet.spine_arrow, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.succ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋n⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.arrow i.succ

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.succ
rw₁ rw₂ : f.arrow i.succ = f.arrow i.succ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.succ

Tactic:
rw [mkOfSucc_δ_gt h, spineToSimplex_arrow]

Premises used: SimplexCategory.mkOfSucc_δ_gt, SSet.StrictSegal.spineToSimplex_arrow
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i_1 : Fin (n + 1)
j_1 : Fin (n + 2)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (↑i : ℕ) + 2 ≤ n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋n⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
⊢ (X.spine n
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (sx.spineToSimplex f))).arrow
      i =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Premises used: SSet.spine_arrow, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋n⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (intervalEdge (↑i : ℕ) 2 ⋯))) :
        (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
rw₁ rw₂ : sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯) = sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)

Tactic:
rw [mkOfSucc_δ_eq h, spineToSimplex_edge]

Premises used: SSet.StrictSegal.spineToSimplex_edge, SimplexCategory.mkOfSucc_δ_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ X.spine 0 (p.vertex 0) = p

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ { s : X _⦋0⦌ // X.spine 0 s = p }

Tactic:
exact ⟨p.vertex 0, by aesop⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
succ :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (p.arrow 0) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
succ₁ : X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯) = p
⊢ { s : X _⦋n + 1⦌ // X.spine (n + 1) s = p }

Tactic:
refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
succ :
  p.vertex (Fin.succ 0) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (p.arrow 0) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))

Tactic:
rw [p.arrow_tgt 0]

Premises used: SSet.Path.arrow_tgt, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ p.vertex (Fin.succ 0) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌)

Tactic:
Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0

Premises used: Fin.succ, Quiver.Hom.op, SSet.Path.congr_vertex, SimplexCategory.const, Subtype.prop, Nat.mod, SSet.Path.interval, OfNat.ofNat, Eq.symm, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ p.vertex (Fin.succ 0) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌)

Tactic:
exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0

Premises used: SSet.Path.congr_vertex, Subtype.prop, SSet.Path.interval, OfNat.ofNat, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
succ :
  ∀ (i : Fin (n + 1)),
    (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow i = p.arrow i
⊢ X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯) = p

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin (n + 1)
succ : (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow 0 = p.arrow 0
succ₁ :
  ∀ (i : Fin n),
    (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow i.succ = p.arrow i.succ
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow i = p.arrow i

Tactic:
obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ

Premises used: Fin.eq_zero_or_eq_succ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
succ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯) =
    p.arrow 0
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow 0 = p.arrow 0

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
succ succ₁ : p.arrow 0 = p.arrow 0
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯) =
    p.arrow 0

Tactic:
rw [map_mkOfSucc_zero_concat]

Premises used: SSet.StrictSegalCore.map_mkOfSucc_zero_concat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 0 < i.succ.castSucc

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 1 + n ≤ n + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 1 + (↑i : ℕ) = (↑i.succ : ℕ)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow i.succ = p.arrow i.succ

Tactic:
simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
          op_comp, Functor.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
          ← p.arrow_interval 1 n i i.succ (by grind) (by grind)] using
            Path.congr_arrow (hn (p.interval 1 n)).prop i

Premises used: CategoryTheory.op_comp, Fin.succ, CategoryTheory.SimplicialObject.δ_def, SSet.spine_arrow, SSet.StrictSegalCore.δ₀_concat, CategoryTheory.Functor.map_comp_apply, SSet.Path.congr_arrow, SimplexCategory.mkOfSucc_δ_gt, Subtype.prop, SSet.Path.arrow_interval, SSet.Path.interval, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
zero : (p : X.Path 0) → { s : X _⦋0⦌ // X.spine 0 s = p }
succ :
  (n : ℕ) →
    (hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }) →
      (p : X.Path (n + 1)) → { s : X _⦋n + 1⦌ // X.spine (n + 1) s = p }
⊢ { s : X _⦋n⦌ // X.spine n s = p }

Tactic:
induction n with
  | zero => exact ⟨p.vertex 0, by aesop⟩
  | succ n hn =>
    refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
    · rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0
    · ext i
      obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
      · dsimp
        rw [map_mkOfSucc_zero_concat]
      · simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
          op_comp, Functor.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
          ← p.arrow_interval 1 n i i.succ (by grind) (by grind)] using
            Path.congr_arrow (hn (p.interval 1 n)).prop i

Premises used: CategoryTheory.op_comp, SSet.StrictSegalCore.map_mkOfSucc_zero_concat, CategoryTheory.SimplicialObject.δ_def, SSet.spine_arrow, SSet.StrictSegalCore.δ₀_concat, CategoryTheory.Functor.map_comp_apply, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
⊢ X.spine n (spineToSimplex h p) = p

Tactic:
(spineToSimplexAux h p).prop

Premises used: SSet.StrictSegalCore.spineToSimplexAux, SSet.StrictSegalCore.spineToSimplex, Subtype.prop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ spineToSimplex h p = p.vertex 0

Tactic:
rfl

Premises used: SSet.StrictSegalCore.spineToSimplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p_1 : X.Path n
p : X.Path (n + 1)
rw :
  p.vertex (Fin.succ 0) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (spineToSimplex h (p.interval 1 n ⋯))
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (p.arrow 0) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (spineToSimplex h (p.interval 1 n ⋯)) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))

Tactic:
rw [p.arrow_tgt 0]

Premises used: SSet.Path.arrow_tgt, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p_1 : X.Path n
p : X.Path (n + 1)
⊢ p.vertex (Fin.succ 0) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (spineToSimplex h (p.interval 1 n ⋯))

Tactic:
Path.congr_vertex (spine_spineToSimplex h (p.interval 1 n)).symm 0

Premises used: Fin.succ, Quiver.Hom.op, SSet.Path.congr_vertex, SimplexCategory.const, Nat.mod, SSet.Path.interval, OfNat.ofNat, Eq.symm, SSet.StrictSegalCore.spine_spineToSimplex, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p_1 : X.Path n
p : X.Path (n + 1)
⊢ p.vertex (Fin.succ 0) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (spineToSimplex h (p.interval 1 n ⋯))

Tactic:
exact Path.congr_vertex (spine_spineToSimplex h (p.interval 1 n)).symm 0

Premises used: SSet.Path.congr_vertex, SSet.Path.interval, OfNat.ofNat, Eq.symm, SSet.StrictSegalCore.spine_spineToSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ spineToSimplex h p = (h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯

Tactic:
rfl

Premises used: SSet.StrictSegalCore.spineToSimplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    p.arrow 0
rw₁ rw₂ : p.arrow 0 = p.arrow 0
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (spineToSimplex h p) =
    p.arrow 0

Tactic:
rw [spineToSimplex_succ, map_mkOfSucc_zero_concat]

Premises used: SSet.StrictSegalCore.map_mkOfSucc_zero_concat, SSet.StrictSegalCore.spineToSimplex_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    spineToSimplex h (p.interval 1 n ⋯)
rw₁ rw₂ : spineToSimplex h (p.interval 1 n ⋯) = spineToSimplex h (p.interval 1 n ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (spineToSimplex h p) =
    spineToSimplex h (p.interval 1 n ⋯)

Tactic:
rw [spineToSimplex_succ, δ₀_concat]

Premises used: SSet.StrictSegalCore.δ₀_concat, SSet.StrictSegalCore.spineToSimplex_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋0⦌
⊢ spineToSimplex h (X.spine 0 s) = s

Tactic:
simp [spineToSimplex_zero]

Premises used: SSet.StrictSegalCore.spineToSimplex_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n_1 n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
rw :
  spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      s
rw₁ :
  spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) =
    spineToSimplex h
      (X.spine n
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          s))
rw₂ rw₃ : spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) = spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (spineToSimplex h (X.spine (n + 1) s)) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        s :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))

Tactic:
rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀]

Premises used: CategoryTheory.ConcreteCategory.hom, SSet.spine_δ₀, SSet.StrictSegalCore.δ₀_spineToSimplex, CategoryTheory.SimplicialObject.δ, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n_1 n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ spineToSimplex h (X.spine (n + 1) s) = s

Tactic:
exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])

Premises used: SSet.StrictSegalCore.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋n⦌
zero : ∀ (s : X _⦋0⦌), spineToSimplex h (X.spine 0 s) = s
succ :
  ∀ (n : ℕ) (hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s) (s : X _⦋n + 1⦌),
    spineToSimplex h (X.spine (n + 1) s) = s
⊢ spineToSimplex h (X.spine n s) = s

Tactic:
induction n with
  | zero => simp [spineToSimplex_zero]
  | succ n hn =>
    exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])

Premises used: SSet.StrictSegalCore.spineToSimplex_zero, SSet.StrictSegalCore.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
⊢ ∀ (n : ℕ), X.spine n ∘ StrictSegalCore.spineToSimplex h = id

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
⊢ StrictSegalCore.spineToSimplex h ∘ X.spine n = id

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
C : Type u
inst : Category.{v, u} C
⊢ (nerve.{v, u} C).IsStrictSegal

Tactic:
strictSegal C |>.isStrictSegal

Premises used: CategoryTheory.Nerve.strictSegal, SSet.StrictSegal.isStrictSegal
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
rw : ∀ (X_1 : SimplexCategoryᵒᵖ), IsIso (f.app X_1)
⊢ IsIso f

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
rw :
  Function.Bijective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
⊢ IsIso (f.app X_1)

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective