awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).arrow i =
    Path.arrow
      {
        vertex := fun (i : Fin (n + 1)) ↦
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app
                  (StructuredArrow.mk (Y :=
                    op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        lift._proof_2))
                    (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
              (a : s.pt) → X _⦋0⦌)
            x,
        arrow := fun (i : Fin n) ↦
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app
                  (StructuredArrow.mk (Y :=
                    op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                        lift._proof_4))
                    (mkOfLe i.castSucc i.succ ⋯).op)) :
              (a : s.pt) → X _⦋1⦌)
            x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
exact ConcreteCategory.congr_hom (hm (.mk (Y := op ⦋1⦌₂)
        (.op (mkOfLe _ _ (Fin.castSucc_le_succ i))))) x

Premises used: Fin.castSucc_le_succ, Quiver.Hom.op, SimplexCategory.mkOfLe, CategoryTheory.StructuredArrow.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X : SSet
sx : X.StrictSegal
⊢ IsRightKanExtension (C := (SimplexCategory.Truncated 2)ᵒᵖ) X (L := Functor.op (inclusion 2))
    (𝟙 (Functor.op (inclusion 2) ⋙ X))

Tactic:
RightExtension.IsPointwiseRightKanExtension.isRightKanExtension
    sx.isPointwiseRightKanExtension

Premises used: CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension, SSet.StrictSegal.isPointwiseRightKanExtension
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X : SSet
sx : X.StrictSegal
inst : X.IsStrictSegal
⊢ SimplicialObject.IsCoskeletal X 2

Tactic:
isCoskeletal <| ofIsStrictSegal X

Premises used: SSet.StrictSegal.isCoskeletal, SSet.StrictSegal.ofIsStrictSegal
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
C : Type u
inst : Category.{v, u} C
⊢ SimplicialObject.IsCoskeletal (nerve.{v, u} C) 2

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
Goal:
X : Cat
⊢ Truncated.IsStrictSegal (n := 1) (obj (truncation 2) (nerve.{v, u} (↑X : Type u)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
h : ∀ (x : X _⦋0⦌), Membership.mem (γ := Set (X _⦋0⦌)) (X.degenerate 0) x ↔ Membership.mem (γ := Set (X _⦋0⦌)) ∅ x
⊢ Eq (α := Set (X _⦋0⦌)) (X.degenerate 0) ∅

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
x : X _⦋0⦌
h : x ∉ X.degenerate 0
⊢ Membership.mem (γ := Set (X _⦋0⦌)) (X.degenerate 0) x ↔ Membership.mem (γ := Set (X _⦋0⦌)) ∅ x

Tactic:
simp only [Set.mem_empty_iff_false, iff_false]

Premises used: iff_false, Set.mem_empty_iff_false
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
x : X _⦋0⦌
m : ℕ
hm : m < 0
h :
  ∃ (f : ⦋0⦌ ⟶ ⦋m⦌),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋0⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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 _⦋0⦌)))
      x
⊢ False

Tactic:
simp at hm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
⊢ Eq (α := Set (X _⦋0⦌)) (X.nonDegenerate 0) Set.univ

Tactic:
simp [nonDegenerate]

Premises used: SSet.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.nonDegenerate n ↔ x ∉ X.degenerate n

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, SSet.nonDegenerate, setOf, Not
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ x ∉ X.nonDegenerate n

Tactic:
simp [nonDegenerate]

Premises used: SSet.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
i : Fin (n + 1)
x : X _⦋n⦌
⊢ n < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
mp :
  x ∈ X.degenerate n →
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        x
mpr :
  (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        x) →
    x ∈ X.degenerate n
⊢ x ∈ X.degenerate n ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (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
⊢ (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 _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x

Tactic:
rw [← image.fac f, op_comp] at hy

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.image.fac
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (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 _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x
⊢ (image f).len ≤ m

Tactic:
have : _ ≤ m := SimplexCategory.len_le_of_mono (image.ι f)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (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 _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x
this : (image f).len ≤ m
⊢ (image f).len < n

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (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 _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x
this : (image f).len ≤ m
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋(image f).len⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(image f).len⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
    x

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy :
  (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 _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    x
this : (image f).len ≤ m
⊢ ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
      x

Tactic:
exact ⟨(image f).len, by lia, factorThruImage f, inferInstance, by aesop⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
hx :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
    x
⊢ x ∈ X.degenerate n

Tactic:
⟨m, hm, f, hx⟩

Premises used: Set.Mem, setOf, Exists.intro, SSet.degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
hx :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
    x
⊢ x ∈ X.degenerate n

Tactic:
exact ⟨m, hm, f, hx⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
simp :
  (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
⊢ Membership.mem (α := X _⦋n⦌) (X.degenerate n) ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌) ↔
    Membership.mem (γ := Set (X.op _⦋n⦌)) (X.op.degenerate n) x

Tactic:
simp only [mem_degenerate_iff]

Premises used: SSet.mem_degenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x

Tactic:
exists_congr (fun m ↦ exists_congr (fun _ ↦ ?_))

Premises used: exists_congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
refine :
  ∀ m < n,
    (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
        Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
          (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
          ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
      ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
        Membership.mem (γ := Set (X.op _⦋n⦌))
          (Set.range (ι := X.op _⦋m⦌)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
          x
⊢ (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x

Tactic:
refine exists_congr (fun m ↦ exists_congr (fun _ ↦ ?_))

Premises used: exists_congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
h : m < n
mp :
  (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) →
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
mpr :
  (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x) →
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)
⊢ (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
h : m < n
mp :
  ∀ (x : X _⦋n⦌),
    (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
        Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
          (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
          ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌) x : X.op _⦋n⦌) :
            X _⦋n⦌)) →
      ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
        Membership.mem (α := X.op _⦋n⦌) (γ := Set (X.op _⦋n⦌))
          (Set.range (ι := X.op _⦋m⦌)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
          ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌) x : X.op _⦋n⦌)
⊢ (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) →
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x

Tactic:
obtain ⟨x, rfl⟩ := opObjEquiv.symm.surjective x

Premises used: SSet.opObjEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
h : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
⊢ Eq (α := X.op _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map (SimplexCategory.rev.map f).op) : (a : X.op _⦋m⦌) → X.op _⦋n⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋m⦌) → X.op _⦋m⦌) y : X.op _⦋m⦌) :
      X.op _⦋n⦌)
    ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) y : X _⦋n⦌) :
      X.op _⦋n⦌)

Tactic:
simp [op_map]

Premises used: SSet.op_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
h : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
⊢ ∃ (f_1 : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f_1),
    Membership.mem (α := X.op _⦋n⦌) (γ := Set (X.op _⦋n⦌))
      (Set.range (ι := X.op _⦋m⦌)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f_1.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
      ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) y : X _⦋n⦌) :
        X.op _⦋n⦌)

Tactic:
exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv.symm y, by simp [op_map]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
h : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X.op _⦋m⦌
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.rev.map f).op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((opObjEquiv : (a : X.op _⦋m⦌) → X _⦋m⦌) y : X _⦋m⦌) :
      X _⦋n⦌)
    ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋m⦌) → X.op _⦋n⦌) y : X.op _⦋n⦌) :
      X _⦋n⦌)

Tactic:
simp [op_map]

Premises used: SSet.op_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ Membership.mem (α := X _⦋n⦌) (X.nonDegenerate n) ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌) ↔
    Membership.mem (γ := Set (X.op _⦋n⦌)) (X.op.nonDegenerate n) x

Tactic:
simp only [mem_nonDegenerate_iff_notMem_degenerate,
    opObjEquiv_mem_degenerate_iff]

Premises used: SSet.opObjEquiv_mem_degenerate_iff, SSet.mem_nonDegenerate_iff_notMem_degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
h :
  ∀ (x : X _⦋n + 1⦌),
    Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x ↔
      Membership.mem (γ := Set (X _⦋n + 1⦌))
        (⋃ (i : Fin (n + 1)),
          Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
        x
⊢ Eq (α := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
h :
  Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x →
    Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x
h₁ :
  Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x →
    Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x ↔
    Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
⊢ ∃ (m : ℕ) (_ : m < n + 1) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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 + 1⦌)))
      x

Tactic:
rw [mem_degenerate_iff] at hx

Premises used: SSet.mem_degenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx :
  ∃ (m : ℕ) (_ : m < n + 1) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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 + 1⦌)))
      x
h :
  ∀ (m : ℕ) (hm : m < n + 1) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (hf : Epi f) (y : X _⦋m⦌),
    Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 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 + 1⦌))
          y :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x

Tactic:
obtain ⟨m, hm, f, hf, y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf_1 : Epi f
y : X _⦋m⦌
hf :
  Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (⦋m⦌.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋m⦌.len + 1))
⊢ Mono f

Tactic:
rw [← SimplexCategory.mono_iff_injective] at hf

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf_1 : Epi f
y : X _⦋m⦌
hf : Mono f
⊢ n + 1 ≤ m

Tactic:
have := SimplexCategory.le_of_mono f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf_1 : Epi f
y : X _⦋m⦌
hf : Mono f
this : n + 1 ≤ m
⊢ False

Tactic:
lia