awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.σ₀Iter i hi).op ≫ (SimplexCategory.σ j).op) = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
rw₁ : X.map (SimplexCategory.σ j ≫ SimplexCategory.σ₀Iter i hi).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
rw₂ rw₃ : X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
⊢ X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]

Premises used: CategoryTheory.op_comp, SimplexCategory.σ_σ₀Iter, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + i = m
hj : (↑j : ℕ) = (↑j' : ℕ) + i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ j' ≫ X.σ₀Iter i ⋯

Tactic:
simp [σ, σ₀Iter, ← Functor.map_comp, ← op_comp,
    SimplexCategory.σ_σ₀Iter' i j j']

Premises used: CategoryTheory.op_comp, SimplexCategory.σ_σ₀Iter', CategoryTheory.Functor.map_comp, CategoryTheory.SimplicialObject.σ₀Iter, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
hi : n + i = m
⊢ X.σ₀Iter i hi ≫ X.δ₀Iter i hi = 𝟙 (X _⦋n⦌)

Tactic:
simp [σ₀Iter, δ₀Iter, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.SimplicialObject.δ₀Iter, CategoryTheory.Functor.map_comp, CategoryTheory.SimplicialObject.σ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
hi : n + i = m
⊢ Mono (X.σ₀Iter i hi)

Tactic:
mono_of_mono_fac (X.σ₀Iter_δ₀Iter i hi)

Premises used: CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
hi : n + i = m
⊢ Epi (X.δ₀Iter i hi)

Tactic:
epi_of_epi_fac (X.σ₀Iter_δ₀Iter i hi)

Premises used: CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter, CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Y : Augmented.{v_1, u_1} C
n m i : ℕ
hi : n + i = m
⊢ Y.left.δ₀Iter i hi ≫ Y.hom.app (op ⦋n⦌) = Y.hom.app (op ⦋m⦌)

Tactic:
simpa using Y.hom.naturality (SimplexCategory.δ₀Iter i hi).op

Premises used: Quiver.Hom.op, CategoryTheory.Comma.hom, CategoryTheory.NatTrans.naturality, SimplexCategory.δ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Y : Augmented.{v_1, u_1} C
n m i : ℕ
hi : n + i = m
⊢ Y.left.σ₀Iter i hi ≫ Y.hom.app (op ⦋m⦌) = Y.hom.app (op ⦋n⦌)

Tactic:
simpa using Y.hom.naturality (SimplexCategory.σ₀Iter i hi).op

Premises used: Quiver.Hom.op, SimplexCategory.σ₀Iter, CategoryTheory.Comma.hom, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
x y : (↑(X.nonDegenerate n) : Type u)
h :
  Eq.{u + 1} (α := X.N) ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) x)
    ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) y)
⊢ ∃ (h :
    S.dim.{u} (X := X) (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) x)) =
      S.dim.{u} (X := X) (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) y))),
    (S.cast (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) x)) h).simplex =
      S.simplex (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) y))

Tactic:
rw [N.ext_iff, S.ext_iff'] at h

Premises used: SSet.N.ext_iff, SSet.S.ext_iff'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
x y : (↑(X.nonDegenerate n) : Type u)
h :
  ∃ (h :
    S.dim.{u} (X := X) (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) x)) =
      S.dim.{u} (X := X) (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) y))),
    (S.cast (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) x)) h).simplex =
      S.simplex (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) ⋯) y))
⊢ x = y

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
⊢ ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)

Tactic:
have (i : Fin d) : Finite (X.nonDegenerate i) := h i.1 i.2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
⊢ Finite.{u + 1} X.N

Tactic:
Finite.of_surjective (α := Σ (i : Fin d), X.nonDegenerate i)
      (f := fun ⟨i, x⟩ ↦ N.mk _ x.property) (fun x ↦ ?_)

Premises used: SSet.N.mk, SSet.N, _private.0.SSet.finite_of_hasDimensionLT.match_1, Subtype.val, Finite.of_surjective, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
refine :
  ∀ (x : X.N),
    ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
      (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
            (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
              | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
              X.N))
          a =
        x
⊢ Finite.{u + 1} X.N

Tactic:
refine Finite.of_surjective (α := Σ (i : Fin d), X.nonDegenerate i)
      (f := fun ⟨i, x⟩ ↦ N.mk _ x.property) (fun x ↦ ?_)

Premises used: Finite.of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
x : X.N
pos :
  ∀ (hj : x.dim < d),
    ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
      (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
            (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
              | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
              X.N))
          a =
        x
neg :
  ∀ (hj : ¬x.dim < d),
    ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
      (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
            (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
              | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
              X.N))
          a =
        x
⊢ ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
    (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
          (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
            | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
            X.N))
        a =
      x

Tactic:
by_cases hj : x.dim < d

Premises used: SSet.N.toS, SSet.S.dim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
x : X.N
hj : x.dim < d
⊢ ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
    (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
          (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
            | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
            X.N))
        a =
      x

Tactic:
⟨⟨⟨_, hj⟩, ⟨_, x.nonDegenerate⟩⟩, rfl⟩

Premises used: Fin.mk, Subtype.mk, Exists.intro, SSet.N.nonDegenerate, Sigma.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
x : X.N
hj : x.dim < d
⊢ ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
    (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
          (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
            | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
            X.N))
        a =
      x

Tactic:
exact ⟨⟨⟨_, hj⟩, ⟨_, x.nonDegenerate⟩⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
x : X.N
hj : ¬x.dim < d
⊢ Membership.mem (γ := Set (X _⦋x.dim⦌)) (X.nonDegenerate x.dim) x.simplex

Tactic:
have := x.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this_1 : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
x : X.N
hj : ¬x.dim < d
this : Membership.mem (γ := Set (X _⦋x.dim⦌)) (X.nonDegenerate x.dim) x.simplex
⊢ d ≤ x.dim

Tactic:
simpa using hj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
this_1 : ∀ (i : Fin d), Finite.{u + 1} (↑(X.nonDegenerate (↑i : ℕ)) : Type u)
x : X.N
hj : ¬x.dim < d
this : Membership.mem (γ := Set (X _⦋x.dim⦌)) (X.nonDegenerate x.dim) x.simplex
⊢ ∃ (a : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
    (fun (x : (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u)) ↦
          (match (motive := (i : Fin d) × (↑(X.nonDegenerate (↑i : ℕ)) : Type u) → X.N) x with
            | ⟨i, x⟩ => N.mk (↑x : X _⦋(↑i : ℕ)⦌) ⋯ :
            X.N))
        a =
      x

Tactic:
simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d x.dim (by simpa using hj)] at this

Premises used: SSet.N.toS, SSet.S.dim, SSet.nonDegenerate_eq_empty_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
have : ∀ (this : Fintype X.N), ∃ (d : ℕ), X.HasDimensionLT d
⊢ ∃ (d : ℕ), X.HasDimensionLT d

Tactic:
have : Fintype X.N := Fintype.ofFinite _
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
pos : ∀ (h : (Finset.image φ ⊤).Nonempty), ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
neg : ∀ (h : ¬(Finset.image φ ⊤).Nonempty), ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
by_cases h : (Finset.image φ ⊤).Nonempty

Premises used: Finset.Nonempty, Top.top, Finset.image
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
pos : ∀ (d : ℕ) (hd : (Finset.image φ ⊤).max = (↑d : WithBot ℕ)), ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
obtain ⟨d, hd⟩ := Finset.max_of_nonempty h

Premises used: Finset.max_of_nonempty
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
d : ℕ
hd : (Finset.image φ ⊤).max = (↑d : WithBot ℕ)
x : ℕ
h_1 : x ∈ Finset.image φ ⊤
⊢ x < d + 1

Tactic:
grind [WithBot.coe_le_coe, → Finset.le_max]

Premises used: WithBot.coe_le_coe, Finset.le_max
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
d : ℕ
hd : (Finset.image φ ⊤).max = (↑d : WithBot ℕ)
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
exact ⟨d + 1, fun _ _ ↦ by grind [WithBot.coe_le_coe, → Finset.le_max]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : ¬(Finset.image φ ⊤).Nonempty
⊢ Finset.image φ ⊤ = ∅

Tactic:
rw [Finset.not_nonempty_iff_eq_empty] at h

Premises used: Finset.not_nonempty_iff_eq_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : Finset.image φ ⊤ = ∅
neg : ∃ (d : ℕ), ∀ (s : ℕ), Membership.mem (γ := Finset ℕ) ∅ s → s < d
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
simp only [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∀ (s : ℕ), Membership.mem (γ := Finset ℕ) ∅ s → s < 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∃ (d : ℕ), ∀ (s : ℕ), Membership.mem (γ := Finset ℕ) ∅ s → s < d

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
obtain : ∀ (d : ℕ) (hd : ∀ s ∈ Finset.image φ ⊤, s < d), ∃ (d : ℕ), X.HasDimensionLT d
⊢ ∃ (d : ℕ), X.HasDimensionLT d

Tactic:
obtain ⟨d, hd⟩ : ∃ (d : ℕ), ∀ (s : ℕ) (_ : s ∈ Finset.image φ ⊤), s < d := by
    by_cases h : (Finset.image φ ⊤).Nonempty
    · obtain ⟨d, hd⟩ := Finset.max_of_nonempty h
      exact ⟨d + 1, fun _ _ ↦ by grind [WithBot.coe_le_coe, → Finset.le_max]⟩
    · rw [Finset.not_nonempty_iff_eq_empty] at h
      simp only [h]
      exact ⟨0, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
⊢ ∃ (d : ℕ), X.HasDimensionLT d

Tactic:
⟨d, ⟨fun n hn ↦ ?_⟩⟩

Premises used: SSet.HasDimensionLT.mk, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
refine : ∀ (n : ℕ) (hn : d ≤ n), X.degenerate n = ⊤
⊢ ∃ (d : ℕ), X.HasDimensionLT d

Tactic:
refine ⟨d, ⟨fun n hn ↦ ?_⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
h : ∀ (x : X _⦋n⦌), x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
⊢ X.degenerate n = ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
h : x ∉ X.nonDegenerate n
⊢ x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x

Tactic:
simp only [mem_degenerate_iff_notMem_nonDegenerate, Set.top_eq_univ,
    Set.mem_univ, iff_true]

Premises used: SSet.mem_degenerate_iff_notMem_nonDegenerate, iff_true, Set.top_eq_univ, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ φ (N.mk x hx) ∈ Finset.image φ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ φ (N.mk x hx) < d

Tactic:
have := hd (φ (N.mk _ hx)) (by simp)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
this_1 : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
this : n < d
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : SimplexCategoryᵒᵖ
obtain : ∀ (n : SimplexCategory), Finite.{u + 1} (X.obj (Opposite.op n))
⊢ Finite.{u + 1} (X.obj n)

Tactic:
obtain ⟨n⟩ := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : SimplexCategory
mk : ∀ (n : ℕ), Finite.{u + 1} (X _⦋n⦌)
⊢ Finite.{u + 1} (X.obj (Opposite.op n))

Tactic:
induction n using SimplexCategory.rec with | _ n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
x : X _⦋n⦌
obtain :
  ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (hf : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    ∃ (a : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)),
      φ a =
        (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 : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)), φ a = x

Tactic:
obtain ⟨m, f, hf, y, rfl⟩ := X.exists_nonDegenerate x

Premises used: SSet.exists_nonDegenerate, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ m ≤ n

Tactic:
have := SimplexCategory.le_of_epi f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : m ≤ n
⊢ m < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : m ≤ n
⊢ ∃ (a : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)),
    φ a =
      (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⦌)

Tactic:
exact ⟨⟨⟨m, by lia⟩, f, y⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
⊢ Function.Surjective φ

Tactic:
have hφ : Function.Surjective φ := fun x ↦ by
    obtain ⟨m, f, hf, y, rfl⟩ := X.exists_nonDegenerate x
    have := SimplexCategory.le_of_epi f
    exact ⟨⟨⟨m, by lia⟩, f, y⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
hφ : Function.Surjective φ
⊢ Finite.{u + 1} (X _⦋n⦌)

Tactic:
Finite.of_surjective _ hφ

Premises used: Finite.of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌ :=
  fun (x : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)) ↦
    match (motive := (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u) → X _⦋n⦌)
      x with
    | ⟨m, ⟨f, 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⦌))
        (↑x : X _⦋(↑m : ℕ)⦌)
hφ : Function.Surjective φ
⊢ Finite.{u + 1} (X _⦋n⦌)

Tactic:
exact Finite.of_surjective _ hφ

Premises used: Finite.of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
obtain : ∀ (d : ℕ), X.HasDimensionLT d → SSet.Finite.{u} A.toSSet
⊢ SSet.Finite.{u} A.toSSet

Tactic:
obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite

Premises used: SSet.hasDimensionLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
d : ℕ
h : X.HasDimensionLT d
⊢ SSet.Finite.{u} A.toSSet

Tactic:
finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)

Premises used: SSet.finite_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
d : ℕ
h : X.HasDimensionLT d
refine : ∀ (i : ℕ) (hi : i < d), Finite.{u + 1} (↑(A.toSSet.nonDegenerate i) : Type u)
⊢ SSet.Finite.{u} A.toSSet

Tactic:
refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)

Premises used: SSet.finite_of_hasDimensionLT