awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
h :
  ∀ (x_3 : X.obj x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map x_2 ≫
            ↾fun (x : X.obj x_1) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
                  (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) →
                    (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x_1))))
                y))
        x_3 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x_4 : X.obj x) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
                  (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) →
                    (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x))))
                y) ≫
            Y.map x_2))
        x_3
⊢ (X.map x_2 ≫
      ↾fun (x : X.obj x_1) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x_1))))
          y) =
    (↾fun (x_3 : X.obj x) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x))))
          y) ≫
      Y.map x_2

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj x
h :
  Eq (α := Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map x_2) : (a : Y.obj x) → Y.obj x_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
              (a : Y _⦋0⦌) → Y.obj x)
            y :
          Y.obj x) :
      Y.obj x_1)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map x_2 ≫
          ↾fun (x : X.obj x_1) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) →
                  (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x_1))))
              y))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_4 : X.obj x) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x))))
              y) ≫
          Y.map x_2))
      x_3

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj x
h :
  Eq (α := Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0) ≫ x_2)) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)
⊢ Eq (α := Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map x_2) : (a : Y.obj x) → Y.obj x_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
              (a : Y _⦋0⦌) → Y.obj x)
            y :
          Y.obj x) :
      Y.obj x_1)

Tactic:
rw [← CategoryTheory.comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj x
⊢ Eq (α := Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0) ≫ x_2)) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
X Y Z : SSet
f : X ⟶ Y
z : Z _⦋0⦌
⊢ f ≫ const z = const z

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, SSet.const, TypeCat.Fun.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
X Y : Truncated n
f g : X ⟶ Y
w : ∀ (n_1 : (SimplexCategory.Truncated n)ᵒᵖ), f.app n_1 = g.app n_1
⊢ f = g

Tactic:
NatTrans.ext (funext w)

Premises used: CategoryTheory.NatTrans.ext, funext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
X : Truncated n
d : (SimplexCategory.Truncated n)ᵒᵖ
⊢ NatTrans.app (𝟙 X) d = 𝟙 (X.obj d)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
X Y Z : Truncated n
f : X ⟶ Y
g : Y ⟶ Z
d : (SimplexCategory.Truncated n)ᵒᵖ
⊢ (f ≫ g).app d = f.app d ≫ g.app d

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
⊢ IsIso (coskAdj n).counit

Tactic:
SimplicialObject.Truncated.cosk_reflective n

Premises used: CategoryTheory.SimplicialObject.Truncated.cosk_reflective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
⊢ IsIso (skAdj n).unit

Tactic:
SimplicialObject.Truncated.sk_coreflective n

Premises used: CategoryTheory.SimplicialObject.Truncated.sk_coreflective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
⊢ (Truncated.cosk n).Full

Tactic:
SimplicialObject.Truncated.cosk.full n

Premises used: CategoryTheory.SimplicialObject.Truncated.cosk.full
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
⊢ (Truncated.cosk n).Faithful

Tactic:
SimplicialObject.Truncated.cosk.faithful n

Premises used: CategoryTheory.SimplicialObject.Truncated.cosk.faithful
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
⊢ (Truncated.sk n).Full

Tactic:
SimplicialObject.Truncated.sk.full n

Premises used: CategoryTheory.SimplicialObject.Truncated.sk.full
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
n : ℕ
⊢ (Truncated.sk n).Faithful

Tactic:
SimplicialObject.Truncated.sk.faithful n

Premises used: CategoryTheory.SimplicialObject.Truncated.sk.faithful
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
x : S _⦋n + 2⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j.succ) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))

Tactic:
congr_hom (S.δ_comp_δ H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
x : S _⦋n + 2⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S (j.pred ⋯)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))

Tactic:
congr_hom (S.δ_comp_δ' H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
x : S _⦋n + 2⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S (i.castLT ⋯)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j.succ) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))

Tactic:
congr_hom (S.δ_comp_δ'' H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 2⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.succ) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))

Tactic:
congr_hom S.δ_comp_δ_self x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
x : S _⦋n + 2⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.succ) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n⦌))

Tactic:
congr_hom (S.δ_comp_δ_self' H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
x : S _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.castSucc) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j.succ) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))

Tactic:
congr_hom (S.δ_comp_σ_of_le H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.castSucc) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          x :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) =
    x

Tactic:
congr_hom S.δ_comp_σ_self x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          x :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) =
    x

Tactic:
congr_hom (S.δ_comp_σ_self' H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.succ) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          x :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) =
    x

Tactic:
congr_hom S.δ_comp_σ_succ x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          x :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) =
    x

Tactic:
congr_hom (S.δ_comp_σ_succ' H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
x : S _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i.succ) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))

Tactic:
congr_hom (S.δ_comp_σ_of_gt H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
x : S _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S (j.castLT ⋯)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S (i.pred ⋯)) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))

Tactic:
congr_hom (S.δ_comp_σ_of_gt' H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S : SSet
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
x : S _⦋n⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i.castSucc) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S j.succ) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌))

Tactic:
congr_hom (S.σ_comp_σ H) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
change :
  Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ T i) :
          (a : (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))

Tactic:
change (S.δ i ≫ f.app (op ⦋n⦌)) x = (f.app (op ⦋n + 1⦌) ≫ T.δ i) x

Premises used: CategoryTheory.ConcreteCategory.hom, HAdd.hAdd, SimplexCategory.mk, Opposite.op, CategoryTheory.CategoryStruct.comp, CategoryTheory.SimplicialObject.δ, OfNat.ofNat, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))

Tactic:
congr_hom (SimplicialObject.δ_naturality f i) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))

Tactic:
exact congr_hom (SimplicialObject.δ_naturality f i) x

Premises used: CategoryTheory.SimplicialObject.δ_naturality, CategoryTheory.ConcreteCategory.congr_hom