awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
pos :
  ∀ (hi : i < x),
    map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
      i.succ.castSucc.succAbove x.castSucc
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
have neg : ∀ (hi : x ≤ i),
  map' { toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
Tactic: by_cases! hi : i < x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
have pos : x.castSucc ≤
    Fin.castSucc
      (({ toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } : (a : Fin (n + 1 + 1)) → Fin (n + 1))
        x.succ) ∧
  ∀ i_1 < x.succ,
    Fin.castSucc
        (({ toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          i_1) <
      x.castSucc
Tactic: rw [Fin.succAbove_of_le_castSucc _ _ (by simpa), Fin.succ_castSucc, map'_eq_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x.castSucc ≤
      Fin.castSucc
        (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          x.succ) ∧
    ∀ i_1 < x.succ,
      Fin.castSucc
          (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            i_1) <
        x.castSucc
have pos : x ≤ i.predAbove x.succ ∧ ∀ i_1 < x.succ, i.predAbove i_1 < x
Tactic: simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ i.predAbove x.succ ∧ ∀ i_1 < x.succ, i.predAbove i_1 < x
have pos : x ≤ i.predAbove x.succ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
pos : x ≤ i.predAbove x.succ
⊢ x ≤ i.predAbove x.succ ∧ ∀ i_1 < x.succ, i.predAbove i_1 < x
have pos₁ : ∀ i_1 < x.succ, i.predAbove i_1 < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ i.predAbove x.succ
have pos : x ≤ x.succ.pred sorry
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
pos : x ≤ x.succ.pred ⋯
⊢ x ≤ i.predAbove x.succ
have pos₁ : x ≤ x
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
⊢ i.predAbove j < x
have pos : ∀ (h : i.castSucc < j), i.predAbove j < x
Tactic: by_cases! h : i.castSucc < j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
pos : ∀ (h : i.castSucc < j), i.predAbove j < x
⊢ i.predAbove j < x
have neg : ∀ (h : j ≤ i.castSucc), i.predAbove j < x
Tactic: by_cases! h : i.castSucc < j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ i.predAbove j < x
have pos : j.pred sorry < x
Tactic: rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
pos : j.pred ⋯ < x
⊢ i.predAbove j < x
have pos₁ : (j.pred sorry).succ < x.succ
Tactic: rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x
have neg : j < x.castSucc
Tactic: rw [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
have neg : x.castSucc ≤
    Fin.castSucc
      (({ toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } : (a : Fin (n + 1 + 1)) → Fin (n + 1))
        x.castSucc) ∧
  ∀ i_1 < x.castSucc,
    Fin.castSucc
        (({ toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          i_1) <
      x.castSucc
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa), map'_eq_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤
      Fin.castSucc
        (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          x.castSucc) ∧
    ∀ i_1 < x.castSucc,
      Fin.castSucc
          (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            i_1) <
        x.castSucc
have neg : x ≤ i.predAbove x.castSucc ∧ ∀ i_1 < x.castSucc, i.predAbove i_1 < x
Tactic: simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x ≤ i.predAbove x.castSucc ∧ ∀ i_1 < x.castSucc, i.predAbove i_1 < x
have neg : x ≤ i.predAbove x.castSucc
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
neg : x ≤ i.predAbove x.castSucc
⊢ x ≤ i.predAbove x.castSucc ∧ ∀ i_1 < x.castSucc, i.predAbove i_1 < x
have neg₁ : ∀ i_1 < x.castSucc, i.predAbove i_1 < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
⊢ i.predAbove j < x
have pos : ∀ (h : i.castSucc < j), i.predAbove j < x
Tactic: by_cases! h : i.castSucc < j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
pos : ∀ (h : i.castSucc < j), i.predAbove j < x
⊢ i.predAbove j < x
have neg : ∀ (h : j ≤ i.castSucc), i.predAbove j < x
Tactic: by_cases! h : i.castSucc < j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : i.castSucc < j
⊢ i.predAbove j < x
have pos : j < x.succ
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
⊢ i.predAbove j < x
have neg : j.castPred sorry < x
Tactic: rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
neg : j.castPred ⋯ < x
⊢ i.predAbove j < x
have neg₁ : (j.castPred sorry).castSucc < x.castSucc
Tactic: rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 2)
hz : z ∈ finset f y
⊢ z ∈ finset f x
have inl : ∀ (z : Fin (n + 1)) (hz : z.castSucc ∈ finset f y), z.castSucc ∈ finset f x
Tactic: obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 2)
hz : z ∈ finset f y
inl : ∀ (z : Fin (n + 1)) (hz : z.castSucc ∈ finset f y), z.castSucc ∈ finset f x
⊢ z ∈ finset f x
have inr : ∀ (hz : Fin.last (n + 1) ∈ finset f y), Fin.last (n + 1) ∈ finset f x
Tactic: obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 1)
hz : z.castSucc ∈ finset f y
⊢ z.castSucc ∈ finset f x
have inl : ∀ (hz : y ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)),
  x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)
Tactic: simp only [castSucc_mem_finset_iff] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : SimplexCategory
⊢ Quiver.Hom.unop
      (op
        (Hom.mk
          { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ :
            Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋n.len + 1⦌)).len + 1) })) =
    Quiver.Hom.unop (𝟙 (op ⦋n.len + 1⦌))
have a : ∀ (x : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)),
  Eq (α := Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                (Hom.mk
                  { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := sorry :
                    Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋n.len + 1⦌)).len + 1) }))) :
          (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
    ((Hom.toOrderHom (Quiver.Hom.unop (𝟙 (op ⦋n.len + 1⦌))) :
          (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
m n p : SimplexCategory
f : m ⟶ n
g : n ⟶ p
⊢ Quiver.Hom.unop
      (op
        (Hom.mk
          { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ :
            Fin ((unop (op ⦋p.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) })) =
    Quiver.Hom.unop
      (op
          (Hom.mk
            { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ :
              Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }) ≫
        op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ }))
have a : ∀ (x : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)),
  Eq (α := Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                (Hom.mk
                  { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := sorry :
                    Fin ((unop (op ⦋p.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }))) :
          (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                  (Hom.mk
                    { toFun := II.map' (Hom.toOrderHom f), monotone' := sorry :
                      Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }) ≫
                op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := sorry }))) :
          (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ (II.δ i).unop = (σ i).op.unop
have a : ∀ (x : Fin ((unop (II ^⦋n + 1⦌)).len + 1)),
  Eq (α := Fin ((unop (II ^⦋n⦌)).len + 1))
    ((Hom.toOrderHom (II.δ i).unop : (a : Fin ((unop (II ^⦋n + 1⦌)).len + 1)) → Fin ((unop (II ^⦋n⦌)).len + 1)) x :
      Fin ((unop (II ^⦋n⦌)).len + 1))
    ((Hom.toOrderHom (σ i).op.unop : (a : Fin ((unop (II ^⦋n + 1⦌)).len + 1)) → Fin ((unop (II ^⦋n⦌)).len + 1)) x :
      Fin ((unop (II ^⦋n⦌)).len + 1))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (II.σ i).unop = (δ i.succ.castSucc).op.unop
have a : ∀ (x : Fin ((unop (II ^⦋n⦌)).len + 1)),
  Eq (α := Fin ((unop (II ^⦋n + 1⦌)).len + 1))
    ((Hom.toOrderHom (II.σ i).unop : (a : Fin ((unop (II ^⦋n⦌)).len + 1)) → Fin ((unop (II ^⦋n + 1⦌)).len + 1)) x :
      Fin ((unop (II ^⦋n + 1⦌)).len + 1))
    ((Hom.toOrderHom (δ i.succ.castSucc).op.unop :
          (a : Fin ((unop (II ^⦋n⦌)).len + 1)) → Fin ((unop (II ^⦋n + 1⦌)).len + 1))
        x :
      Fin ((unop (II ^⦋n + 1⦌)).len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ :
  A₁.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) =
    A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
⊢ unop (A₁.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) =
    unop (A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
have rw : unop (A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) =
  unop (A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A₁ A₂ : IndexSet Δ
h₁ :
  A₁.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) =
    A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
h₂ : A₁.e ≫ eqToHom ⋯ = A₂.e
⊢ A₁ = A₂
have rcases : ∀ (Δ₁ : SimplexCategoryᵒᵖ) (α₁ : unop Δ ⟶ unop Δ₁) (hα₁ : Epi α₁)
  (h₁ :
    Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) =
      A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
  (h₂ :
    e
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) ≫
        eqToHom sorry =
      A₂.e),
  Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁) =
    A₂
Tactic: rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
Cleared hypotheses: A₁, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
h₁ :
  Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) =
    A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
h₂ :
  e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) ≫
      eqToHom ⋯ =
    A₂.e
⊢ Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁) =
    A₂
have rcases : ∀ (Δ₂ : SimplexCategoryᵒᵖ) (α₂ : unop Δ ⟶ unop Δ₂) (hα₂ : Epi α₂)
  (h₁ :
    Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) =
      Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂)))
  (h₂ :
    e
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) ≫
        eqToHom sorry =
      e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))),
  Eq (α := IndexSet Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))
Tactic: rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
Cleared hypotheses: A₂, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ :
  Eq (α :=
    unop Δ ⟶
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))))
    (CategoryStruct.comp (Y :=
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))))
      (e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)))
      (eqToHom ⋯))
    (e
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂)))
⊢ Eq (α := IndexSet Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))
have subst : ∀ (α₂ : unop Δ ⟶ unop Δ₁) (hα₂ : Epi α₂)
  (h₂ :
    Eq (α :=
      unop Δ ⟶
        unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
            (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
              (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))))
      (CategoryStruct.comp (Y :=
        unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
            (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
              (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))))
        (e
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)))
        (eqToHom sorry))
      (e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂)))),
  Eq (α := IndexSet Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))
Tactic: subst h₁
Cleared hypotheses: Δ₂, α₂, hα₂, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (hypothesis)
Goal:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ :
  Eq (α :=
    unop Δ ⟶
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))))
    (CategoryStruct.comp (Y :=
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))))
      (e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)))
      (eqToHom ⋯))
    (e
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂)))
⊢ Eq (α := IndexSet Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))
have h₃ : α₁ = α₂
Tactic: simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂
Cleared hypotheses: h₂