awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ 0)
hs : orderHomOfSimplex (s₁, objMk₁ 0) ⋯ = OrderHom.id
this :
  Eq (α := Fin (p + 1 + 1)) ((orderHomOfSimplex (s₁, objMk₁ 0) ⋯ : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
⊢ Eq (α := Fin (p + 1 + 1)) ⟨(↑((s₁ : (a : Fin (p + 1 + 1)) → Fin (p + 1)) 0) : ℕ) + (↑1 : ℕ), ⋯⟩
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)

Tactic:
simp only [orderHomOfSimplex_coe,
          stdSimplex.objMk₁_of_le_castSucc (0 : Fin (p + 3)) 0 (by simp)] at this

Premises used: SSet.prodStdSimplex.orderHomOfSimplex_coe, SSet.stdSimplex.objMk₁_of_le_castSucc, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ 0)
hs : orderHomOfSimplex (s₁, objMk₁ 0) ⋯ = OrderHom.id
this :
  Eq (α := Fin (p + 1 + 1)) ⟨(↑((s₁ : (a : Fin (p + 1 + 1)) → Fin (p + 1)) 0) : ℕ) + (↑1 : ℕ), ⋯⟩
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
⊢ False

Tactic:
simp at this
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 1)
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i.castSucc.succ)
hs : orderHomOfSimplex (s₁, objMk₁ i.castSucc.succ) ⋯ = OrderHom.id
⊢ ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, objMk₁ i.castSucc.succ) hs_1

Tactic:
⟨i, nonDegenerate_ext₂ rfl rfl⟩

Premises used: SSet.prodStdSimplex.nonDegenerate_ext₂, Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 1)
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i.castSucc.succ)
hs : orderHomOfSimplex (s₁, objMk₁ i.castSucc.succ) ⋯ = OrderHom.id
⊢ ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, objMk₁ i.castSucc.succ) hs_1

Tactic:
exact ⟨i, nonDegenerate_ext₂ rfl rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ (Fin.succ (Fin.last (p + 1))))
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ = OrderHom.id
⊢ Eq (α := Fin (p + 1 + 1))
    ((orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1))
        (Fin.last (p + 1)) :
      Fin (p + 1 + 1))
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) (Fin.last (p + 1)) : Fin (p + 1 + 1))

Tactic:
have := DFunLike.congr_fun hs (Fin.last _)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ (Fin.succ (Fin.last (p + 1))))
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ = OrderHom.id
this :
  Eq (α := Fin (p + 1 + 1))
    ((orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1))
        (Fin.last (p + 1)) :
      Fin (p + 1 + 1))
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) (Fin.last (p + 1)) : Fin (p + 1 + 1))
⊢ LT.lt (α := Fin (p + 1 + 1 + 1)) (Fin.castSucc (Fin.last (p + 1))) (Fin.last (p + 2))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ (Fin.succ (Fin.last (p + 1))))
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ = OrderHom.id
this :
  Eq (α := Fin (p + 1 + 1))
    ((orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1))
        (Fin.last (p + 1)) :
      Fin (p + 1 + 1))
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) (Fin.last (p + 1)) : Fin (p + 1 + 1))
⊢ (↑((s₁ : (a : Fin (p + 1 + 1)) → Fin (p + 1)) (Fin.last (p + 1))) : ℕ) = p + 1

Tactic:
simp only [Fin.succ_last, orderHomOfSimplex_coe,
          OrderHom.id_coe, id_eq, Fin.ext_iff, Fin.val_last,
          stdSimplex.objMk₁_of_castSucc_lt (Fin.last (p + 2))
            (Fin.last (p + 1)) (by simp),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero] at this

Premises used: Fin.ext_iff, OrderHom.id_coe, SSet.prodStdSimplex.orderHomOfSimplex_coe, SSet.stdSimplex.objMk₁_of_castSucc_lt, HAdd.hAdd, Fin.last, Fin.coe_ofNat_eq_mod, Nat.zero_mod, Fin.succ_last, add_zero, OfNat.ofNat, Fin.val_last, id_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ (Fin.succ (Fin.last (p + 1))))
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) ⋯ = OrderHom.id
this : (↑((s₁ : (a : Fin (p + 1 + 1)) → Fin (p + 1)) (Fin.last (p + 1))) : ℕ) = p + 1
⊢ ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) hs_1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
⊢ Eq.{u_1 + 1} (α := Δ[p] _⦋p + 1⦌)
    ((↑((nonDegenerateEquiv₁ : (a : Fin (p + 1)) → (↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)) : Type u_1)) i) :
          Δ[p] _⦋p + 1⦌ ⊗ Δ[1] _⦋p + 1⦌).1 :
      Δ[p] _⦋p + 1⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
⊢ (↑((nonDegenerateEquiv₁ : (a : Fin (p + 1)) → (↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)) : Type u_1)) i) :
        Δ[p] _⦋p + 1⦌ ⊗ Δ[1] _⦋p + 1⦌).2 =
    stdSimplex.objMk₁ i.castSucc.succ

Tactic:
rfl

Premises used: Fin.succ, SSet.stdSimplex.objMk₁, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
h₀ :
  ι₁ S T ≫
      CategoryStruct.comp (Y :=
        Functor.PushoutObjObj.pt (F := curriedTensor SSet)
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom))
        (Iso.hom ⋯.isoPushout)
        (Functor.PushoutObjObj.ι
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom)) =
    ι₁ S T ≫ (S.unionProd T).ι ≫ Iso.hom (Iso.refl (tensorObj (𝒞 := Functor.category) X Y))
h₁ :
  ι₂ S T ≫
      CategoryStruct.comp (Y :=
        Functor.PushoutObjObj.pt (F := curriedTensor SSet)
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom))
        (Iso.hom ⋯.isoPushout)
        (Functor.PushoutObjObj.ι
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom)) =
    ι₂ S T ≫ (S.unionProd T).ι ≫ Iso.hom (Iso.refl (tensorObj (𝒞 := Functor.category) X Y))
⊢ CategoryStruct.comp (Y :=
      Functor.PushoutObjObj.pt (F := curriedTensor SSet)
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom))
      (Iso.hom ⋯.isoPushout)
      (Functor.PushoutObjObj.ι
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom)) =
    (S.unionProd T).ι ≫ Iso.hom (Iso.refl (tensorObj (𝒞 := Functor.category) X Y))

Tactic:
apply (unionProd.isPushout S T).hom_ext

Premises used: SSet.Subcomplex.unionProd.isPushout, CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₁ S T ≫
      CategoryStruct.comp (Y :=
        Functor.PushoutObjObj.pt (F := curriedTensor SSet)
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom))
        (Iso.hom ⋯.isoPushout)
        (Functor.PushoutObjObj.ι
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom)) =
    ι₁ S T ≫ (S.unionProd T).ι ≫ Iso.hom (Iso.refl (tensorObj (𝒞 := Functor.category) X Y))

Tactic:
simp [Functor.PushoutObjObj.ofHasPushout, Functor.PushoutObjObj.ι]

Premises used: CategoryTheory.Functor.PushoutObjObj.ofHasPushout, CategoryTheory.Functor.PushoutObjObj.ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₂ S T ≫
      CategoryStruct.comp (Y :=
        Functor.PushoutObjObj.pt (F := curriedTensor SSet)
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom))
        (Iso.hom ⋯.isoPushout)
        (Functor.PushoutObjObj.ι
          (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom)) =
    ι₂ S T ≫ (S.unionProd T).ι ≫ Iso.hom (Iso.refl (tensorObj (𝒞 := Functor.category) X Y))

Tactic:
simp [Functor.PushoutObjObj.ofHasPushout, Functor.PushoutObjObj.ι]

Premises used: CategoryTheory.Functor.PushoutObjObj.ofHasPushout, CategoryTheory.Functor.PushoutObjObj.ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi
Goal:
⊢ IsRegularEpiCategory SSet

Tactic:
inferInstanceAs (IsRegularEpiCategory (_ ⥤ _))

Premises used: _private.0.SSet.instIsRegularEpiCategory._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
n : SimplexCategoryᵒᵖ
a : X.obj n
ha : a ∈ A.obj n
⊢ Eq (α := (fun (X : Type u) ↦ X) (Y.obj n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.map.app n) :
          (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
        a :
      (fun (X : Type u) ↦ X) (Y.obj n))
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app n) :
              (a : (fun (X : Type u) ↦ X) (A.toSSet.obj n)) → (fun (X : Type u) ↦ X) (B.toSSet.obj n))
            (Subtype.mk (p := fun (x : X.obj n) ↦ x ∈ A.obj n) a ha)) :
        Y.obj n) :
      Y.obj n)

Tactic:
ConcreteCategory.congr_hom (congr_app f.comm n) ⟨a, ha⟩

Premises used: SSet.RelativeMorphism.comm, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
n : SimplexCategoryᵒᵖ
a : (↑(A.obj n) : Type u)
⊢ Eq (α := (fun (X : Type u) ↦ X) (Y.obj n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.map.app n) :
          (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
        (↑a : X.obj n) :
      (fun (X : Type u) ↦ X) (Y.obj n))
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app n) :
              (a : (fun (X : Type u) ↦ X) (A.toSSet.obj n)) → (fun (X : Type u) ↦ X) (B.toSSet.obj n))
            a) :
        Y.obj n) :
      Y.obj n)

Tactic:
map_eq_of_mem _ _ _

Premises used: SSet.RelativeMorphism.map_eq_of_mem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
n : SimplexCategoryᵒᵖ
a : X.obj n
ha : a ∈ A.obj n
⊢ Eq (α := (fun (X : Type u) ↦ X) (Y.obj n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.map.app n) :
          (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
        (↑(Subtype.mk (p := fun (x : X.obj n) ↦ x ∈ A.obj n) a ha) : X.obj n) :
      (fun (X : Type u) ↦ X) (Y.obj n))
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app n) :
              (a : (fun (X : Type u) ↦ X) (A.toSSet.obj n)) → (fun (X : Type u) ↦ X) (B.toSSet.obj n))
            (Subtype.mk (p := fun (x : X.obj n) ↦ x ∈ A.obj n) a ha)) :
        Y.obj n) :
      Y.obj n)

Tactic:
have := f.map_coe ⟨a, ha⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
n : SimplexCategoryᵒᵖ
a : X.obj n
ha : a ∈ A.obj n
this :
  Eq (α := (fun (X : Type u) ↦ X) (Y.obj n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.map.app n) :
          (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
        (↑(Subtype.mk (p := fun (x : X.obj n) ↦ x ∈ A.obj n) a ha) : X.obj n) :
      (fun (X : Type u) ↦ X) (Y.obj n))
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app n) :
              (a : (fun (X : Type u) ↦ X) (A.toSSet.obj n)) → (fun (X : Type u) ↦ X) (B.toSSet.obj n))
            (Subtype.mk (p := fun (x : X.obj n) ↦ x ∈ A.obj n) a ha)) :
        Y.obj n) :
      Y.obj n)
⊢ Membership.mem (α := Y.obj n) (B.obj n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.map.app n) :
          (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
        a :
      (fun (X : Type u) ↦ X) (Y.obj n))

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
⊢ A ≤ B.preimage f.map

Tactic:
simpa only [← Subcomplex.image_le_iff] using f.image_le

Premises used: SSet.RelativeMorphism.image_le, SSet.Subcomplex.image_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f g : RelativeMorphism A B φ
h : f.Homotopy g
⊢ f.homotopyClass = g.homotopyClass

Tactic:
Quot.sound ⟨h⟩

Premises used: Quot.sound, SSet.RelativeMorphism.homotopyClass, SSet.RelativeMorphism.HomotopyClass, Nonempty.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
x : HomotopyClass A B φ
⊢ ∃ (f : RelativeMorphism A B φ), f.homotopyClass = x

Tactic:
Quot.mk_surjective x

Premises used: SSet.RelativeMorphism.homotopyClass, SSet.RelativeMorphism.HomotopyClass, Quot.mk_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
h : f.Homotopy g
f' : RelativeMorphism B C ψ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ h.h ≫ f'.map = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι

Tactic:
simp [h.rel_assoc, ← fac]

Premises used: SSet.RelativeMorphism.Homotopy.rel_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f_1 g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
rw : A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ (φ ≫ ψ) ≫ C.ι
rw₁ : A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι
rw₂ : (A.ι ≫ f.map) ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι
rw₃ : (φ ≫ B.ι) ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι
rw₄ : φ ▷ Δ[1] ≫ B.ι ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι
rw₅ :
  Eq (α := tensorObj (𝒞 := Functor.category) A.toSSet Δ[1] ⟶ Z) (φ ▷ Δ[1] ≫ fst B.toSSet Δ[1] ≫ ψ ≫ C.ι)
    (fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι)
rw₆ rw₇ :
  Eq (α := tensorObj (𝒞 := Functor.category) A.toSSet Δ[1] ⟶ Z) (fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι)
    (fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι)
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι

Tactic:
rw [← fac, Category.assoc, ← comp_whiskerRight_assoc, f.comm,
      comp_whiskerRight_assoc, h.rel, whiskerRight_fst_assoc]

Premises used: CategoryTheory.Category.assoc, SSet.RelativeMorphism.comm, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, SSet.RelativeMorphism.Homotopy.rel, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f : RelativeMorphism A B φ
f' : RelativeMorphism B C ψ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ f.homotopyClass.postcomp f' fac = (f.comp f' fac).homotopyClass

Tactic:
rfl

Premises used: SSet.RelativeMorphism.HomotopyClass.postcomp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
Goal:
X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f : RelativeMorphism A B φ
f' : RelativeMorphism B C ψ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ f'.homotopyClass.precomp f fac = (f.comp f' fac).homotopyClass

Tactic:
rfl

Premises used: SSet.RelativeMorphism.HomotopyClass.precomp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
⊢ ∃ (n : ℕ) (x : X _⦋n⦌), s = { dim := n, simplex := x }

Tactic:
⟨s.dim, s.simplex, rfl⟩

Premises used: SSet.S.simplex, SSet.S.dim, Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s t : X.S
h : s = t
⊢ s.dim = t.dim

Tactic:
congr_arg dim h

Premises used: congr_arg, SSet.S.dim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
h : { dim := n, simplex := x : X.S } = { dim := m, simplex := y }
⊢ n = m

Tactic:
dim_eq_of_eq h

Premises used: SSet.S.dim_eq_of_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ X _⦋s.dim⦌ = X _⦋d⦌

Tactic:
simp only [hd]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
d : ℕ
hd : s.dim = d
obtain :
  ∀ (d_1 : ℕ) (w : X _⦋d_1⦌) (hd : { dim := d_1, simplex := w : X.S }.dim = d),
    { dim := d_1, simplex := w : X.S }.cast hd = { dim := d_1, simplex := w }
⊢ s.cast hd = s

Tactic:
obtain ⟨d, _, rfl⟩ := s.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
d_1 d : ℕ
w : X _⦋d⦌
hd : { dim := d, simplex := w : X.S }.dim = d_1
obtain : { dim := d, simplex := w : X.S }.cast ⋯ = { dim := d, simplex := w }
⊢ { dim := d, simplex := w : X.S }.cast hd = { dim := d, simplex := w }

Tactic:
obtain rfl := hd

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
d : ℕ
w : X _⦋d⦌
⊢ { dim := d, simplex := w : X.S }.cast ⋯ = { dim := d, simplex := w }

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
⊢ (s.cast ⋯).simplex = s.simplex

Tactic:
rfl

Premises used: cast, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
⊢ ∃ (h : s.dim = s.dim), (s.cast h).simplex = s.simplex

Tactic:
⟨rfl, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
⊢ ∃ (h : s.dim = s.dim), (s.cast h).simplex = s.simplex

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s t : X.S
h : ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex
h₁ : s.dim = t.dim
h₂ : (s.cast h₁).simplex = t.simplex
obtain :
  ∀ (w : ℕ) (w_1 : X _⦋w⦌),
    (∃ (h : { dim := w, simplex := w_1 : X.S }.dim = t.dim),
        ({ dim := w, simplex := w_1 : X.S }.cast h).simplex = t.simplex) →
      ∀ (h₁ : { dim := w, simplex := w_1 : X.S }.dim = t.dim)
        (h₂ : ({ dim := w, simplex := w_1 : X.S }.cast h₁).simplex = t.simplex), { dim := w, simplex := w_1 : X.S } = t
⊢ s = t

Tactic:
obtain ⟨_, _, rfl⟩ := s.mk_surjective

Premises used: SSet.S.mk_surjective, rfl