awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (hypothesis)
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)
⊢ False
have this₁ : Eq (α := Fin (p + 1 + 1)) ⟨(↑((s₁ : (a : Fin (p + 1 + 1)) → Fin (p + 1)) 0) : ℕ) + (↑1 : ℕ), sorry⟩
  ((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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 1 + 2)
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i)
hs : orderHomOfSimplex (s₁, objMk₁ i) ⋯ = 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) hs_1
have refine_2 : ∀ (i : Fin (p + 2))
  (hs :
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i.succ))
  (hs_2 : orderHomOfSimplex (s₁, objMk₁ i.succ) sorry = 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)
              sorry :
            { 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.succ) hs
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by
        rintro rfl
        have := DFunLike.congr_fun hs 0
        simp only [orderHomOfSimplex_coe,
          stdSimplex.objMk₁_of_le_castSucc (0 : Fin (p + 3)) 0 (by simp)] at this
        simp at this)
Cleared hypotheses: i, hs_1, hs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 2)
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i.succ)
hs : orderHomOfSimplex (s₁, objMk₁ i.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.succ) hs_1
have refine_2 : ∀ (i : Fin (p + 1))
  (hs :
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i.castSucc.succ))
  (hs_2 : orderHomOfSimplex (s₁, objMk₁ i.castSucc.succ) sorry = 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)
              sorry :
            { 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
Tactic: obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
Cleared hypotheses: i, hs_1, hs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (hypothesis)
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
⊢ ∃ (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
have this : Eq (α := Fin (p + 1 + 1))
  ((orderHomOfSimplex (s₁, objMk₁ (Fin.succ (Fin.last (p + 1)))) sorry : (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 _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (hypothesis)
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))
⊢ ∃ (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
have this₁ : (↑((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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ 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))
have 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 sorry.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: apply (unionProd.isPushout S T).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct (goal)
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))
⊢ 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))
have 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 sorry.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: apply (unionProd.isPushout S T).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (hypothesis)
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
⊢ 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))
have 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)
Tactic: have := f.map_coe ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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 : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw : 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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.ι
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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.ι
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw₂ : (A.ι ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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.ι
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw₃ : (φ ≫ B.ι) ▷ Δ[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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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.ι
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw₄ : φ ▷ Δ[1] ≫ B.ι ▷ Δ[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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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.ι
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw₅ : Eq (α := tensorObj (𝒞 := Functor.category) A.toSSet Δ[1] ⟶ Z) (φ ▷ Δ[1] ≫ fst B.toSSet Δ[1] ≫ ψ ≫ C.ι)
  (fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι)
Tactic: rw [← fac, Category.assoc, ← comp_whiskerRight_assoc, f.comm,
      comp_whiskerRight_assoc, h.rel, whiskerRight_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism (goal)
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.ι)
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι
have rw₆ : Eq (α := tensorObj (𝒞 := Functor.category) A.toSSet Δ[1] ⟶ Z) (fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι)
  (fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι)
Tactic: rw [← fac, Category.assoc, ← comp_whiskerRight_assoc, f.comm,
      comp_whiskerRight_assoc, h.rel, whiskerRight_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s
have 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 }
Tactic: obtain ⟨d, _, rfl⟩ := s.mk_surjective
Cleared hypotheses: s, hd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
d_1 d : ℕ
w : X _⦋d⦌
hd : { dim := d, simplex := w : X.S }.dim = d_1
⊢ { dim := d, simplex := w : X.S }.cast hd = { dim := d, simplex := w }
have obtain : { dim := d, simplex := w : X.S }.cast sorry = { dim := d, simplex := w }
Tactic: obtain rfl := hd
Cleared hypotheses: d_1, hd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
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
⊢ s = t
have 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
Tactic: obtain ⟨_, _, rfl⟩ := s.mk_surjective
Cleared hypotheses: s, h, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
t : X.S
w : ℕ
w_1 : X _⦋w⦌
h :
  ∃ (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
have obtain : ∀ (w_2 : ℕ) (w_3 : X _⦋w_2⦌),
  (∃ (h : { dim := w, simplex := w_1 : X.S }.dim = { dim := w_2, simplex := w_3 : X.S }.dim),
      ({ dim := w, simplex := w_1 : X.S }.cast h).simplex = { dim := w_2, simplex := w_3 }.simplex) →
    ∀ (h₁ : { dim := w, simplex := w_1 : X.S }.dim = { dim := w_2, simplex := w_3 : X.S }.dim)
      (h₂ : ({ dim := w, simplex := w_1 : X.S }.cast h₁).simplex = { dim := w_2, simplex := w_3 }.simplex),
      { dim := w, simplex := w_1 : X.S } = { dim := w_2, simplex := w_3 }
Tactic: obtain ⟨_, _, rfl⟩ := t.mk_surjective
Cleared hypotheses: t, h, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ (s.cast hd).subcomplex = s.subcomplex
have rw : s.subcomplex = s.subcomplex
Tactic: rw [cast_eq_self]