awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
f : unop x ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n].obj x) (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
⊢ Membership.mem.{u, u} (α := Δ[n].obj x) (γ := Set (Δ[n].obj x))
    (Subfunctor.obj
      (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
have simp : ∃ (f_1 : unop x ⟶ ⦋n⦌),
  Eq (α := Δ[n].obj x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map f_1.op) : (a : Δ[n] _⦋n⦌) → Δ[n].obj x)
        ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
      Δ[n].obj x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
Tactic: simp only [Subcomplex.mem_ofSimplex_obj_iff, op_unop]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
⊢ Membership.mem.{u, u} (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        (𝟙 (unop (op ⦋n⦌))) :
      stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
have rw : StrictMono (α := Fin (n + 1)) (β := Fin (n + 1))
  (⇑((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
          (𝟙 (unop (op ⦋n⦌))) :
        stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌) :
    (a : Fin (n + 1)) → Fin (n + 1))
Tactic: rw [mem_nonDegenerate_iff_strictMono]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
⊢ Eq (α := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    (singleton (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
      ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
          (𝟙 (unop (op ⦋n⦌))) :
        stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌))
have h : ∀ (x : Δ[n] _⦋n⦌),
  Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x ↔
    Membership.mem (γ := Set (Δ[n] _⦋n⦌))
      (singleton (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
            (𝟙 (unop (op ⦋n⦌))) :
          stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : Δ[n] _⦋n⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x ↔
    x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)
have h : ∀ (h : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x),
  x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : Δ[n] _⦋n⦌
h :
  ∀ (h : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x),
    x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x ↔
    x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)
have h₁ : x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) →
  Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : Δ[n] _⦋n⦌
h : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x
⊢ x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)
have h₁ : ∀ (f : unop (op ⦋n⦌) ⟶ ⦋n⦌)
  (h :
    Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
      ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)),
  Eq.{u + 1} (α := Δ[n] _⦋n⦌) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
    ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌)
Tactic: obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (hypothesis)
Goal:
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
⊢ Eq.{u + 1} (α := Δ[n] _⦋n⦌) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
    ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌)
have this : Mono f
Tactic: have : Mono f := by simpa using (mem_nonDegenerate_iff_mono _).mp h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
⊢ (stdSimplex.obj n).op.map f ≫
      Iso.hom
        ((fun (d : SimplexCategoryᵒᵖ) ↦
            (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
          d') =
    Iso.hom
        ((fun (d : SimplexCategoryᵒᵖ) ↦
            (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
          d) ≫
      (stdSimplex.obj n).map f
have h : ∀ (g : (stdSimplex.obj n).op.obj d),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((stdSimplex.obj n).op.map f ≫
          Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d) ≫
          (stdSimplex.obj n).map f))
      g
Tactic: ext g
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((stdSimplex.obj n).op.map f ≫
          Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d) ≫
          (stdSimplex.obj n).map f))
      g
have h : ∀ (i : Fin (len d'.1 + 1)),
  Eq (α := Fin (n.len + 1))
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((stdSimplex.obj n).op.map f ≫
                Iso.hom
                  ((fun (d : SimplexCategoryᵒᵖ) ↦
                      (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
                    d')))
            g :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i :
      Fin (n.len + 1))
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.hom
                  ((fun (d : SimplexCategoryᵒᵖ) ↦
                      (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
                    d) ≫
                (stdSimplex.obj n).map f))
            g :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i :
      Fin (n.len + 1))
Tactic: refine stdSimplex.ext _ _ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
⊢ Eq (α := Fin (n.len + 1))
    ((((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d') → (stdSimplex.obj n).obj d')
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).op.map f) :
                    (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).op.obj d')
                  g :
                (stdSimplex.obj n).op.obj d') :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i :
      Fin (n.len + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
                (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
              ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
                (stdSimplex.obj n).obj d) :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i :
      Fin (n.len + 1))
have h : Eq (α := Fin (n.len + 1))
  (Fin.rev
    ((((opObjEquiv : (a : Δ[n.len].op _⦋d'.1.len⦌) → Δ[n.len] _⦋d'.1.len⦌)
            ((Equiv.symm opObjEquiv :
                  (a : (stdSimplex.obj n).obj (op (rev.obj (unop d')))) →
                    (stdSimplex.obj n).op.obj (op (rev.obj (unop d'))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                      (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d))))) →
                        (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d')))))
                    ((opObjEquiv :
                          (a : (stdSimplex.obj n).op.obj (op (rev.obj (unop d)))) →
                            (stdSimplex.obj n).obj (op (rev.obj (unop d))))
                        g :
                      (stdSimplex.obj n).obj (op (rev.obj (unop d)))) :
                  (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d'))))) :
              (stdSimplex.obj n).op.obj (op (rev.obj (unop d')))) :
          Δ[n.len] _⦋len d'.1⦌) :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i.rev))
  ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
            (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
          ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
            (stdSimplex.obj n).obj d) :
        (stdSimplex.obj n).obj d') :
      (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
    i)
Tactic: rw [stdSimplex.opObjEquiv_apply, op_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
⊢ Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d))))) →
                  (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d')))))
              ((opObjEquiv :
                    (a : (stdSimplex.obj n).op.obj (op (rev.obj (unop d)))) →
                      (stdSimplex.obj n).obj (op (rev.obj (unop d))))
                  g :
                (stdSimplex.obj n).obj (op (rev.obj (unop d)))) :
            (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj (op (rev.obj (unop d'))))) :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i.rev))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)
have h : Eq (α := Fin (n.len + 1))
  (Fin.rev
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g : (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i.rev))
  ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
            (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
          ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
            (stdSimplex.obj n).obj d) :
        (stdSimplex.obj n).obj d') :
      (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
    i)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (len d'.1 + 1)
⊢ Eq (α := Fin (n.len + 1))
    (Fin.rev
      ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map (rev.map f.unop).op) :
                (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
              ((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
                (stdSimplex.obj n).obj d) :
            (stdSimplex.obj n).obj d') :
          (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
        i.rev))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
              (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
            ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
              (stdSimplex.obj n).obj d) :
          (stdSimplex.obj n).obj d') :
        (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
      i)
have h : Eq (α := Fin (n.len + 1))
  (Fin.rev
    ((((opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g : (stdSimplex.obj n).obj d) :
        (a : Fin (d.1.len + 1)) → Fin (n.len + 1))
      (Fin.rev
        ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f.unop :
            (a : Fin (d'.1.len + 1)) → Fin (d.1.len + 1))
          i.rev.rev))))
  ((((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
            (a : (stdSimplex.obj n).obj d) → (stdSimplex.obj n).obj d')
          ((stdSimplex.opObjEquiv : (a : (stdSimplex.obj n).op.obj d) → (stdSimplex.obj n).obj d) g :
            (stdSimplex.obj n).obj d) :
        (stdSimplex.obj n).obj d') :
      (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
    i)
Tactic: rw [map_rev_map_op_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have neg : j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
neg : j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 0 1
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have pos₁ : ¬j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
neg : j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 0 1
pos₁ : ¬j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 1 0
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have neg₁ : ¬j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
      (objMk₁ i) =
    objMk₁ (i.castPred ⋯)
have h₁ : ∀ (k : Fin (n + 1)),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ (i.castPred sorry) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
      (objMk₁ i) =
    objMk₁ (i.pred ⋯)
have h₁ : ∀ (k : Fin (n + 1)),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ (i.pred sorry) : (a : Fin (n + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
      (objMk₁ i) =
    objMk₁ i.castSucc
have h₁ : ∀ (k : Fin (n + 1 + 1)),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ i.castSucc : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
        (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
      (objMk₁ i) =
    objMk₁ i.succ
have h₁ : ∀ (k : Fin (n + 1 + 1)),
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Δ[1] j) :
                (a : (fun (X : Type u) ↦ X) (Δ[1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌))
              (objMk₁ i) :
            (fun (X : Type u) ↦ X) (Δ[1] _⦋n + 1⦌)) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((objMk₁ i.succ : (a : Fin (n + 1 + 1)) → Fin (1 + 1)) k : Fin (HAdd.hAdd (α := ℕ) 1 1))
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
inst : X.IsStrictSegal
d : ℕ
hd : ⦋d + 1⦌.len ≤ n + 1
x y : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋d + 1⦌ hd))
h :
  ∀ (i : Fin (d + 1)),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hd))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋d + 1⦌, property := hd }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hd))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋d + 1⦌, property := hd }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
          y :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
⊢ X.spine (d + 1) hd x = X.spine (d + 1) hd y
have h₁ : ∀ (i : Fin (d + 1)), (X.spine (d + 1) hd x).arrow i = (X.spine (d + 1) hd y).arrow i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
⊢ f = g
have w : ∀ (m : SimplexCategory) (hm : m.len ≤ n + 1)
  (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
      x
Tactic: ext ⟨⟨m, hm⟩⟩ x