awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ Eq (α := Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) : (a : Y _⦋y.dim⦌) → Y _⦋x.dim⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex :
            Y _⦋y.dim⦌) :
        Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex :
        Y _⦋x.dim⦌) ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
have rw : Eq (α := Y _⦋x.dim⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex :
          X _⦋x.dim⦌) :
      Y _⦋x.dim⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
        x.simplex :
      Y _⦋x.dim⦌) ↔
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
Tactic: rw [← NatTrans.naturality_apply e.hom f.op]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
⊢ x = x_1
have a : x ≤ x_1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
a : x ≤ x_1
⊢ x = x_1
have a₁ : x_1 ≤ x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
⊢ x ≤ x_1
have a : x.subcomplex ≤ x_1.subcomplex
Tactic: rw [N.le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
a : x.subcomplex ≤ x_1.subcomplex
⊢ x ≤ x_1
have a₁ : x_1.subcomplex ≤ x_1.subcomplex
Tactic: rw [N.le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
⊢ x_1 ≤ x
have a : x_1.subcomplex ≤ x.subcomplex
Tactic: rw [N.le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
a : x_1.subcomplex ≤ x.subcomplex
⊢ x_1 ≤ x
have a₁ : x_1.subcomplex ≤ x_1.subcomplex
Tactic: rw [N.le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y
have trans : { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy
Tactic: trans N.mk x hx = N.mk y hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
trans : { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy
⊢ { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y
have trans₁ : N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y
Tactic: trans N.mk x hx = N.mk y hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y
have simp : N.mk x hx ≤ N.mk y hy ∧ N.mk y hy ≤ N.mk x hx ↔
  Subcomplex.ofSimplex x ≤ Subcomplex.ofSimplex y ∧ Subcomplex.ofSimplex y ≤ Subcomplex.ofSimplex x
Tactic: simp only [le_antisymm_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
⊢ x.subcomplex ≤ y.subcomplex
have simp : Membership.mem (γ := Set (X _⦋x.dim⦌)) (y.subcomplex.obj (Opposite.op ⦋x.dim⦌)) x.simplex
Tactic: simp only [Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
⊢ x.subcomplex = y.subcomplex
have refine : y.subcomplex ≤ x.subcomplex
Tactic: refine le_antisymm (subcomplex_map_le x y f hf) ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
⊢ y.subcomplex ≤ x.subcomplex
have simp : Membership.mem (γ := Set (X _⦋y.dim⦌)) (x.subcomplex.obj (Opposite.op ⦋y.dim⦌)) y.simplex
Tactic: simp only [Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
⊢ Membership.mem (γ := Set (X _⦋y.dim⦌)) (x.subcomplex.obj (Opposite.op ⦋y.dim⦌)) y.simplex
have this : IsSplitEpi f
Tactic: have := isSplitEpi_of_epi f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x : X.S
⊢ ∃ (x_1 : X.N), x_1.subcomplex = x.subcomplex
have obtain : ∀ (n : ℕ) (x : X _⦋n⦌), ∃ (x_1 : X.N), x_1.subcomplex = { dim := n, simplex := x }.subcomplex
Tactic: obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ ∃ (x_1 : X.N), x_1.subcomplex = { dim := n, simplex := x }.subcomplex
have obtain : ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
  Epi f →
    ∀ (y : (↑(X.nonDegenerate m) : Type u)),
      ∃ (x : X.N),
        x.subcomplex =
          subcomplex
            (mk (dim := 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⦌))
                (↑y : X _⦋m⦌)))
Tactic: obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ ∃ (x : X.N),
    x.subcomplex =
      subcomplex
        (mk (dim := 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⦌))
            (↑y : X _⦋m⦌)))
have refine_1 : (N.mk (↑y : X _⦋m⦌) sorry).subcomplex ≤
  subcomplex
    (mk (dim := 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⦌))
        (↑y : X _⦋m⦌)))
Tactic: refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
refine_1 :
  (N.mk (↑y : X _⦋m⦌) ⋯).subcomplex ≤
    subcomplex
      (mk (dim := 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⦌))
          (↑y : X _⦋m⦌)))
⊢ ∃ (x : X.N),
    x.subcomplex =
      subcomplex
        (mk (dim := 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⦌))
            (↑y : X _⦋m⦌)))
have refine_2 : subcomplex
    (mk (dim := 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⦌))
        (↑y : X _⦋m⦌))) ≤
  (N.mk (↑y : X _⦋m⦌) sorry).subcomplex
Tactic: refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ (N.mk (↑y : X _⦋m⦌) ⋯).subcomplex ≤
    subcomplex
      (mk (dim := 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⦌))
          (↑y : X _⦋m⦌)))
have refine_1 : Membership.mem (γ := Set (X _⦋(N.mk (↑y : X _⦋m⦌) sorry).dim⦌))
  (Subfunctor.obj
    (subcomplex
      (mk (dim := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌))))
    (Opposite.op ⦋(N.mk (↑y : X _⦋m⦌) sorry).dim⦌))
  (N.mk (↑y : X _⦋m⦌) sorry).simplex
Tactic: simp only [Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ Membership.mem (γ := Set (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (Subfunctor.obj
      (subcomplex
        (mk (dim := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌))))
      (Opposite.op ⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (N.mk (↑y : X _⦋m⦌) ⋯).simplex
have this : IsSplitEpi f
Tactic: have := isSplitEpi_of_epi f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : IsSplitEpi f
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
have rw : Mono (X.map f.op)
Tactic: rw [← mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : IsSplitEpi f
⊢ Membership.mem (γ := Set (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (Subfunctor.obj
      (subcomplex
        (mk (dim := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌))))
      (Opposite.op ⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (N.mk (↑y : X _⦋m⦌) ⋯).simplex
have this₁ : Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
Tactic: have : Function.Injective (X.map f.op) := by
        rw [← mono_iff_injective]
        infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
⊢ Membership.mem (γ := Set (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (Subfunctor.obj
      (subcomplex
        (mk (dim := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌))))
      (Opposite.op ⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (N.mk (↑y : X _⦋m⦌) ⋯).simplex
have refine_1 : Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) :
            (a :
                (fun (X : Type u) ↦ X)
                  (X _⦋{ dim := n,
                        simplex := (ConcreteCategory.hom (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) }.dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) sorry).dim⦌))
          (simplex
            (mk (dim := n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌)))) :
        (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) sorry).dim⦌)) :
    (fun (X : Type u) ↦ X) (X _⦋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⦌))
      (N.mk (↑y : X _⦋m⦌) sorry).simplex :
    (fun (X : Type u) ↦ X) (X _⦋n⦌))
Tactic: refine ⟨(section_ f).op, this ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (X _⦋{ dim := n,
                          simplex :=
                            (ConcreteCategory.hom (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
            (simplex
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌)))) :
          (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌)) :
      (fun (X : Type u) ↦ X) (X _⦋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⦌))
        (N.mk (↑y : X _⦋m⦌) ⋯).simplex :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
have refine_1 : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
        X _⦋m⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1 : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1₁ : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((section_ f).op ≫ f.op)) : (a : X _⦋n⦌) → X _⦋n⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₁ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((section_ f).op ≫ f.op)) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1₂ : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op ≫ X.map ((section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
      (↑y : X _⦋m⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋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⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₁ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((section_ f).op ≫ f.op)) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₂ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op ≫ X.map ((section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1₃ : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
      (↑y : X _⦋m⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]