awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X_1 Y : SimplexCategoryᵒᵖ
x : X_1 ⟶ Y
⊢ Δ[m].map x ≫
      Iso.hom
        ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n)) Y) =
    Iso.hom
        ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n)) X_1) ≫
      X.map x
have h₁ : ∀ (x_1 : Δ[m].obj X_1),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Δ[m].map x ≫
          Iso.hom
            ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n)) Y)))
      x_1 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n))
              X_1) ≫
          X.map x))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.δ i) = face {i}ᶜ
have rw : Eq.{u + 1} (α := Δ[n + 1].Subcomplex)
  (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ i))) (face {i}ᶜ)
Tactic: rw [Subcomplex.range_eq_ofSimplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) s ↔
    StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
have rw : StrictMono.{0, u} (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := ULift.{u, 0} (Fin (n + 1)))
    (Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve.{u} n).hom.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋d⦌)) → (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (n + 1))) _⦋d⦌))
        s)) ↔
  StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
Tactic: rw [← nonDegenerate_iff_of_mono (isoNerve n).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) s ↔
    Mono (C := SimplexCategory) (X := unop (op ⦋d⦌)) (Y := ⦋n⦌)
      (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)
have rw : StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1)) ↔
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
Tactic: rw [mem_nonDegenerate_iff_strictMono,
    SimplexCategory.mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1)) ↔
    Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
        (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
have refine : ∀
  (h :
    Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
        (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))),
  StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
Tactic: refine ⟨fun h ↦ h.injective, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
have rw : ∀ (i : Fin d),
  LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
Tactic: rw [Fin.strictMono_iff_lt_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
i : Fin d
⊢ LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
have inl : ∀
  (h' :
    LT.lt (α := Fin (n + 1))
      ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
      ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)),
  LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
Tactic: obtain h' | h' := (stdSimplex.monotone_apply s i.castSucc_le_succ).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
i : Fin d
inl :
  ∀
    (h' :
      LT.lt (α := Fin (n + 1))
        ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
        ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)),
    LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
      ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
⊢ LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
have inr : ∀
  (h' :
    Eq (α := Fin (n + 1)) ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
      ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)),
  LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
Tactic: obtain h' | h' := (stdSimplex.monotone_apply s i.castSucc_le_succ).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n i : ℕ
hi : n + 1 ≤ i
⊢ Eq.{u + 1} (α := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) ⊤
have h : ∀ (x : Δ[n] _⦋i⦌),
  Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x ↔ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x ↔ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) ⊤ x
have h : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x
Tactic: simp only [Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x
have h : ∀ (hx : x ∉ Δ[n].degenerate i), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
⊢ Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)
have rwa : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].nonDegenerate i) x
Tactic: rwa [← mem_nonDegenerate_iff_mono]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (hypothesis)
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
⊢ False
have this : Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
  (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)
Tactic: have : Mono (objEquiv x) := by rwa [← mem_nonDegenerate_iff_mono]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (hypothesis)
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this :
  Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)
⊢ False
have this₁ : (unop (op ⦋i⦌)).len ≤ ⦋n⦌.len
Tactic: have := SimplexCategory.len_le_of_mono (objEquiv x)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
⊢ Fin n ≃ ↥{i, j}ᶜ
have refine_1 : ∀ (k : Fin n), Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove ((i.castPred sorry).succAbove k))
Tactic: refine Equiv.ofBijective
      (fun k ↦ ⟨j.succAbove ((i.castPred (Fin.ne_last_of_lt h)).succAbove k), ?_⟩)
        ⟨fun _ _ hk ↦ ?_, fun ⟨l, hl⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
refine_1 : ∀ (k : Fin n), Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove ((i.castPred ⋯).succAbove k))
⊢ Fin n ≃ ↥{i, j}ᶜ
have refine_2 : ∀ (x x_1 : Fin n)
  (hk :
    Eq (α := ↥{i, j}ᶜ)
      ((fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
        x)
      ((fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
        x_1)),
  x = x_1
Tactic: refine Equiv.ofBijective
      (fun k ↦ ⟨j.succAbove ((i.castPred (Fin.ne_last_of_lt h)).succAbove k), ?_⟩)
        ⟨fun _ _ hk ↦ ?_, fun ⟨l, hl⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
refine_1 : ∀ (k : Fin n), Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove ((i.castPred ⋯).succAbove k))
refine_2 :
  ∀ (x x_1 : Fin n)
    (hk :
      Eq (α := ↥{i, j}ᶜ)
        ((fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          x)
        ((fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          x_1)),
    x = x_1
⊢ Fin n ≃ ↥{i, j}ᶜ
have refine_3 : ∀ (x : ↥{i, j}ᶜ) (l : Fin (n + 2)) (hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ l),
  ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) l hl
Tactic: refine Equiv.ofBijective
      (fun k ↦ ⟨j.succAbove ((i.castPred (Fin.ne_last_of_lt h)).succAbove k), ?_⟩)
        ⟨fun _ _ hk ↦ ?_, fun ⟨l, hl⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x x_1 : Fin n
hk :
  Eq (α := ↥{i, j}ᶜ)
    ((fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      x)
    ((fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      x_1)
⊢ Eq (α := Fin (n + 1 + 1))
    ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb :
          (a : Fin n) → Fin (n + 1 + 1))
        x :
      Fin (n + 1 + 1))
    ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb :
          (a : Fin n) → Fin (n + 1 + 1))
        x_1 :
      Fin (n + 1 + 1))
have rwa : ∀
  (hk :
    Eq (α := Fin (n + 2))
      (↑((fun (k : Fin n) ↦
              Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
                (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
            x) :
        Fin (n + 2))
      (↑((fun (k : Fin n) ↦
              Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
                (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
            x_1) :
        Fin (n + 2))),
  Eq (α := Fin (n + 1 + 1))
    ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred sorry).succAboveOrderEmb j.succAboveOrderEmb :
          (a : Fin n) → Fin (n + 1 + 1))
        x :
      Fin (n + 1 + 1))
    ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred sorry).succAboveOrderEmb j.succAboveOrderEmb :
          (a : Fin n) → Fin (n + 1 + 1))
        x_1 :
      Fin (n + 1 + 1))
Tactic: rwa [Subtype.ext_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ l
⊢ ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) l hl
have refine_3 : ∀ (m : Fin (n + 1)) (hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)),
  ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m) hl
Tactic: obtain ⟨m, rfl⟩ : l ∈ Set.range j.succAbove := by
        grind [Fin.range_succAbove, mem_compl, Fin.succAbove]
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)
⊢ ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m) hl
have refine_3 : ∀ (k : Fin n) (hk : (i.castPred sorry).succAbove k = m),
  ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred sorry).succAbove k)) sorry)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m) hl
Tactic: obtain ⟨k, hk⟩ : m ∈ Set.range (i.castPred (Fin.ne_last_of_lt h)).succAbove := by
        grind [Fin.range_succAbove, compl_insert, Fin.succAbove, Fin.castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ (facePairComplIso i j h).hom ≫ Subcomplex.ι (face {i, j}ᶜ) = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i
have rw : stdSimplex.δ (i.castPred sorry) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred sorry) ≫ stdSimplex.δ i
Tactic: rw [facePairComplIso_hom_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ stdSimplex.δ (i.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i
have obtain : ∀ (i : Fin (n + 2)) (h : i.castSucc < j),
  stdSimplex.δ (i.castSucc.castPred sorry) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred sorry) ≫ stdSimplex.δ i.castSucc
Tactic: obtain ⟨i, rfl⟩ := i.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
h : i.castSucc < j
⊢ stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i.castSucc
have obtain : ∀ (j : Fin (n + 2)) (h : i.castSucc < j.succ),
  stdSimplex.δ (i.castSucc.castPred sorry) ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred sorry) ≫ stdSimplex.δ i.castSucc
Tactic: obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc
have dsimp : stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred sorry) ≫ stdSimplex.δ i.castSucc
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc
have rw : stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ j ≫ stdSimplex.δ i.castSucc
Tactic: rw [Fin.pred_succ, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
rw : stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ j ≫ stdSimplex.δ i.castSucc
⊢ stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc
have rw₁ : stdSimplex.δ j ≫ stdSimplex.δ i.castSucc = stdSimplex.δ j ≫ stdSimplex.δ i.castSucc
Tactic: rw [Fin.pred_succ, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
⊢ Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1}
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
        (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
      univ)
have dsimp : card (α := Fin (n + 1))
    (Finset.image (α := Fin (m + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
        (a : Fin (m + 1)) → Fin (n + 1))
      univ) =
  m + 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (hypothesis)
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
⊢ card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1))
        (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
          (a : Fin (m + 1)) → Fin (n + 1))
        univ) =
    m + 1
have hx₁ : Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
  (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
    (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
Tactic: rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1))
        (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
          (a : Fin (m + 1)) → Fin (n + 1))
        univ) =
    m + 1
have rw : card (α := Fin (m + 1)) univ = m + 1
Tactic: rw [Finset.card_image_of_injective _ (by exact hx), Finset.card_univ,
          Fintype.card_fin]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
rw : card (α := Fin (m + 1)) univ = m + 1
⊢ card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1))
        (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
          (a : Fin (m + 1)) → Fin (n + 1))
        univ) =
    m + 1
have rw₁ : Fintype.card (Fin (m + 1)) = m + 1
Tactic: rw [Finset.card_image_of_injective _ (by exact hx), Finset.card_univ,
          Fintype.card_fin]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
rw : card (α := Fin (m + 1)) univ = m + 1
rw₁ : Fintype.card (Fin (m + 1)) = m + 1
⊢ card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1))
        (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
          (a : Fin (m + 1)) → Fin (n + 1))
        univ) =
    m + 1
have rw₂ : m + 1 = m + 1
Tactic: rw [Finset.card_image_of_injective _ (by exact hx), Finset.card_univ,
          Fintype.card_fin]