awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin (n + 1)
succ : (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow 0 = p.arrow 0
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow i = p.arrow i
have succ₁ : ∀ (i : Fin n),
  (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌) sorry)).arrow i.succ = p.arrow i.succ
Tactic: obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow 0 = p.arrow 0
have succ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
    ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌) sorry) =
  p.arrow 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯) =
    p.arrow 0
have succ : p.arrow 0 = p.arrow 0
Tactic: rw [map_mkOfSucc_zero_concat]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
⊢ { s : X _⦋n⦌ // X.spine n s = p }
have zero : (p : X.Path 0) → { s : X _⦋0⦌ // X.spine 0 s = p }
Tactic: induction n with
  | zero => exact ⟨p.vertex 0, by aesop⟩
  | succ n hn =>
    refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
    · rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0
    · ext i
      obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
      · dsimp
        rw [map_mkOfSucc_zero_concat]
      · simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
          op_comp, Functor.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
          ← p.arrow_interval 1 n i i.succ (by grind) (by grind)] using
            Path.congr_arrow (hn (p.interval 1 n)).prop i
Cleared hypotheses: n, p
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
zero : (p : X.Path 0) → { s : X _⦋0⦌ // X.spine 0 s = p }
⊢ { s : X _⦋n⦌ // X.spine n s = p }
have succ : (n : ℕ) →
  (hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }) →
    (p : X.Path (n + 1)) → { s : X _⦋n + 1⦌ // X.spine (n + 1) s = p }
Tactic: induction n with
  | zero => exact ⟨p.vertex 0, by aesop⟩
  | succ n hn =>
    refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
    · rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0
    · ext i
      obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
      · dsimp
        rw [map_mkOfSucc_zero_concat]
      · simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
          op_comp, Functor.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
          ← p.arrow_interval 1 n i i.succ (by grind) (by grind)] using
            Path.congr_arrow (hn (p.interval 1 n)).prop i
Cleared hypotheses: n, p
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p_1 : X.Path n
p : X.Path (n + 1)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (p.arrow 0) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (spineToSimplex h (p.interval 1 n ⋯)) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
have rw : p.vertex (Fin.succ 0) =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
    (spineToSimplex h (p.interval 1 n sorry))
Tactic: rw [p.arrow_tgt 0]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (spineToSimplex h p) =
    p.arrow 0
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n sorry)) sorry) =
  p.arrow 0
Tactic: rw [spineToSimplex_succ, map_mkOfSucc_zero_concat]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    p.arrow 0
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (spineToSimplex h p) =
    p.arrow 0
have rw₁ : p.arrow 0 = p.arrow 0
Tactic: rw [spineToSimplex_succ, map_mkOfSucc_zero_concat]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (spineToSimplex h p) =
    spineToSimplex h (p.interval 1 n ⋯)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
      (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n sorry)) sorry) =
  spineToSimplex h (p.interval 1 n sorry)
Tactic: rw [spineToSimplex_succ, δ₀_concat]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n ⋯)) ⋯) =
    spineToSimplex h (p.interval 1 n ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (spineToSimplex h p) =
    spineToSimplex h (p.interval 1 n ⋯)
have rw₁ : spineToSimplex h (p.interval 1 n sorry) = spineToSimplex h (p.interval 1 n sorry)
Tactic: rw [spineToSimplex_succ, δ₀_concat]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n_1 n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (spineToSimplex h (X.spine (n + 1) s)) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        s :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
have rw : spineToSimplex h ((X.spine (n + 1) s).interval 1 n sorry) =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
      (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
    s
Tactic: rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n_1 n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
rw :
  spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      s
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (spineToSimplex h (X.spine (n + 1) s)) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        s :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
have rw₁ : spineToSimplex h ((X.spine (n + 1) s).interval 1 n sorry) =
  spineToSimplex h
    (X.spine n
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        s))
Tactic: rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n_1 n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
rw :
  spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      s
rw₁ :
  spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) =
    spineToSimplex h
      (X.spine n
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          s))
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (spineToSimplex h (X.spine (n + 1) s)) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        s :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
have rw₂ : spineToSimplex h ((X.spine (n + 1) s).interval 1 n sorry) = spineToSimplex h ((X.spine (n + 1) s).interval 1 n sorry)
Tactic: rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋n⦌
⊢ spineToSimplex h (X.spine n s) = s
have zero : ∀ (s : X _⦋0⦌), spineToSimplex h (X.spine 0 s) = s
Tactic: induction n with
  | zero => simp [spineToSimplex_zero]
  | succ n hn =>
    exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋n⦌
zero : ∀ (s : X _⦋0⦌), spineToSimplex h (X.spine 0 s) = s
⊢ spineToSimplex h (X.spine n s) = s
have succ : ∀ (n : ℕ) (hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s) (s : X _⦋n + 1⦌),
  spineToSimplex h (X.spine (n + 1) s) = s
Tactic: induction n with
  | zero => simp [spineToSimplex_zero]
  | succ n hn =>
    exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
⊢ IsIso f
have rw : ∀ (X_1 : SimplexCategoryᵒᵖ), IsIso (f.app X_1)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
⊢ IsIso (f.app X_1)
have rw : Function.Bijective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
    (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
Tactic: rw [isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
⊢ Function.Bijective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
have left : Function.Injective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
    (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
left :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
⊢ Function.Bijective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
have right : Function.Surjective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
    (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
have left : Mono (f.app X_1)
Tactic: rw [← mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : Mono f
h_1 : Epi f
X_1 : SimplexCategoryᵒᵖ
⊢ Function.Surjective (α := (fun (X : Type u) ↦ X) (X.obj X_1)) (β := (fun (X : Type u) ↦ X) (Y.obj X_1))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X_1)) :
      (a : (fun (X : Type u) ↦ X) (X.obj X_1)) → (fun (X : Type u) ↦ X) (Y.obj X_1))
have right : Epi (f.app X_1)
Tactic: rw [← epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
x x_1 : toSSet (X := X) ⊥ ⟶ Y
⊢ x = x_1
have w : ∀ (n : SimplexCategoryᵒᵖ) (val : X.obj n) (h : Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) val),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (x.app n)).toFun
      (Subtype.mk (p := fun (x : X.obj n) ↦ Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) x) val h) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app n)).toFun
      (Subtype.mk (p := fun (x : X.obj n) ↦ Membership.mem (γ := Set (X.obj n)) (Subfunctor.obj ⊥ n) x) val h)
Tactic: ext _ ⟨_, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
⊢ ((toSSet (X := X) ⊥).map x_2 ≫
      ↾fun (x : (toSSet (X := X) ⊥).obj x_1) ↦
        match (motive := (toSSet (X := X) ⊥).obj x_1 → Y.obj x_1) x with
        | ⟨val, h⟩ => False.elim ⋯) =
    (↾fun (x_3 : (toSSet (X := X) ⊥).obj x) ↦
        match (motive := (toSSet (X := X) ⊥).obj x → Y.obj x) x_3 with
        | ⟨val, h⟩ => False.elim ⋯) ≫
      Y.map x_2
have h : ∀ (val : X.obj x) (h : Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) val),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((toSSet (X := X) ⊥).map x_2 ≫
          ↾fun (x : (toSSet (X := X) ⊥).obj x_1) ↦
            match (motive := (toSSet (X := X) ⊥).obj x_1 → Y.obj x_1) x with
            | ⟨val, h⟩ => False.elim sorry))
      (Subtype.mk (p := fun (x_3 : X.obj x) ↦ Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) x_3) val h) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_3 : (toSSet (X := X) ⊥).obj x) ↦
            match (motive := (toSSet (X := X) ⊥).obj x → Y.obj x) x_3 with
            | ⟨val, h⟩ => False.elim sorry) ≫
          Y.map x_2))
      (Subtype.mk (p := fun (x_3 : X.obj x) ↦ Membership.mem (γ := Set (X.obj x)) (Subfunctor.obj ⊥ x) x_3) val h)
Tactic: ext ⟨_, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X : SSet
x : X _⦋0⦌
⊢ (ofSimplex x).ι = const x
have w : ∀ (n : SimplexCategoryᵒᵖ) (u : Opposite.unop n ⟶ Opposite.unop (Opposite.op ⦋0⦌)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        sorry) =
    TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        sorry)
Tactic: ext n ⟨_, ⟨u⟩, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : SimplexCategoryᵒᵖ
u : Opposite.unop n ⟶ Opposite.unop (Opposite.op ⦋0⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯) =
    TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
      (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.op u)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
          x)
        ⋯)
have w : (ConcreteCategory.hom (FC := TypeCat.Fun) ((ofSimplex x).ι.app n)).toFun
    (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
        x)
      sorry) =
  TypeCat.Fun.toFun (X := (ofSimplex x).toSSet.obj n)
    (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (const x) n))
    (Subtype.mk (p := fun (x_1 : X.obj n) ↦ x_1 ∈ (ofSimplex x).obj n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X.obj n))
        x)
      sorry)
Tactic: obtain rfl := Subsingleton.elim u (SimplexCategory.const _ _ 0)
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
y : X.obj m
⊢ y ∈ (ofSimplex x).obj m ↔
    ∃ (f : Opposite.unop m ⟶ ⦋n⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj (Opposite.op (Opposite.unop m))))
          x =
        y
have dsimp : (∃ (f : Opposite.op ⦋n⦌ ⟶ m), (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) : (a : X _⦋n⦌) → X.obj m) x = y) ↔
  ∃ (f : Opposite.unop m ⟶ ⦋n⦌), (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋n⦌) → X.obj m) x = y
Tactic: dsimp [ofSimplex, Subfunctor.ofSection]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ ofSimplex (n := n)
      ((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) ≤
    ofSimplex x
have simp : Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((ofSimplex x).obj (Opposite.op ⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x : X _⦋n⦌)
Tactic: simp only [Subfunctor.ofSection_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
⊢ ofSimplex (n := n)
      ((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) =
    ofSimplex x
have refine : ofSimplex x ≤
  ofSimplex (n := n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      x)
Tactic: refine le_antisymm (ofSimplex_map_le f x) ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
⊢ ofSimplex x ≤
    ofSimplex (n := n)
      ((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)
have simp : Membership.mem (γ := Set (X _⦋m⦌))
  (Subfunctor.obj
    (ofSimplex (n := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x))
    (Opposite.op ⦋m⦌))
  x
Tactic: simp only [Subfunctor.ofSection_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (hypothesis)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
x : X _⦋m⦌
⊢ Membership.mem (γ := Set (X _⦋m⦌))
    (Subfunctor.obj
      (ofSimplex (n := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) x))
      (Opposite.op ⦋m⦌))
    x
have this : IsSplitEpi f
Tactic: have := isSplitEpi_of_epi f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
⊢ range f = ⊤ ↔ Epi f
have rw : (∀ (x : SimplexCategoryᵒᵖ), (range f).obj x = Subfunctor.obj ⊤ x) ↔ ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
Tactic: rw [NatTrans.epi_iff_epi_app, Subfunctor.ext_iff, funext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
⊢ ⊤ ≤ (range f).preimage f
have rw : image ⊤ f ≤ range f
Tactic: rw [← image_le_iff, image_top]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
rw : image ⊤ f ≤ range f
⊢ ⊤ ≤ (range f).preimage f
have rw₁ : range f ≤ range f
Tactic: rw [← image_le_iff, image_top]