awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
have rw : X.δ i.succ ≫ X.δ i = X.δ i.succ ≫ X.δ i
Tactic: rw [δ_comp_δ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.σ j.succ ≫ X.δ i.castSucc = X.δ i ≫ X.σ j
have dsimp : X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
  X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)
have dsimp : X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)
have subst : X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)
have rw : Eq.{v + 1} (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌)) (𝟙 (X _⦋n⦌))
Tactic: rw [δ_comp_σ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)
have dsimp : X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _⦋n⦌)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)
have subst : X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)
have rw : Eq.{v + 1} (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌)) (𝟙 (X _⦋n⦌))
Tactic: rw [δ_comp_σ_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.σ j.castSucc ≫ X.δ i.succ = X.δ i ≫ X.σ j
have dsimp : X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
  X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.σ j ≫ X.δ i = X.δ (i.pred ⋯) ≫ X.σ (j.castLT ⋯)
have dsimp : X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
  X.map (SimplexCategory.δ (i.pred sorry)).op ≫ X.map (Quiver.Hom.op (SimplexCategory.σ (j.castLT sorry)))
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.σ j ≫ X.σ i.castSucc = X.σ i ≫ X.σ j.succ
have dsimp : X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op =
  X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension (obj (Truncated.sk n) (obj (truncation n) X))
    (NatTrans.app (Adjunction.unit ((SimplexCategory.Truncated.inclusion n).op.lanAdjunction C)) (obj (truncation n) X))
have rw : IsLeftKanExtension (obj (Truncated.sk n) (obj (truncation n) X))
  (NatTrans.app (SimplexCategory.Truncated.inclusion n).op.lanUnit (obj (truncation n) X))
Tactic: rw [lanAdjunction_unit]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst_2 :
  ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C),
    (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsRightKanExtension (obj (Truncated.cosk n) (obj (truncation n) X))
    (NatTrans.app (Adjunction.counit ((SimplexCategory.Truncated.inclusion n).op.ranAdjunction C))
      (obj (truncation n) X))
have rw : IsRightKanExtension (obj (Truncated.cosk n) (obj (truncation n) X))
  (NatTrans.app (SimplexCategory.Truncated.inclusion n).op.ranCounit (obj (truncation n) X))
Tactic: rw [ranAdjunction_counit]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
⊢ map (𝟭 (SimplicialObject.{v_1, u_1} D)) (whiskerRight η.left F) ≫
      { left := (obj (whiskering C D) F).obj (obj drop Y), right := F.obj (obj point Y),
          hom := whiskerRight Y.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ Y.right F) :
          Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom =
    { left := (obj (whiskering C D) F).obj (obj drop X_1), right := F.obj (obj point X_1),
          hom := whiskerRight X_1.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ X_1.right F) :
          Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom ≫
      map (const D) (F.map η.right)
have h : ∀ (n : SimplexCategoryᵒᵖ),
  (map (𝟭 (SimplicialObject.{v_1, u_1} D)) (whiskerRight η.left F) ≫
          { left := (obj (whiskering C D) F).obj (obj drop Y), right := F.obj (obj point Y),
              hom := whiskerRight Y.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ Y.right F) :
              Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom).app
      n =
    ({ left := (obj (whiskering C D) F).obj (obj drop X_1), right := F.obj (obj point X_1),
              hom := whiskerRight X_1.hom F ≫ Iso.hom (constComp SimplexCategoryᵒᵖ X_1.right F) :
              Comma (A := SimplicialObject.{v_1, u_1} D) (𝟭 (SimplicialObject.{v_1, u_1} D)) (const D) }.hom ≫
          map (const D) (F.map η.right)).app
      n
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
⊢ map (𝟭 (SimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η) ≫ ((whiskeringObj C D Y).obj A).hom =
    ((whiskeringObj C D X_1).obj A).hom ≫ map (const D) (η.app (obj point A))
have h : ∀ (n : SimplexCategoryᵒᵖ),
  (map (𝟭 (SimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
    (((whiskeringObj C D X_1).obj A).hom ≫ map (const D) (η.app (obj point A))).app n
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
⊢ (map (𝟭 (SimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
    (((whiskeringObj C D X_1).obj A).hom ≫ map (const D) (η.app (obj point A))).app n
have h : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) ≫ 𝟙 (Y.obj A.right) =
  (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
⊢ η.app (A.left.obj n) ≫ Y.map (A.hom.app n) ≫ 𝟙 (Y.obj A.right) =
    (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
have h : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
Tactic: rw [Category.comp_id, Category.comp_id, η.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
h : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
⊢ η.app (A.left.obj n) ≫ Y.map (A.hom.app n) ≫ 𝟙 (Y.obj A.right) =
    (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
have h₁ : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = X_1.map (A.hom.app n) ≫ η.app A.right
Tactic: rw [Category.comp_id, Category.comp_id, η.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
n : SimplexCategoryᵒᵖ
h : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
h₁ : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = X_1.map (A.hom.app n) ≫ η.app A.right
⊢ η.app (A.left.obj n) ≫ Y.map (A.hom.app n) ≫ 𝟙 (Y.obj A.right) =
    (X_1.map (A.hom.app n) ≫ 𝟙 (X_1.obj A.right)) ≫ η.app A.right
have h₂ : η.app (A.left.obj n) ≫ Y.map (A.hom.app n) = η.app (A.left.obj n) ≫ Y.map (A.hom.app n)
Tactic: rw [Category.comp_id, Category.comp_id, η.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y Z : Functor.{v, v', u, u'} C D
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
⊢ {
      app := fun (A : Augmented.{v, u} C) ↦
        { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := ⋯ :
          CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
      naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) } =
    {
        app := fun (A : Augmented.{v, u} C) ↦
          { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := ⋯ :
            CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
        naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
      {
        app := fun (A : Augmented.{v, u} C) ↦
          { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := ⋯ },
        naturality := ⋯ }
have w : ∀ (x_2 : Augmented.{v, u} C) (n : SimplexCategoryᵒᵖ),
  ({
                app := fun (A : Augmented.{v, u} C) ↦
                  { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := sorry :
                    CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
                naturality := sorry : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) }.app
            x_2).left.app
      n =
    NatTrans.app
      (CommaMorphism.left
        (NatTrans.app
          ({
              app := fun (A : Augmented.{v, u} C) ↦
                { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := sorry :
                  CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
              naturality := sorry : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
            {
              app := fun (A : Augmented.{v, u} C) ↦
                { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := sorry },
              naturality := sorry })
          x_2))
      n
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : SimplicialObject.{v, u} C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ (obj (𝟭 (SimplicialObject.{v, u} C)) X).map g ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f =
    (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ map (obj (const C) X₀) g
have dsimp : X.map g ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f = (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 X : SimplicialObject.{v, u} C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f = (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀
have rw : X.map g.unop.op ≫ X.map (Quiver.Hom.op (⦋0⦌.const (unop j) 0)) ≫ f =
  (X.map (Quiver.Hom.op (⦋0⦌.const (unop i) 0)) ≫ f) ≫ 𝟙 X₀
Tactic: rw [← g.op_unop]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n m : ℕ
h : n = m
⊢ ⦋n⦌ = ⦋m⦌
have rw : ⦋m⦌ = ⦋m⦌
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ i.castSucc
have dsimp : X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j.succ) =
  X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i.castSucc)
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ i ≫ X.δ j = X.δ (j.pred ⋯) ≫ X.δ i.castSucc
have dsimp : X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
  X.map (SimplexCategory.δ (j.pred sorry)) ≫ X.map (SimplexCategory.δ i.castSucc)
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.δ (i.castLT ⋯) ≫ X.δ j.succ = X.δ j ≫ X.δ i
have dsimp : X.map (SimplexCategory.δ (i.castLT sorry)) ≫ X.map (SimplexCategory.δ j.succ) =
  X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ
have dsimp : X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.castSucc) =
  X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.succ)
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ
have subst : X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ
have rw : X.δ i ≫ X.δ i.succ = X.δ i ≫ X.δ i.succ
Tactic: rw [δ_comp_δ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.δ i.castSucc ≫ X.σ j.succ = X.σ j ≫ X.δ i
have dsimp : X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ j.succ) =
  X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)
have dsimp : X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)
have subst : X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)
have rw : Eq.{v + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n⦌) (𝟙 (X ^⦋n⦌)) (𝟙 (X ^⦋n⦌))
Tactic: rw [δ_comp_σ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)
have dsimp : X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)
have subst : X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)
have rw : Eq.{v + 1} (α := X ^⦋n⦌ ⟶ X ^⦋n⦌) (𝟙 (X ^⦋n⦌)) (𝟙 (X ^⦋n⦌))
Tactic: rw [δ_comp_σ_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.δ i.succ ≫ X.σ j.castSucc = X.σ j ≫ X.δ i
have dsimp : X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ j.castSucc) =
  X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.δ i ≫ X.σ j = X.σ (j.castLT ⋯) ≫ X.δ (i.pred ⋯)
have dsimp : X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
  X.map (SimplexCategory.σ (j.castLT sorry)) ≫ X.map (SimplexCategory.δ (i.pred sorry))
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.σ i.castSucc ≫ X.σ j = X.σ j.succ ≫ X.σ i
have dsimp : X.map (SimplexCategory.σ i.castSucc) ≫ X.map (SimplexCategory.σ j) =
  X.map (SimplexCategory.σ j.succ) ≫ X.map (SimplexCategory.σ i)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
⊢ map (const D) (F.map η.left) ≫
      { left := F.obj (obj point Y), right := (obj (whiskering C D) F).obj (obj drop Y),
          hom := Iso.inv (constComp SimplexCategory (obj point Y) F) ≫ whiskerRight Y.hom F :
          Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom =
    { left := F.obj (obj point X_1), right := (obj (whiskering C D) F).obj (obj drop X_1),
          hom := Iso.inv (constComp SimplexCategory (obj point X_1) F) ≫ whiskerRight X_1.hom F :
          Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom ≫
      map (𝟭 (CosimplicialObject.{v_1, u_1} D)) (whiskerRight η.right F)
have h : ∀ (n : SimplexCategory),
  (map (const D) (F.map η.left) ≫
          { left := F.obj (obj point Y), right := (obj (whiskering C D) F).obj (obj drop Y),
              hom := Iso.inv (constComp SimplexCategory (obj point Y) F) ≫ whiskerRight Y.hom F :
              Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom).app
      n =
    ({ left := F.obj (obj point X_1), right := (obj (whiskering C D) F).obj (obj drop X_1),
              hom := Iso.inv (constComp SimplexCategory (obj point X_1) F) ≫ whiskerRight X_1.hom F :
              Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom ≫
          map (𝟭 (CosimplicialObject.{v_1, u_1} D)) (whiskerRight η.right F)).app
      n
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
n : SimplexCategory
⊢ (map (const D) (F.map η.left) ≫
          { left := F.obj (obj point Y), right := (obj (whiskering C D) F).obj (obj drop Y),
              hom := Iso.inv (constComp SimplexCategory (obj point Y) F) ≫ whiskerRight Y.hom F :
              Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom).app
      n =
    ({ left := F.obj (obj point X_1), right := (obj (whiskering C D) F).obj (obj drop X_1),
              hom := Iso.inv (constComp SimplexCategory (obj point X_1) F) ≫ whiskerRight X_1.hom F :
              Comma (const D) (𝟭 (CosimplicialObject.{v_1, u_1} D)) }.hom ≫
          map (𝟭 (CosimplicialObject.{v_1, u_1} D)) (whiskerRight η.right F)).app
      n
have h : F.map η.left ≫ 𝟙 (F.obj Y.left) ≫ F.map (Y.hom.app n) =
  (𝟙 (F.obj X_1.left) ≫ F.map (X_1.hom.app n)) ≫ F.map (η.right.app n)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X_1 Y : Augmented.{v, u} C
η : X_1 ⟶ Y
n : SimplexCategory
⊢ F.map η.left ≫ 𝟙 (F.obj Y.left) ≫ F.map (Y.hom.app n) =
    (𝟙 (F.obj X_1.left) ≫ F.map (X_1.hom.app n)) ≫ F.map (η.right.app n)
have h : F.map (η.left ≫ Y.hom.app n) = F.map (X_1.hom.app n ≫ η.right.app n)
Tactic: rw [Category.id_comp, Category.id_comp, ← F.map_comp, ← F.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : CosimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
A : Augmented.{v, u} C
⊢ map (const D) (η.app (obj point A)) ≫ ((whiskeringObj C D Y).obj A).hom =
    ((whiskeringObj C D X_1).obj A).hom ≫ map (𝟭 (CosimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η)
have h : ∀ (n : SimplexCategory),
  (map (const D) (η.app (obj point A)) ≫ ((whiskeringObj C D Y).obj A).hom).app n =
    (((whiskeringObj C D X_1).obj A).hom ≫ map (𝟭 (CosimplicialObject.{v', u'} D)) (whiskerLeft (obj drop A) η)).app n
Tactic: ext n