awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
h :
  Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((opObjEquiv : (a : Δ[n.len].op _⦋d'.1.len⦌) → Δ[n.len] _⦋d'.1.len⦌)
              ((Equiv.symm opObjEquiv :
                    (a : (stdSimplex.obj n).obj (op (rev.obj (unop d')))) →
                      (stdSimplex.obj n).op.obj (op (rev.obj (unop d'))))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                        (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d))))) →
                          (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d')))))
                      ((opObjEquiv :
                            (a : (stdSimplex.obj n).op.obj (op (rev.obj (unop d)))) →
                              (stdSimplex.obj n).obj (op (rev.obj (unop d))))
                          g :
                        (stdSimplex.obj n).obj (op (rev.obj (unop d)))) :
                    (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d'))))) :
                (stdSimplex.obj n).op.obj (op (rev.obj (unop d')))) :
            Δ[n.len] _⦋len d'.1⦌) :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i.rev))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)
⊢ Eq (α := Fin (n.len + 1))
    ((((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d') → (stdSimplex.obj n).obj d')
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).op.map f) :
                    (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).op.obj d')
                  g :
                (stdSimplex.obj n).op.obj d') :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i :
      Fin (n.len + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
                (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
              ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
                (stdSimplex.obj n).obj d) :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i :
      Fin (n.len + 1))

Tactic:
rw [stdSimplex.opObjEquiv_apply, op_map]

Premises used: SSet.stdSimplex.opObjEquiv_apply, SSet.op_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
h :
  Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
              ((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
                (stdSimplex.obj n).obj d) :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i.rev))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)
⊢ Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d))))) →
                  (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d')))))
              ((opObjEquiv :
                    (a : (stdSimplex.obj n).op.obj (op (rev.obj (unop d)))) →
                      (stdSimplex.obj n).obj (op (rev.obj (unop d))))
                  g :
                (stdSimplex.obj n).obj (op (rev.obj (unop d)))) :
            (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d'))))) :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i.rev))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
h :
  Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g : (stdSimplex.obj n).obj d) :
          (a : Fin (d.1.len + 1)) → Fin (n.len + 1))
        (Fin.rev
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f.unop :
              (a : Fin (d'.1.len + 1)) → Fin (d.1.len + 1))
            i.rev.rev))))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)
⊢ Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
              ((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
                (stdSimplex.obj n).obj d) :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i.rev))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)

Tactic:
rw [map_rev_map_op_apply]

Premises used: SSet.stdSimplex.map_rev_map_op_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
⊢ Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g : (stdSimplex.obj n).obj d) :
          (a : Fin (d.1.len + 1)) → Fin (n.len + 1))
        (Fin.rev
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f.unop :
              (a : Fin (d'.1.len + 1)) → Fin (d.1.len + 1))
            i.rev.rev))))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
dsimp : LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
⊢ LE.le (α := Fin (⦋1⦌.len + 1))
    ((fun (j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) ↦ (if j.castSucc < i then 0 else 1 : Fin (⦋1⦌.len + 1)))
      j₁)
    ((fun (j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) ↦ (if j.castSucc < i then 0 else 1 : Fin (⦋1⦌.len + 1)))
      j₂)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
neg : j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 0 1
pos₁ : ¬j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 1 0
neg₁ : ¬j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 1 1
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h_1 : j₁.castSucc < i
h_2 : j₂.castSucc < i
⊢ LE.le (α := Fin 2) 0 0

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h_1 : j₁.castSucc < i
h_2 : ¬j₂.castSucc < i
⊢ LE.le (α := Fin 2) 0 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h_1 : ¬j₁.castSucc < i
h_2 : j₂.castSucc < i
⊢ LE.le (α := Fin 2) 1 0

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h_1 : ¬j₁.castSucc < i
h_2 : ¬j₂.castSucc < i
⊢ LE.le (α := Fin 2) 1 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := Fin 2) ((objMk₁ i : (a : Fin (n + 1)) → Fin 2) j : Fin 2) (if j.castSucc < i then 0 else 1 : Fin 2)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := Fin 2) ((objMk₁ i : (a : Fin (n + 1)) → Fin 2) j : Fin 2) (0 : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↔ j.castSucc < i

Tactic:
SimplexCategory.toMk₁_apply_eq_zero_iff ..

Premises used: SimplexCategory.toMk₁_apply_eq_zero_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ Eq (α := Fin 2) ((objMk₁ i : (a : Fin (n + 1)) → Fin 2) j : Fin 2) (0 : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
SimplexCategory.toMk₁_of_castSucc_lt _ _ h

Premises used: SimplexCategory.toMk₁_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := Fin 2) ((objMk₁ i : (a : Fin (n + 1)) → Fin 2) j : Fin 2) (1 : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↔ i ≤ j.castSucc

Tactic:
SimplexCategory.toMk₁_apply_eq_one_iff ..

Premises used: SimplexCategory.toMk₁_apply_eq_one_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ Eq (α := Fin 2) ((objMk₁ i : (a : Fin (n + 1)) → Fin 2) j : Fin 2) (1 : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
SimplexCategory.toMk₁_of_le_castSucc _ _ h

Premises used: SimplexCategory.toMk₁_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
h₁ :
  ∀ (k : Fin (n + 1)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                  (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
                (objMk₁ i) :
              (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
            (a : Fin (n + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((objMk₁ (i.castPred ⋯) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
      (objMk₁ i) =
    objMk₁ (i.castPred ⋯)

Tactic:
ext k : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
k : Fin (n + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ (i.castPred ⋯) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
ConcreteCategory.congr_hom (SimplexCategory.δ_comp_toMk₁_of_le _ _ h) k

Premises used: SimplexCategory.δ_comp_toMk₁_of_le, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
k : Fin (n + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ (i.castPred ⋯) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
exact ConcreteCategory.congr_hom (SimplexCategory.δ_comp_toMk₁_of_le _ _ h) k

Premises used: SimplexCategory.δ_comp_toMk₁_of_le, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
h₁ :
  ∀ (k : Fin (n + 1)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                  (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
                (objMk₁ i) :
              (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
            (a : Fin (n + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((objMk₁ (i.pred ⋯) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
      (objMk₁ i) =
    objMk₁ (i.pred ⋯)

Tactic:
ext k : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
k : Fin (n + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ (i.pred ⋯) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
ConcreteCategory.congr_hom (SimplexCategory.δ_comp_toMk₁_of_lt _ _ h) k

Premises used: CategoryTheory.ConcreteCategory.congr_hom, SimplexCategory.δ_comp_toMk₁_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
k : Fin (n + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ (i.pred ⋯) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
exact ConcreteCategory.congr_hom (SimplexCategory.δ_comp_toMk₁_of_lt _ _ h) k

Premises used: CategoryTheory.ConcreteCategory.congr_hom, SimplexCategory.δ_comp_toMk₁_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
h₁ :
  ∀ (k : Fin (n + 1 + 1)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                  (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
                (objMk₁ i) :
              (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
            (a : Fin (n + 1 + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((objMk₁ i.castSucc : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
      (objMk₁ i) =
    objMk₁ i.castSucc

Tactic:
ext k : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (n + 1 + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ i.castSucc : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_le _ _ h) k

Premises used: SimplexCategory.σ_comp_toMk₁_of_le, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (n + 1 + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ i.castSucc : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
exact ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_le _ _ h) k

Premises used: SimplexCategory.σ_comp_toMk₁_of_le, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
h₁ :
  ∀ (k : Fin (n + 1 + 1)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                  (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
                (objMk₁ i) :
              (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
            (a : Fin (n + 1 + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((objMk₁ i.succ : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
      (objMk₁ i) =
    objMk₁ i.succ

Tactic:
ext k : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (n + 1 + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ i.succ : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_lt _ _ h) k

Premises used: SimplexCategory.σ_comp_toMk₁_of_lt, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (n + 1 + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ i.succ : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
exact ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_lt _ _ h) k

Premises used: SimplexCategory.σ_comp_toMk₁_of_lt, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
⊢ Function.Bijective.{1, u + 1} (α := Fin (n + 2)) objMk₁

Tactic:
((SimplexCategory.toMk₁Equiv (n := n)).trans objEquiv.symm).bijective

Premises used: Equiv.bijective, SimplexCategory.toMk₁, Equiv.trans, SSet.stdSimplex.objMk₁, Equiv.symm, SimplexCategory.toMk₁Equiv, SSet.stdSimplex.objEquiv, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
⊢ Function.Injective.{1, u + 1} (α := Fin (n + 2)) objMk₁

Tactic:
objMk₁_bijective.injective

Premises used: SSet.stdSimplex.objMk₁_bijective, Function.Bijective.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
Goal:
n : ℕ
⊢ Function.Surjective.{1, u + 1} (α := Fin (n + 2)) objMk₁

Tactic:
objMk₁_bijective.surjective

Premises used: SSet.stdSimplex.objMk₁_bijective, Function.Bijective.surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
inst : X.IsStrictSegal
m : ℕ
h : m ≤ n + 1
⊢ Function.Injective (X.spine m h)

Tactic:
(spine_bijective X m).injective

Premises used: Function.Bijective.injective, SSet.Truncated.IsStrictSegal.spine_bijective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
inst : X.IsStrictSegal
m : ℕ
p : X.Path m
h : m ≤ n + 1
⊢ ∃ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ h))),
    X.spine m h x = p

Tactic:
(spine_bijective X m).surjective p

Premises used: Function.Bijective.surjective, SSet.Truncated.IsStrictSegal.spine_bijective