awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : j < i.castSucc
⊢ stdSimplex.δ j ≫ r.map = const x
have rw : Eq (α := Δ[n] ⟶ X) (const x) (const x)
Tactic: rw [δ_map_of_lt _ j hj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : i.succ < j
⊢ stdSimplex.δ j ≫ r.map = const x
have rw : Eq (α := Δ[n] ⟶ X) (const x) (const x)
Tactic: rw [δ_map_of_gt _ j hj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.castSucc.succ < j
⊢ stdSimplex.δ j ≫ h.map = const x
have hj₁ : i.succ.succ ≤ j
Tactic: rw [Fin.succ_castSucc, Fin.castSucc_lt_iff_succ_le] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
⊢ stdSimplex.δ j ≫ h.map = const x
have inl : ∀ (hj : i.succ.succ ≤ i.succ.succ), stdSimplex.δ i.succ.succ ≫ h.map = const x
Tactic: obtain rfl | hj := hj.eq_or_lt
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
inl : ∀ (hj : i.succ.succ ≤ i.succ.succ), stdSimplex.δ i.succ.succ ≫ h.map = const x
⊢ stdSimplex.δ j ≫ h.map = const x
have inr : ∀ (hj : i.succ.succ < j), stdSimplex.δ j ≫ h.map = const x
Tactic: obtain rfl | hj := hj.eq_or_lt
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
⊢ stdSimplex.δ i.castSucc.succ ≫ h.map = f.map
have rw : stdSimplex.δ i.succ.castSucc ≫ h.map = f.map
Tactic: rw [← Fin.castSucc_succ, h.δ_castSucc_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
rw : stdSimplex.δ i.succ.castSucc ≫ h.map = f.map
⊢ stdSimplex.δ i.castSucc.succ ≫ h.map = f.map
have rw₁ : f.map = f.map
Tactic: rw [← Fin.castSucc_succ, h.δ_castSucc_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.succ.castSucc
⊢ stdSimplex.δ j ≫ h.map = const x
have hj₁ : j < i.castSucc.succ
Tactic: rw [← Fin.succ_castSucc] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
⊢ stdSimplex.δ j ≫ h.map = const x
have inl : ∀ (hj : i.castSucc.castSucc < i.castSucc.succ), stdSimplex.δ i.castSucc.castSucc ≫ h.map = const x
Tactic: obtain rfl | hj := (Fin.le_castSucc_iff.mpr hj).eq_or_lt
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
inl : ∀ (hj : i.castSucc.castSucc < i.castSucc.succ), stdSimplex.δ i.castSucc.castSucc ≫ h.map = const x
⊢ stdSimplex.δ j ≫ h.map = const x
have inr : ∀ (hj : j < i.castSucc.castSucc), stdSimplex.δ j ≫ h.map = const x
Tactic: obtain rfl | hj := (Fin.le_castSucc_iff.mpr hj).eq_or_lt
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (hypothesis)
Goal:
S : SSet
inst : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ ∃ (σ : Δ[n + 1] ⟶ S), σ₀ = Λ[n + 1, i].ι ≫ σ
have sq' : CommSq (Z := ⊤_ SSet) σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])
Tactic: have sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from _) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst : X.KanComplex
hf : horn.IsCompatible f
⊢ ∃ (φ : Δ[n + 1] ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
have obtain : ∀ (φ : Δ[n + 1] ⟶ X) (hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj),
  Eq (α := Δ[n + 1] ⟶ ⊤_ SSet) (φ ≫ terminal.from X) (terminal.from Δ[n + 1]) →
    ∃ (φ : Δ[n + 1] ⟶ X), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
Tactic: obtain ⟨φ, hφ, _⟩ := hf.exists_lift (terminal.from _) (terminal.from _) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (goal)
Goal:
Z : SSet
⊢ Z.KanComplex ↔
    ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
      horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
have refine : ∀
  (h :
    ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
      horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj),
  fibrations SSet (Y := ⊤_ SSet) (terminal.from Z)
Tactic: refine ⟨fun _ n i f hf ↦ hf.exists_lift_of_kanComplex,
    fun h ↦ (isFibrant_iff _).2 ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (hypothesis)
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X Y : SSet
g : X ⟶ Y
hf : J g
⊢ HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)
have hf₁ : ∃ (i : ℕ),
  MorphismProperty.ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦
    Δ[i + 1]) (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) g
Tactic: simp only [J, MorphismProperty.iSup_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (goal)
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X Y : SSet
g : X ⟶ Y
hf :
  ∃ (i : ℕ),
    MorphismProperty.ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦
      Δ[i + 1]) (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) g
⊢ HasLiftingProperty (Y := ⊤_ SSet) g (terminal.from Z)
have obtain : ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : Fin (n + 2)), HasLiftingProperty (Y := ⊤_ SSet) Λ[n + 1, i].ι (terminal.from Z)
Tactic: obtain ⟨n, ⟨i⟩⟩ := hf
Cleared hypotheses: X, Y, g, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (goal)
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ HasLiftingProperty (Y := ⊤_ SSet) Λ[n + 1, i].ι (terminal.from Z)
have refine : ∀ {t : Λ[n + 1, i].toSSet ⟶ Z} {x : Δ[n + 1] ⟶ ⊤_ SSet} (x_1 : CommSq t Λ[n + 1, i].ι (terminal.from Z) x), x_1.HasLift
Tactic: refine ⟨fun {t _} _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex (goal)
Goal:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ (φ : Δ[n + 1] ⟶ Z), ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x : Δ[n + 1] ⟶ ⊤_ SSet
h_1 : CommSq t Λ[n + 1, i].ι (terminal.from Z) x
⊢ h_1.HasLift
have obtain : ∀ (φ : Δ[n + 1] ⟶ Z) (hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t), h_1.HasLift
Tactic: obtain ⟨φ, hφ⟩ := h _ (horn.IsCompatible.of_hom t)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms (goal)
Goal:
⊢ IsStableUnderCobaseChange.{u_1, u_1 + 1} (C := SimplexCategoryᵒᵖ ⥤ Type u_1)
    (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u_1))
have rw : IsStableUnderCobaseChange (C := SimplexCategoryᵒᵖ ⥤ Type u_1)
  (functorCategory (monomorphisms (Type u_1)) SimplexCategoryᵒᵖ)
Tactic: rw [← functorCategory_monomorphisms]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms (goal)
Goal:
J : Type u
x : Category.{u, u} J
h : IsFiltered J
⊢ IsStableUnderColimitsOfShape (C := SimplexCategoryᵒᵖ ⥤ Type u) (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u)) J
have rw : IsStableUnderColimitsOfShape (C := SimplexCategoryᵒᵖ ⥤ Type u)
  (functorCategory (monomorphisms (Type u)) SimplexCategoryᵒᵖ) J
Tactic: rw [← functorCategory_monomorphisms]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (ComposableArrows.left.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0 + 1⦌))
          (ComposableArrows.mk₀ x)))
      (ComposableArrows.right.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0 + 1⦌))
          (ComposableArrows.mk₀ x))))
    (ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0 + 1⦌))
        (ComposableArrows.mk₀ x)))
    (eqToHom ⋯ ≫ ComposableArrows.hom (ComposableArrows.mk₁ (𝟙 x)) ≫ eqToHom ⋯)
have simp : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C)
    (ComposableArrows.left.{v, u} (n := 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
          (a : ComposableArrows C 0) → ComposableArrows C 1)
        (ComposableArrows.mk₀ x)))
    (ComposableArrows.right.{v, u} (n := 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
          (a : ComposableArrows C 0) → ComposableArrows C 1)
        (ComposableArrows.mk₀ x))))
  (ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
          (a : ComposableArrows C 0) → ComposableArrows C 1)
        (ComposableArrows.mk₀ x)) :
    Quiver.Hom.{v, u} (V := C)
      (ComposableArrows.left.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x)))
      (ComposableArrows.right.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x))))
  (eqToHom sorry :
    Quiver.Hom.{v, u} (V := C)
      (ComposableArrows.left.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x)))
      (ComposableArrows.right.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x))))
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ f).hom ≫ eqToHom ⋯
have simp : ComposableArrows.hom
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : ComposableArrows C 2) → ComposableArrows C 1)
      (ComposableArrows.mk₂ f g)) =
  f
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ g).hom ≫ eqToHom ⋯
have simp : ComposableArrows.hom
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : ComposableArrows C 2) → ComposableArrows C 1)
      (ComposableArrows.mk₂ f g)) =
  g
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (f ≫ g)).hom ≫ eqToHom ⋯
have simp : ComposableArrows.hom
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
        (a : ComposableArrows C 2) → ComposableArrows C 1)
      (ComposableArrows.mk₂ f g)) =
  f ≫ g
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ ComposableArrows.left e.edge = (nerveEquiv : (a : ComposableArrows C 0) → C) x
have simp : ComposableArrows.left e.edge =
  (nerveEquiv : (a : ComposableArrows C 0) → C)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : nerve C _⦋0 + 1⦌) → nerve C _⦋0⦌)
        e.edge :
      nerve.{v, u} C _⦋0⦌)
Tactic: simp only [← e.src_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ ComposableArrows.right e.edge = (nerveEquiv : (a : ComposableArrows C 0) → C) y
have simp : ComposableArrows.right e.edge =
  (nerveEquiv : (a : ComposableArrows C 0) → C)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
          (a : nerve C _⦋0 + 1⦌) → nerve C _⦋0⦌)
        e.edge :
      nerve.{v, u} C _⦋0⦌)
Tactic: simp only [← e.tgt_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : ComposableArrows.{v, u} C 0
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C))
    ((homEquiv :
          (a : Edge x x) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) x ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) x)
        (Edge.id x) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C))
    (𝟙 ((nerveEquiv : (a : ComposableArrows C 0) → C) x) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C))
have obtain : ∀ (x : C),
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
        C))
    ((homEquiv :
          (a :
              Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x)
                ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x)) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x) ⟶
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x))
        (Edge.id ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C))
    (𝟙
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0)) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C))
Tactic: obtain ⟨x, rfl⟩ := nerveEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
⊢ Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) ↔ f₀₁ ≫ f₁₂ = f₀₂
have refine : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) →
  ∀ (h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)), f₀₁ ≫ f₁₂ = f₀₂
Tactic: refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨by rwa [← h]⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ f₀₁ ≫ f₁₂ = f₀₂
have rw : Arrow.mk (f₀₁ ≫ f₁₂) = Arrow.mk f₀₂
Tactic: rw [← Arrow.mk_inj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ Arrow.mk (f₀₁ ≫ f₁₂) = Arrow.mk f₀₂
have a : Eq (α := ComposableArrows.{v, u} C 1)
  ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk (f₀₁ ≫ f₁₂)) :
    ComposableArrows.{v, u} C 1)
  ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
    ComposableArrows.{v, u} C 1)
Tactic: apply ComposableArrows.arrowEquiv.symm.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk (f₀₁ ≫ f₁₂)) :
      ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)
have h₁ : ComposableArrows.{v, u} C 1 = (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌) →
  Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk (f₀₁ ≫ f₁₂)) :
      ComposableArrows.{v, u} C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h'.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))
Tactic: convert_to (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₁ :
  ComposableArrows.{v, u} C 1 = (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌) →
    Eq (α := ComposableArrows.{v, u} C 1)
      ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk (f₀₁ ≫ f₁₂)) :
        ComposableArrows.{v, u} C 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
            (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
          h'.simplex :
        (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk (f₀₁ ≫ f₁₂)) :
      ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)
have h₂ : ComposableArrows.{v, u} C 1 = (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌) →
  Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))
Tactic: convert_to (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex