awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
hff' :
  LE.le (α :=
    (fun (X : SimplexCategory) ↦ Fin (X.len + 1))
      (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₁, property := hΔ₁ })) →
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
      0)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
      0)
⊢ Zigzag
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋0⦌ ⋯,
      right := { as := PUnit.unit },
      hom :=
        ⦋0⦌.const (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} })
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
            0) }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
      right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }

Tactic:
apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0

Premises used: SimplexCategory.Truncated.Hom.tr, CategoryTheory.CostructuredArrow.homMk, SimplexCategory.const, SimplexCategory.mk, OfNat.ofNat, CategoryTheory.Zigzag.of_hom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
hff' :
  ¬LE.le (α :=
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1))
        (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₁, property := hΔ₁ })) →
            (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
        0)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
            (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
        0)
⊢ Zigzag
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋0⦌ ⋯,
      right := { as := PUnit.unit },
      hom :=
        ⦋0⦌.const (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} })
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f' :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₂, property := hΔ₂ })) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
            0) }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
      right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }

Tactic:
apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0

Premises used: SimplexCategory.Truncated.Hom.tr, CategoryTheory.CostructuredArrow.homMk, SimplexCategory.const, SimplexCategory.mk, OfNat.ofNat, CategoryTheory.Zigzag.of_hom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n m : ℕ
inst : NeZero n
hm : n ≤ m
⊢ n ≤ m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n m : ℕ
inst : NeZero n
hm : n ≤ m
⊢ (incl n m hm ⋙ inclusion m).Initial

Tactic:
have : (incl n m hm ⋙ inclusion m).Initial :=
    Functor.initial_of_natIso (inclCompInclusion (by lia)).symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n m : ℕ
inst : NeZero n
hm : n ≤ m
this : (incl n m hm ⋙ inclusion m).Initial
⊢ (incl n m ⋯).Initial

Tactic:
apply Functor.initial_of_comp_full_faithful _ (inclusion m)

Premises used: SimplexCategory.Truncated.inclusion, CategoryTheory.Functor.initial_of_comp_full_faithful
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
hn : ⦋n⦌.len ≤ 2
hn' : ⦋n + 1⦌.len ≤ 2
⊢ δ₂ 0 hn hn' ≫ σ₂ 0 hn' hn = 𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋n⦌ hn)

Tactic:
ObjectProperty.hom_ext _ (SimplexCategory.δ_comp_σ_self)

Premises used: CategoryTheory.ObjectProperty.hom_ext, SimplexCategory.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_1 δ₂_zero_comp_σ₂_one._proof_2 ≫
      σ₂ 1 δ₂_zero_comp_σ₂_one._proof_2 δ₂_zero_comp_σ₂_one._proof_1 =
    σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
      δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
ObjectProperty.hom_ext _ (SimplexCategory.δ_comp_σ_of_le (i := 0) (j := 0) (Fin.zero_le _))

Premises used: SimplexCategory.δ_comp_σ_of_le, Fin.zero_le, CategoryTheory.ObjectProperty.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
hn : ⦋n⦌.len ≤ 2
hn' : ⦋n + 1⦌.len ≤ 2
⊢ δ₂ 1 hn hn' ≫ σ₂ 0 hn' hn = 𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋n⦌ hn)

Tactic:
ObjectProperty.hom_ext _ (SimplexCategory.δ_comp_σ_succ)

Premises used: CategoryTheory.ObjectProperty.hom_ext, SimplexCategory.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
hn : ⦋n + 1⦌.len ≤ 2
hn' : ⦋n + 1 + 1⦌.len ≤ 2
⊢ δ₂ 1 hn hn' ≫ σ₂ 1 hn' hn =
    𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋n + 1⦌ hn)

Tactic:
ObjectProperty.hom_ext _ (SimplexCategory.δ_comp_σ_self (n := n + 1) (i := 1))

Premises used: CategoryTheory.ObjectProperty.hom_ext, SimplexCategory.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 2)) 2 (Fin.succ 1)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
⊢ LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 2 + 1)) (Fin.succ 0) 2

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
⊢ δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 =
    Hom.tr (⦋0⦌.const ⦋HAdd.hAdd (α := ℕ) 0 1⦌ 0) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 =
    Hom.tr (⦋0⦌.const ⦋HAdd.hAdd (α := ℕ) 0 1⦌ 1) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 ≫
      δ₂ 2 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1 =
    δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 ≫
      δ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K x : PreAbstractSimplicialComplex ι
h :
  Eq.{u_1 + 1} (α := Set (Finset ι)) ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) K)
    ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) x)
mk :
  ∀ (faces : Set (Finset ι)) (isRelLowerSet_faces : IsRelLowerSet faces Finset.Nonempty),
    Eq.{u_1 + 1} (α := Set (Finset ι))
        ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces)
          { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces })
        ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) x) →
      { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces : PreAbstractSimplicialComplex ι } = x
⊢ K = x

Tactic:
cases K
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x : PreAbstractSimplicialComplex ι
faces : Set (Finset ι)
isRelLowerSet_faces : IsRelLowerSet faces Finset.Nonempty
h :
  Eq.{u_1 + 1} (α := Set (Finset ι))
    ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces)
      { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces })
    ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) x)
⊢ { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces : PreAbstractSimplicialComplex ι } = x

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (PreAbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) ((⋂ K ∈ s, K.faces) ∩ {t : Finset ι | t.Nonempty}) x
hx : Membership.mem (γ := Set (Finset ι)) (⋂ K ∈ s, K.faces) x
hn : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | t.Nonempty} x
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄,
      b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) ((⋂ K ∈ s, K.faces) ∩ {t : Finset ι | t.Nonempty}) b

Tactic:
grind [IsRelLowerSet.mem_of_le, isRelLowerSet_faces, mem_iInter]

Premises used: IsRelLowerSet.mem_of_le, Set.mem_iInter, PreAbstractSimplicialComplex.isRelLowerSet_faces
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : Membership.mem (γ := Set (Finset β)) ((fun (s : Finset α) ↦ Finset.image f s) '' K.faces) x
⊢ ∃ x_1 ∈ K.faces, Finset.image f x_1 = x

Tactic:
simp only [Set.mem_image] at h ⊢

Premises used: Set.mem_image
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : ∃ x_1 ∈ K.faces, Finset.image f x_1 = x
obtain :
  ∀ (s' : Finset α) (hs' : s' ∈ K.faces),
    (Finset.image f s').Nonempty ∧
      ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ≤ x → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b

Tactic:
obtain ⟨s', hs', rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
left : (Finset.image f s').Nonempty
right : ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
⊢ (Finset.image f s').Nonempty ∧
    ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty

Tactic:
Finset.image_nonempty.mpr (K.isRelLowerSet_faces hs').1

Premises used: Iff.mpr, Finset.image_nonempty, And.left, PreAbstractSimplicialComplex.isRelLowerSet_faces
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty

Tactic:
exact Finset.image_nonempty.mpr (K.isRelLowerSet_faces hs').1

Premises used: Iff.mpr, Finset.image_nonempty, And.left, PreAbstractSimplicialComplex.isRelLowerSet_faces
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
t : Finset β
hts : t ≤ Finset.image f s'
ht : t.Nonempty
right :
  ∀ (t' : Finset α) (ht' : t' ⊆ s') (hts : Finset.image f t' ≤ Finset.image f s') (ht : (Finset.image f t').Nonempty),
    ∃ x ∈ K.faces, Finset.image f x = Finset.image f t'
⊢ ∃ x ∈ K.faces, Finset.image f x = t

Tactic:
obtain ⟨t', ht', rfl⟩ := Finset.subset_image_iff.mp hts

Premises used: Iff.mp, Finset.subset_image_iff, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
t' : Finset α
ht' : t' ⊆ s'
hts : Finset.image f t' ≤ Finset.image f s'
ht : (Finset.image f t').Nonempty
⊢ ∃ x ∈ K.faces, Finset.image f x = Finset.image f t'

Tactic:
⟨t', (K.isRelLowerSet_faces hs').2 ht' (Finset.image_nonempty.mp ht), rfl⟩

Premises used: Finset.image_nonempty, And.right, And.intro, Exists.intro, Iff.mp, PreAbstractSimplicialComplex.isRelLowerSet_faces, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
t' : Finset α
ht' : t' ⊆ s'
hts : Finset.image f t' ≤ Finset.image f s'
ht : (Finset.image f t').Nonempty
⊢ ∃ x ∈ K.faces, Finset.image f x = Finset.image f t'

Tactic:
exact ⟨t', (K.isRelLowerSet_faces hs').2 ht' (Finset.image_nonempty.mp ht), rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
left : x.Nonempty
right :
  ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
left : Finset.Nonempty (α := ι) {v}
⊢ x.Nonempty

Tactic:
rw [hv]
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ Finset.Nonempty (α := ι) {v}

Tactic:
Finset.singleton_nonempty _

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ Finset.Nonempty (α := ι) {v}

Tactic:
exact Finset.singleton_nonempty _

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = ∅
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
(ht.ne_empty h).elim

Premises used: False.elim, Finset.Nonempty.ne_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = ∅
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
exact (ht.ne_empty h).elim

Premises used: False.elim, Finset.Nonempty.ne_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = {v}
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
⟨v, h⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = {v}
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t

Tactic:
exact ⟨v, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
⊢ t = ∅ ∨ t = {v}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
        | inl h => exact (ht.ne_empty h).elim
        | inr h => exact ⟨v, h⟩

Premises used: Iff.mp, Finset.subset_singleton_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x x_1 : AbstractSimplicialComplex ι
h :
  Eq.{u_1 + 1} (α := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) x)
    ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) x_1)
faces : ∀ (x_2 : Finset ι), x_2 ∈ x.faces ↔ x_2 ∈ x_1.faces
⊢ x = x_1

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
x x_1 : AbstractSimplicialComplex ι
h :
  Eq.{u_1 + 1} (α := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) x)
    ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) x_1)
x_2 : Finset ι
⊢ x_2 ∈ x.faces ↔ x_2 ∈ x_1.faces

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := AbstractSimplicialComplex ι) toPreAbstractSimplicialComplex

Tactic:
fun _ _ h => AbstractSimplicialComplex.ext (congrArg PreAbstractSimplicialComplex.faces h)

Premises used: congrArg, PreAbstractSimplicialComplex.faces, AbstractSimplicialComplex.ext, Function.Injective
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K L : AbstractSimplicialComplex ι
⊢ K.toPreAbstractSimplicialComplex ≤ L.toPreAbstractSimplicialComplex ↔ K ≤ L

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
K L : AbstractSimplicialComplex ι
⊢ K.toPreAbstractSimplicialComplex < L.toPreAbstractSimplicialComplex ↔ K < L

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
left : x.Nonempty
right :
  ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} b
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} b

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
left : Finset.Nonempty (α := ι) {v}
⊢ x.Nonempty

Tactic:
rw [hv]
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
⊢ Finset.Nonempty (α := ι) {v}

Tactic:
Finset.singleton_nonempty _

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
⊢ Finset.Nonempty (α := ι) {v}

Tactic:
exact Finset.singleton_nonempty _

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = ∅
⊢ Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} t

Tactic:
(ht.ne_empty h).elim

Premises used: False.elim, Finset.Nonempty.ne_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = ∅
⊢ Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} t

Tactic:
exact (ht.ne_empty h).elim

Premises used: False.elim, Finset.Nonempty.ne_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = {v}
⊢ Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} t

Tactic:
⟨v, h⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h_1 : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
h : t = {v}
⊢ Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} t

Tactic:
exact ⟨v, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
⊢ t = ∅ ∨ t = {v}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
            | inl h => exact (ht.ne_empty h).elim
            | inr h => exact ⟨v, h⟩

Premises used: Iff.mp, Finset.subset_singleton_iff