awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
ha' :
  x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
have mpr : ∀
  (hx :
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                  Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) sorry) :
              (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
            a) :
        X _⦋n⦌)),
  Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) sorry) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
Tactic: subst ha'
Cleared hypotheses: x, hx, ha'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
hx :
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
have ha₁ : (↑a : X _⦋m⦌) ∈ X.nonDegenerate m
Tactic: rw [mem_nonDegenerate_iff] at ha
Cleared hypotheses: ha, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
n : SimplexCategory
x : X.obj (op n)
hx : Membership.mem (γ := Set (X.obj (op n))) (A.obj (op n)) x
⊢ Membership.mem (γ := Set (X.obj (op n))) (B.obj (op n)) x
have mpr : ∀ (n : ℕ) ⦃x : X _⦋n⦌⦄ (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x),
  Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
Tactic: induction n using SimplexCategory.rec with | _ n =>
    obtain ⟨m, f, _, ⟨a, ha⟩, ha'⟩ := exists_nonDegenerate A ⟨x, hx⟩
    simp only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
      Subfunctor.toFunctor_map] at ha'
    subst ha'
    rw [mem_nonDegenerate_iff] at ha
    exact B.map f.op (h _ ⟨_, ha⟩ a.prop)
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤ ↔ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
have mp : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤ → X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
mp : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤ → X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤ ↔ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
have mpr : X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
have mp : ∀ (x : X _⦋n⦌), x ∈ X.degenerate n ⊓ A.obj (op ⦋n⦌) ↔ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ⊓ A.obj (op ⦋n⦌) ↔ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
have mp : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x → x ∈ X.degenerate n
Tactic: simp only [Set.inf_eq_inter, Set.mem_inter_iff, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
have h₁ : A.obj (op ⦋n⦌) ⊆ X.degenerate n
Tactic: simp only [Set.inf_eq_inter, Set.inter_eq_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
have mpr : ∀ (x : A.toSSet _⦋n⦌),
  Membership.mem (γ := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) x ↔ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
⊢ Eq.{u + 1} (α := X.Subcomplex)
    (⨆ (x : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
      ofSimplex (↑(x.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋x.fst⦌))
    ⊤
have rw : ∀ (n : ℕ),
  X.nonDegenerate n ⊆
    Subfunctor.obj
      (⨆ (x : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
        ofSimplex (↑(x.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋x.fst⦌))
      (op ⦋n⦌)
Tactic: rw [eq_top_iff_contains_nonDegenerate]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Membership.mem (γ := Set (X _⦋n⦌))
    (Subfunctor.obj
      (⨆ (x : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
        ofSimplex (↑(x.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋x.fst⦌))
      (op ⦋n⦌))
    x
have simp : ∃ (a : ℕ), ∃ a_1 ∈ X.nonDegenerate a, Membership.mem (γ := Set (X _⦋n⦌)) ((ofSimplex a_1).obj (op ⦋n⦌)) x
Tactic: simp only [Subfunctor.iSup_obj, Set.mem_iUnion, Sigma.exists,
    Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
f : X ⟶ Y
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
have obtain : ∀ (m : ℕ) (hm : m < n) (g : ⦋n⦌ ⟶ ⦋m⦌) (y : X _⦋m⦌),
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            y :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
Tactic: obtain ⟨m, hm, g, y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋m⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋m⦌))
            y :
          (fun (X : Type u) ↦ X) (Y _⦋m⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            y :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
have rw : Eq (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g.op) :
        (a : (fun (X : Type u) ↦ X) (Y _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋m⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋m⦌))
          y :
        (fun (X : Type u) ↦ X) (Y _⦋m⦌)) :
    (fun (X : Type u) ↦ X) (Y _⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g.op) : (a : Y _⦋m⦌) → Y _⦋n⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋m⦌)) : (a : X _⦋m⦌) → Y _⦋m⦌) y : Y _⦋m⦌) :
    Y _⦋n⦌)
Tactic: rw [NatTrans.naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.degenerate n
have mp : Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌)) →
  x ∈ X.degenerate n
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
mp :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) →
    x ∈ X.degenerate n
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.degenerate n
have mpr : x ∈ X.degenerate n →
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst : Mono f
x : X _⦋n⦌
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.degenerate n
have rw : Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.toRange f).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Subcomplex.range f).toSSet _⦋n⦌))
          x) :
      Y _⦋n⦌) ∈
    Y.degenerate n
Tactic: rw [← degenerate_iff_of_isIso (Subcomplex.toRange f) x,
    Subcomplex.mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
d : ℕ
inst : X.HasDimensionLT d
⊢ n < d
have by_contra! : ∀ (this : d ≤ n), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
d : ℕ
inst : X.HasDimensionLT d
this : d ≤ n
⊢ False
have obtain : ∀ (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n), False
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
have h : ∀ (x : A.toSSet _⦋n⦌),
  Membership.mem (γ := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) x ↔ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
⊢ A ≤ B ↔ ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
have refine : ∀ (h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)), A ≤ B
Tactic: refine ⟨fun h i hi a ⟨ha, _⟩ ↦ h _ ha, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
⊢ A ≤ B
have rw : ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
    Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
Tactic: rw [le_iff_contains_nonDegenerate]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
d : ℕ
inst_1 : Y.HasDimensionLT 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.Dimension (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
d : ℕ
inst_1 : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
have h : Membership.mem (γ := Set (Y _⦋n⦌)) Set.univ
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.toRange f).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Subcomplex.range f).toSSet _⦋n⦌))
          x) :
      Y _⦋n⦌) ↔
  Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
Tactic: rw [← degenerate_iff_of_isIso (Subcomplex.toRange f),
      Subcomplex.mem_degenerate_iff, Y.degenerate_eq_univ_of_hasDimensionLT d n hn]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ Y.degenerate n = ⊤
have h : ∀ (y : Y _⦋n⦌), y ∈ Y.degenerate n ↔ Membership.mem (γ := Set (Y _⦋n⦌)) ⊤ y
Tactic: ext y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
y : Y _⦋n⦌
⊢ y ∈ Y.degenerate n ↔ Membership.mem (γ := Set (Y _⦋n⦌)) ⊤ y
have h : y ∈ Y.degenerate n
Tactic: simp only [Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
y : Y _⦋n⦌
⊢ y ∈ Y.degenerate n
have h : ∀ (x : X _⦋n⦌),
  Membership.mem (α := Y _⦋n⦌) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
Tactic: obtain ⟨x, rfl⟩ := epi_iff_surjective (f := (f.app (op ⦋n⦌))).1 inferInstance y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Epi f
d : ℕ
inst_1 : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ Membership.mem (α := Y _⦋n⦌) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
have h : x ∈ X.degenerate n
Tactic: apply degenerate_app_apply
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
ι : Type u_1
A : ι → X.Subcomplex
d : ℕ
⊢ HasDimensionLT.{u} (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)) d ↔ ∀ (i : ι), HasDimensionLT.{u} (A i).toSSet d
have simp : (∀ (n : ℕ) (hn : d ≤ n),
    X.degenerate n ⊓ Subfunctor.obj (⨆ (i : ι), A i) (op ⦋n⦌) = Subfunctor.obj (⨆ (i : ι), A i) (op ⦋n⦌)) ↔
  ∀ (i : ι) (n : ℕ) (hn : d ≤ n), X.degenerate n ⊓ (A i).obj (op ⦋n⦌) = (A i).obj (op ⦋n⦌)
Tactic: simp only [hasDimensionLT_iff, Subcomplex.degenerate_eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Dimension (goal)
Goal:
X : SSet
n k : ℕ
hk : n ≤ k
⊢ Eq.{u + 1} (α := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ((Subcomplex.toSSet (X := X) ⊥).degenerate k) ⊤
have h : ∀ (x : X _⦋k⦌) (hx : Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x),
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ((Subcomplex.toSSet (X := X) ⊥).degenerate k)
      (Subtype.mk (p := fun (x : X _⦋k⦌) ↦ Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x) x hx) ↔
    Membership.mem (γ := Set (Subcomplex.toSSet (X := X) ⊥ _⦋k⦌)) ⊤
      (Subtype.mk (p := fun (x : X _⦋k⦌) ↦ Membership.mem (γ := Set (X _⦋k⦌)) (Subfunctor.obj ⊥ (op ⦋k⦌)) x) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
⊢ Eq.{u + 1} (α := Subcomplex c.1) (⨆ (j : J), Subcomplex.range (c.ι.app j)) ⊤
have obj : ∀ (n : SimplexCategoryᵒᵖ) (x : Functor.obj c.1 n),
  Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj (⨆ (j : J), Subcomplex.range (c.ι.app j)) n) x ↔
    Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj ⊤ n) x
Tactic: ext n x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : SimplexCategoryᵒᵖ
x : Functor.obj c.1 n
⊢ Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj (⨆ (j : J), Subcomplex.range (c.ι.app j)) n) x ↔
    Membership.mem (γ := Set (Functor.obj c.1 n)) (Subfunctor.obj ⊤ n) x
have obj : ∃ (i : J) (y : (F.obj i).obj n),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.ι.app i).app n) : (a : (F.obj i).obj n) → c.1.obj n) y = x
Tactic: simp only [Subfunctor.iSup_obj, Subfunctor.range_obj, Set.mem_iUnion, Set.mem_range,
    Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
| Subcomplex.range φ
have rw : Subcomplex.range (𝟙 c.pt ≫ φ)
Tactic: rw [← Category.id_comp φ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ Subcomplex.range φ = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)
have conv_lhs : Subcomplex.range (𝟙 c.pt ≫ φ) = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)
Tactic: conv_lhs => rw [← Category.id_comp φ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ Subcomplex.range (𝟙 c.pt ≫ φ) = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)
have simp_rw : (Subcomplex.range (𝟙 c.pt)).image φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
Tactic: simp_rw [Subcomplex.range_comp, Subcomplex.range_eq_top, ← iSup_range_eq_top_of_isColimit hc,
    Subcomplex.image_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
simp_rw : (Subcomplex.range (𝟙 c.pt)).image φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
⊢ Subcomplex.range (𝟙 c.pt ≫ φ) = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)
have simp_rw₁ : Subcomplex.image ⊤ φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
Tactic: simp_rw [Subcomplex.range_comp, Subcomplex.range_eq_top, ← iSup_range_eq_top_of_isColimit hc,
    Subcomplex.image_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
simp_rw : (Subcomplex.range (𝟙 c.pt)).image φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
simp_rw₁ : Subcomplex.image ⊤ φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
⊢ Subcomplex.range (𝟙 c.pt ≫ φ) = ⨆ (j : J), Subcomplex.range (c.ι.app j ≫ φ)
have simp_rw₂ : Subcomplex.image (⨆ (j : J), Subcomplex.range (c.ι.app j)) φ = ⨆ (j : J), (Subcomplex.range (c.ι.app j)).image φ
Tactic: simp_rw [Subcomplex.range_comp, Subcomplex.range_eq_top, ← iSup_range_eq_top_of_isColimit hc,
    Subcomplex.image_iSup]