awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := X.obj (op (image f))) (X.map (Quiver.Hom.op (image.ι f)))
            (X.map (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (CategoryStruct.comp (Y := op (image f)) (Quiver.Hom.op (image.ι f)) (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌) y =
    (↑x : X _⦋n⦌)
rw₄ rw₅ : (↑x : X _⦋n⦌) = (↑x : X _⦋n⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage f))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op (image f)))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι f))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X.obj (op (image f))))
          y :
        (fun (X : Type u) ↦ X) (X.obj (op (image f)))) =
    (↑x : X _⦋n⦌)

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.image.fac, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
⊢ IsIso (Y := image f) (factorThruImage f)

Tactic:
have := X.isIso_of_nonDegenerate x (factorThruImage f) (y := X.map (image.ι f).op y) (by
      rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy])
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
this : IsIso (Y := image f) (factorThruImage f)
rw : Mono (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
⊢ Mono f

Tactic:
rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
this : IsIso (Y := image f) (factorThruImage f)
⊢ Mono (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
dsimp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (g hf₁ f₂).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋m₁⦌))
      y₂ =
    (↑y₁ : X _⦋m₁⦌)

Tactic:
dsimp [g]

Premises used: _private.0.SSet.unique_nonDegenerate.g
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op ≫ X.map hf₁.section_.op) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) : (a : X _⦋m₂⦌) → X _⦋n⦌) y₂ : X _⦋n⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌) x = (↑y₁ : X _⦋m₁⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y₁ : X _⦋m₁⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n⦌)) =
    (↑y₁ : X _⦋m₁⦌)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op ≫ X.map hf₁.section_.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₅ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₁.op ≫ hf₁.section_.op)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₆ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (hf₁.section_ ≫ f₁).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₇ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m₁⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₈ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (𝟙 (op ⦋m₁⦌))) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₉ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (X _⦋m₁⦌)) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₁₀ rw₁₁ : (↑y₁ : X _⦋m₁⦌) = (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)

Tactic:
rw [Functor.map_comp, comp_apply, ← hy₂, hy₁, ← comp_apply, ← Functor.map_comp, ← op_comp,
    SplitEpi.id, op_id, CategoryTheory.Functor.map_id, id_apply]

Premises used: CategoryTheory.op_comp, CategoryTheory.SplitEpi.id, CategoryTheory.id_apply, CategoryTheory.comp_apply, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (g hf₁ f₂).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋m₁⦌))
      y₂ =
    (↑y₁ : X _⦋m₁⦌)

Tactic:
have := map_g_op_y₂ hf₁ hy₁ hy₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (g hf₁ f₂).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋m₁⦌))
      y₂ =
    (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage (g hf₁ f₂)))) :
        (a : X.obj (op (image (g hf₁ f₂)))) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι (g hf₁ f₂)))) :
            (a : X _⦋m₂⦌) → X.obj (op (image (g hf₁ f₂))))
          y₂ :
        X.obj (op (image (g hf₁ f₂)))) =
    (↑y₁ : X _⦋m₁⦌)

Tactic:
rw [← image.fac (g hf₁ f₂), op_comp, Functor.map_comp, comp_apply] at this

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.image.fac, CategoryTheory.comp_apply, _private.0.SSet.unique_nonDegenerate.g, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage (g hf₁ f₂)))) :
        (a : X.obj (op (image (g hf₁ f₂)))) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι (g hf₁ f₂)))) :
            (a : X _⦋m₂⦌) → X.obj (op (image (g hf₁ f₂))))
          y₂ :
        X.obj (op (image (g hf₁ f₂)))) =
    (↑y₁ : X _⦋m₁⦌)
⊢ IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))

Tactic:
X.isIso_of_nonDegenerate y₁ (factorThruImage (g hf₁ f₂)) _ this

Premises used: CategoryTheory.Limits.factorThruImage, SSet.isIso_of_nonDegenerate, _private.0.SSet.unique_nonDegenerate.g
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage (g hf₁ f₂)))) :
        (a : X.obj (op (image (g hf₁ f₂)))) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι (g hf₁ f₂)))) :
            (a : X _⦋m₂⦌) → X.obj (op (image (g hf₁ f₂))))
          y₂ :
        X.obj (op (image (g hf₁ f₂)))) =
    (↑y₁ : X _⦋m₁⦌)
⊢ IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))

Tactic:
exact X.isIso_of_nonDegenerate y₁ (factorThruImage (g hf₁ f₂)) _ this

Premises used: CategoryTheory.Limits.factorThruImage, SSet.isIso_of_nonDegenerate, _private.0.SSet.unique_nonDegenerate.g
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
⊢ IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))

Tactic:
have := isIso_factorThruImage_g hf₁ hy₁ hy₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this : IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))
rw : Mono (CategoryStruct.comp (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂)) (image.ι (g hf₁ f₂)))
⊢ Mono (g hf₁ f₂)

Tactic:
rw [← image.fac (g hf₁ f₂)]

Premises used: CategoryTheory.Limits.image.fac, _private.0.SSet.unique_nonDegenerate.g
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this : IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))
⊢ Mono (CategoryStruct.comp (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂)) (image.ι (g hf₁ f₂)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
⊢ m₁ ≤ m₂

Tactic:
have := isIso_factorThruImage_g hf₁ hy₁ hy₂
  SimplexCategory.len_le_of_mono
    (factorThruImage (g hf₁ f₂) ≫ image.ι _)

Premises used: CategoryTheory.Limits.factorThruImage, SimplexCategory.len_le_of_mono, CategoryTheory.Limits.image.ι, _private.0.SSet.unique_nonDegenerate.g, CategoryTheory.CategoryStruct.comp, _private.0.SSet.unique_nonDegenerate.isIso_factorThruImage_g
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : X _⦋m⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
hf₁ : SplitEpi f₁
⊢ Mono (g hf₁ f₂)

Tactic:
have := mono_g hf₁ hy₁ hy₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : X _⦋m⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
hf₁ : SplitEpi f₁
this : Mono (g hf₁ f₂)
⊢ g hf₁ f₂ = 𝟙 ⦋m⦌

Tactic:
apply SimplexCategory.eq_id_of_mono

Premises used: SimplexCategory.eq_id_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst_1 : Epi f₂
y₂ : (↑(X.nonDegenerate m₂) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m₂⦌)
obtain : ∀ (hf₁ : SplitEpi f₁), m₁ = m₂
⊢ m₁ = m₂

Tactic:
obtain ⟨⟨hf₁⟩⟩ := isSplitEpi_of_epi f₁

Premises used: CategoryTheory.isSplitEpi_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst_1 : Epi f₂
y₂ : (↑(X.nonDegenerate m₂) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m₂⦌)
hf₁ : SplitEpi f₁
obtain : ∀ (hf₂ : SplitEpi f₂), m₁ = m₂
⊢ m₁ = m₂

Tactic:
obtain ⟨⟨hf₂⟩⟩ := isSplitEpi_of_epi f₂

Premises used: CategoryTheory.isSplitEpi_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst_1 : Epi f₂
y₂ : (↑(X.nonDegenerate m₂) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m₂⦌)
hf₁ : SplitEpi f₁
hf₂ : SplitEpi f₂
⊢ m₁ = m₂

Tactic:
le_antisymm (le hf₁ hy₁ hy₂) (le hf₂ hy₂ hy₁)

Premises used: le_antisymm, _private.0.SSet.unique_nonDegenerate.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst_1 : Epi f₂
y₂ : (↑(X.nonDegenerate m₂) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m₂⦌)
hf₁ : SplitEpi f₁
hf₂ : SplitEpi f₂
⊢ m₁ = m₂

Tactic:
exact le_antisymm (le hf₁ hy₁ hy₂) (le hf₂ hy₂ hy₁)

Premises used: le_antisymm, _private.0.SSet.unique_nonDegenerate.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
obtain : ∀ (hf₁ : SplitEpi f₁), y₁ = y₂
⊢ y₁ = y₂

Tactic:
obtain ⟨⟨hf₁⟩⟩ := isSplitEpi_of_epi f₁

Premises used: CategoryTheory.isSplitEpi_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
hf₁ : SplitEpi f₁
a : (↑y₁ : X _⦋m⦌) = (↑y₂ : X _⦋m⦌)
⊢ y₁ = y₂

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
hf₁ : SplitEpi f₁
⊢ (↑y₁ : X _⦋m⦌) = (↑y₂ : X _⦋m⦌)

Tactic:
simpa [g_eq_id hy₁ hy₂ hf₁] using (map_g_op_y₂ hf₁ hy₁ hy₂).symm

Premises used: _private.0.SSet.unique_nonDegenerate.map_g_op_y₂, _private.0.SSet.unique_nonDegenerate.g_eq_id, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
a :
  ∀ (x : Fin (⦋n⦌.len + 1)),
    Eq (α := Fin (⦋m⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
⊢ f₁ = f₂

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
this :
  ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x
obtain :
  ∀ (hf₁ : SplitEpi f₁)
    (hf₁' :
      (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
        x),
    Eq (α := Fin (⦋m⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))

Tactic:
obtain ⟨hf₁, hf₁'⟩ := this