awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
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)
⊢ x = y
have h₁ : ∃ (h :
  S.dim.{u} (X := X) (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) sorry) x)) =
    S.dim.{u} (X := X) (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) sorry) y))),
  (S.cast (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) sorry) x)) h).simplex =
    S.simplex (N.toS ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦ N.mk (↑x : X _⦋n⦌) sorry) y))
Tactic: rw [N.ext_iff, S.ext_iff'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, Finite.{u + 1} (↑(X.nonDegenerate i) : Type u)
⊢ Finite.{u + 1} X.N
have this : ∀ (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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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
have 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 : ℕ)⦌) sorry :
            X.N))
        a =
      x
Tactic: refine Finite.of_surjective (α := Σ (i : Fin d), X.nonDegenerate i)
      (f := fun ⟨i, x⟩ ↦ N.mk _ x.property) (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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
⊢ ∃ (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
have 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 : ℕ)⦌) sorry :
            X.N))
        a =
      x
Tactic: by_cases hj : x.dim < d
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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
⊢ ∃ (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
have 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 : ℕ)⦌) sorry :
            X.N))
        a =
      x
Tactic: by_cases hj : x.dim < d
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
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
have this₁ : Membership.mem (γ := Set (X _⦋x.dim⦌)) (X.nonDegenerate x.dim) x.simplex
Tactic: have := x.nonDegenerate
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
⊢ ∃ (d : ℕ), X.HasDimensionLT d
have have : ∀ (this : Fintype X.N), ∃ (d : ℕ), X.HasDimensionLT d
Tactic: have : Fintype X.N := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
have pos : ∀ (h : (Finset.image φ ⊤).Nonempty), ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
Tactic: by_cases h : (Finset.image φ ⊤).Nonempty
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
have neg : ∀ (h : ¬(Finset.image φ ⊤).Nonempty), ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
Tactic: by_cases h : (Finset.image φ ⊤).Nonempty
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
have pos : ∀ (d : ℕ) (hd : (Finset.image φ ⊤).max = (↑d : WithBot ℕ)), ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
Tactic: obtain ⟨d, hd⟩ := Finset.max_of_nonempty h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : ¬(Finset.image φ ⊤).Nonempty
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
have h₁ : Finset.image φ ⊤ = ∅
Tactic: rw [Finset.not_nonempty_iff_eq_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∃ (d : ℕ), ∀ s ∈ Finset.image φ ⊤, s < d
have neg : ∃ (d : ℕ), ∀ (s : ℕ), Membership.mem (γ := Finset ℕ) ∅ s → s < d
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
this : Fintype X.N
φ : (x : X.N) → ℕ := fun (x : X.N) ↦ x.dim
⊢ ∃ (d : ℕ), X.HasDimensionLT d
have obtain : ∀ (d : ℕ) (hd : ∀ s ∈ Finset.image φ ⊤, s < 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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
have refine : ∀ (n : ℕ) (hn : d ≤ n), X.degenerate n = ⊤
Tactic: refine ⟨d, ⟨fun n hn ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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.degenerate n = ⊤
have h : ∀ (x : X _⦋n⦌), x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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⦌
⊢ x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
have h : x ∉ X.nonDegenerate n
Tactic: simp only [mem_degenerate_iff_notMem_nonDegenerate, Set.top_eq_univ,
    Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
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
⊢ False
have this₁ : φ (N.mk x hx) < d
Tactic: have := hd (φ (N.mk _ hx)) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
n : SimplexCategoryᵒᵖ
⊢ Finite.{u + 1} (X.obj n)
have obtain : ∀ (n : SimplexCategory), Finite.{u + 1} (X.obj (Opposite.op n))
Tactic: obtain ⟨n⟩ := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
n : SimplexCategory
⊢ Finite.{u + 1} (X.obj (Opposite.op n))
have mk : ∀ (n : ℕ), Finite.{u + 1} (X _⦋n⦌)
Tactic: induction n using SimplexCategory.rec with | _ n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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⦌
⊢ ∃ (a : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋(↑m : ℕ)⦌) × (↑(X.nonDegenerate (↑m : ℕ)) : Type u)), φ a = x
have 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⦌)
Tactic: obtain ⟨m, f, hf, y, rfl⟩ := X.exists_nonDegenerate x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
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)
⊢ ∃ (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⦌)
have this : m ≤ n
Tactic: have := SimplexCategory.le_of_epi f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
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 : ℕ)⦌)
⊢ Finite.{u + 1} (X _⦋n⦌)
have hφ : 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
⊢ SSet.Finite.{u} A.toSSet
have obtain : ∀ (d : ℕ), X.HasDimensionLT d → SSet.Finite.{u} A.toSSet
Tactic: obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
d : ℕ
h : X.HasDimensionLT d
⊢ SSet.Finite.{u} A.toSSet
have refine : ∀ (i : ℕ) (hi : i < d), Finite.{u + 1} (↑(A.toSSet.nonDegenerate i) : Type u)
Tactic: refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
inst : X.Finite
A : X.Subcomplex
d : ℕ
h : X.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite.{u + 1} (↑(A.toSSet.nonDegenerate i) : Type u)
have apply : Function.Injective (β := X _⦋i⦌) fun (a : (↑(A.toSSet.nonDegenerate i) : Type u)) ↦ (↑(↑a : A.toSSet _⦋i⦌) : X _⦋i⦌)
Tactic: apply Finite.of_injective (f := fun a ↦ a.1.1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X Y : SSet
inst : Y.Finite
f : X ⟶ Y
hf : Mono f
⊢ X.Finite
have obtain : ∀ (d : ℕ), Y.HasDimensionLT d → X.Finite
Tactic: obtain ⟨d, _⟩ := Y.hasDimensionLT_of_finite
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X Y : SSet
inst : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h : Y.HasDimensionLT d
⊢ X.Finite
have this : X.HasDimensionLT d
Tactic: have := hasDimensionLT_of_mono f d
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
⊢ Y.Finite
have obtain : ∀ (d : ℕ), X.HasDimensionLT d → Y.Finite
Tactic: obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
⊢ Y.Finite
have this : Y.HasDimensionLT d
Tactic: have := hasDimensionLT_of_epi f d
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
⊢ Y.Finite
have refine : ∀ (i : ℕ) (hi : i < d), Finite.{u + 1} (↑(Y.nonDegenerate i) : Type u)
Tactic: refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite.{u + 1} (Y _⦋i⦌)
have rw : ∀ (hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)) (d : ℕ),
  X.HasDimensionLT d → ∀ (this : Y.HasDimensionLT d) (i : ℕ) (hi : i < d), Finite.{u + 1} (Y _⦋i⦌)
Tactic: rw [NatTrans.epi_iff_epi_app] at hf
Cleared hypotheses: hf, d, h, this, i, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite.{u + 1} (Y _⦋i⦌)
have hf₁ : ∀ (k : SimplexCategoryᵒᵖ),
  Function.Surjective (α := X.obj k) (β := Y.obj k)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app k)) : (a : X.obj k) → Y.obj k)
Tactic: simp only [epi_iff_surjective] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X Y : SSet
inst : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite.{u + 1} (↑(Y.nonDegenerate i) : Type u)
have this₁ : Finite.{u + 1} (Y _⦋i⦌)
Tactic: have : Finite (Y _⦋i⦌) := by
    rw [NatTrans.epi_iff_epi_app] at hf
    simp only [epi_iff_surjective] at hf
    exact Finite.of_surjective _ (hf _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
⊢ SSet.Finite.{u} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)) ↔ ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
have refine : ∀ (h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet), Finite.{u + 1} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N
Tactic: refine ⟨fun h i ↦ finite_of_mono (Subcomplex.homOfLE (le_iSup A i)), fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
⊢ Finite.{u + 1} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N
have refine : Function.Surjective (β := (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N)
  fun (x : (i : ι) × N (@Subcomplex.toSSet X (A i))) ↦
  match (motive := (i : ι) × N (@Subcomplex.toSSet X (A i)) → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
  | ⟨i, s⟩ =>
    N.mk
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE sorry).app (Opposite.op ⦋s.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
        s.simplex)
      sorry
Tactic: refine Finite.of_surjective (f := fun (⟨i, s⟩ : Σ (i : ι), (A i).toSSet.N) ↦
    N.mk ((Subcomplex.homOfLE (le_iSup A i)).app _ s.simplex)
      (by simpa only [nonDegenerate_iff_of_mono] using s.nonDegenerate)) ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
s : (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      s
have obtain : ∀ (d : ℕ) (s : X _⦋d⦌) (h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s)
  (h₂ :
    Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
      ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
      (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
        Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)),
  ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE sorry).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                sorry :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
              h₂) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        sorry
Tactic: obtain ⟨d, ⟨⟨s, h₁⟩, h₂⟩, rfl⟩ := s.mk_surjective
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (hypothesis)
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂ :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
              h₂) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        ⋯
have h₃ : ∃ (i : ι), Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
Tactic: simp only [Subfunctor.iSup_obj, Set.mem_iUnion] at h₁