awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RingDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
decreasing_by :
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree
have decreasing_by₁ : ∀
  (wf :
    LT.lt (α := WithBot ℕ)
      (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
      (↑p.natDegree : WithBot ℕ)),
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
Tactic: decreasing_by {
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}
Cleared hypotheses: wf
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Finset (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
⊢ 0 ∈ r • t ↔ 0 ∈ t
have rw : 0 ∈ (↑(r • t) : Set M) ↔ 0 ∈ t
Tactic: rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff hr, mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Finset (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
rw : 0 ∈ (↑(r • t) : Set M) ↔ 0 ∈ t
⊢ 0 ∈ r • t ↔ 0 ∈ t
have rw₁ : 0 ∈ r • (↑t : Set M) ↔ 0 ∈ t
Tactic: rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff hr, mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Finset (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
rw : 0 ∈ (↑(r • t) : Set M) ↔ 0 ∈ t
rw₁ : 0 ∈ r • (↑t : Set M) ↔ 0 ∈ t
⊢ 0 ∈ r • t ↔ 0 ∈ t
have rw₂ : 0 ∈ (↑t : Set M) ↔ 0 ∈ t
Tactic: rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff hr, mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Finset (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
rw : 0 ∈ (↑(r • t) : Set M) ↔ 0 ∈ t
rw₁ : 0 ∈ r • (↑t : Set M) ↔ 0 ∈ t
rw₂ : 0 ∈ (↑t : Set M) ↔ 0 ∈ t
⊢ 0 ∈ r • t ↔ 0 ∈ t
have rw₃ : 0 ∈ t ↔ 0 ∈ t
Tactic: rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff hr, mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Finset (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
have rw : 0 ∈ (↑s : Set R) ∧ (↑t : Set M).Nonempty ∨ 0 ∈ (↑t : Set M) ∧ (↑s : Set R).Nonempty ↔
  0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
Tactic: rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : HomotopicL f g
⊢ HomotopicL g f
have rcases : ∀ (hfg : f.CompStruct (Edge.id y) g), HomotopicL g f
Tactic: rcases hfg with ⟨hfg⟩
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : HomotopicL f g
hgh : HomotopicL g h
⊢ HomotopicL f h
have rcases : ∀ (hfg : f.CompStruct (Edge.id y) g), HomotopicL f h
Tactic: rcases hfg with ⟨hfg⟩
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hgh : HomotopicL g h
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL f h
have rcases : ∀ (hgh : g.CompStruct (Edge.id y) h), HomotopicL f h
Tactic: rcases hgh with ⟨hgh⟩
Cleared hypotheses: hgh
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : HomotopicR f g
⊢ HomotopicR g f
have rcases : ∀ (hfg : (Edge.id x).CompStruct f g), HomotopicR g f
Tactic: rcases hfg with ⟨hfg⟩
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : HomotopicR f g
hgh : HomotopicR g h
⊢ HomotopicR f h
have rcases : ∀ (hfg : (Edge.id x).CompStruct f g), HomotopicR f h
Tactic: rcases hfg with ⟨hfg⟩
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hgh : HomotopicR g h
hfg : (Edge.id x).CompStruct f g
⊢ HomotopicR f h
have rcases : ∀ (hgh : (Edge.id x).CompStruct g h), HomotopicR f h
Tactic: rcases hgh with ⟨hgh⟩
Cleared hypotheses: hgh
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : HomotopicL f g
⊢ HomotopicR f g
have rcases : ∀ (h : f.CompStruct (Edge.id y) g), HomotopicR f g
Tactic: rcases h with ⟨h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : HomotopicR f g
⊢ HomotopicL f g
have rcases : ∀ (h : (Edge.id x).CompStruct f g), HomotopicL f g
Tactic: rcases h with ⟨h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg : HomotopicL g g'
⊢ HomotopicL h h'
have rcases : ∀ (hg : (id y).CompStruct g g'), HomotopicL h h'
Tactic: rcases hg.homotopicR with ⟨hg⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
⊢ HomotopicL h h'
have rcases : ∀ (hf : f.CompStruct (id y) f'), HomotopicL h h'
Tactic: rcases hf with ⟨hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
⊢ HomotopicL h h'
have let : ∀ (s₁ : f.CompStruct g' h'), HomotopicL h h'
Tactic: let ⟨s₁⟩ := Quasicategory₂.fill32 hf (idComp g') s'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (goal)
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
s₁ : f.CompStruct g' h'
⊢ HomotopicL h h'
have let : ∀ (s₂ : f.CompStruct g h'), HomotopicL h h'
Tactic: let ⟨s₂⟩ := Quasicategory₂.fill31 (compId f) hg s₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated (hypothesis)
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
g : Edge y z
h : Edge x z
fac : ⟦f.comp g⟧ = ⟦h⟧
⊢ f.CompStruct g h
have fac₁ : f.comp g ≈ h
Tactic: rw [Quotient.eq_iff_equiv] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.δ₀Iter (i + 1) h = X.δ₀Iter i ⋯ ≫ X.δ 0
have dsimp : X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
  X.map (SimplexCategory.δ₀Iter i sorry).op ≫ X.map (Quiver.Hom.op (SimplexCategory.δ 0))
Tactic: dsimp [δ, δ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (Quiver.Hom.op (SimplexCategory.δ 0))
have rw : X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
  X.map ((SimplexCategory.δ₀Iter i sorry).op ≫ Quiver.Hom.op (SimplexCategory.δ 0))
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
rw :
  X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map ((SimplexCategory.δ₀Iter i ⋯).op ≫ Quiver.Hom.op (SimplexCategory.δ 0))
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (Quiver.Hom.op (SimplexCategory.δ 0))
have rw₁ : X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
rw :
  X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map ((SimplexCategory.δ₀Iter i ⋯).op ≫ Quiver.Hom.op (SimplexCategory.δ 0))
rw₁ : X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (Quiver.Hom.op (SimplexCategory.δ 0))
have rw₂ : X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i sorry).op =
  X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
⊢ X.δ j ≫ X.δ₀Iter i hi = X.δ₀Iter (i + 1) ⋯
have dsimp : X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) sorry).op
Tactic: dsimp [δ, δ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
have rw : X.map ((SimplexCategory.δ j).op ≫ (SimplexCategory.δ₀Iter i hi).op) = X.map (SimplexCategory.δ₀Iter (i + 1) sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.δ j).op ≫ (SimplexCategory.δ₀Iter i hi).op) = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
have rw₁ : X.map (SimplexCategory.δ₀Iter i hi ≫ SimplexCategory.δ j).op = X.map (SimplexCategory.δ₀Iter (i + 1) sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.δ j).op ≫ (SimplexCategory.δ₀Iter i hi).op) = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
rw₁ : X.map (SimplexCategory.δ₀Iter i hi ≫ SimplexCategory.δ j).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
have rw₂ : X.map (SimplexCategory.δ₀Iter (i + 1) sorry).op = X.map (SimplexCategory.δ₀Iter (i + 1) sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + j
⊢ X.δ i' ≫ X.δ₀Iter j ⋯ = X.δ₀Iter j ⋯ ≫ X.δ i
have dsimp : X.map (SimplexCategory.δ i').op ≫ X.map (SimplexCategory.δ₀Iter j sorry).op =
  X.map (SimplexCategory.δ₀Iter j sorry).op ≫ X.map (SimplexCategory.δ i).op
Tactic: dsimp [δ, δ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
⊢ X.σ j ≫ X.δ₀Iter (i + 1) hi = X.δ₀Iter i ⋯
have dsimp : X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i sorry).op
Tactic: dsimp [σ, δ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
have rw : X.map ((SimplexCategory.σ j).op ≫ (SimplexCategory.δ₀Iter (i + 1) hi).op) = X.map (SimplexCategory.δ₀Iter i sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.σ j).op ≫ (SimplexCategory.δ₀Iter (i + 1) hi).op) = X.map (SimplexCategory.δ₀Iter i ⋯).op
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
have rw₁ : X.map (SimplexCategory.δ₀Iter (i + 1) hi ≫ SimplexCategory.σ j).op = X.map (SimplexCategory.δ₀Iter i sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.σ j).op ≫ (SimplexCategory.δ₀Iter (i + 1) hi).op) = X.map (SimplexCategory.δ₀Iter i ⋯).op
rw₁ : X.map (SimplexCategory.δ₀Iter (i + 1) hi ≫ SimplexCategory.σ j).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
have rw₂ : X.map (SimplexCategory.δ₀Iter i sorry).op = X.map (SimplexCategory.δ₀Iter i sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.σ₀Iter (i + 1) h = X.σ 0 ≫ X.σ₀Iter i ⋯
have dsimp : X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
  X.map (Quiver.Hom.op (SimplexCategory.σ 0)) ≫ X.map (SimplexCategory.σ₀Iter i sorry).op
Tactic: dsimp [σ, σ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0)) ≫ X.map (SimplexCategory.σ₀Iter i ⋯).op
have rw : X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
  X.map (Quiver.Hom.op (SimplexCategory.σ 0) ≫ (SimplexCategory.σ₀Iter i sorry).op)
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ₀Iter_succ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
rw :
  X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0) ≫ (SimplexCategory.σ₀Iter i ⋯).op)
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0)) ≫ X.map (SimplexCategory.σ₀Iter i ⋯).op
have rw₁ : X.map (SimplexCategory.σ₀Iter (i + 1) h).op = X.map (SimplexCategory.σ₀Iter i sorry ≫ SimplexCategory.σ 0).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ₀Iter_succ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
rw :
  X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0) ≫ (SimplexCategory.σ₀Iter i ⋯).op)
rw₁ : X.map (SimplexCategory.σ₀Iter (i + 1) h).op = X.map (SimplexCategory.σ₀Iter i ⋯ ≫ SimplexCategory.σ 0).op
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0)) ≫ X.map (SimplexCategory.σ₀Iter i ⋯).op
have rw₂ : X.map (SimplexCategory.σ₀Iter i sorry ≫ SimplexCategory.σ 0).op =
  X.map (SimplexCategory.σ₀Iter i sorry ≫ SimplexCategory.σ 0).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ₀Iter_succ ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ₀Iter (i + 1) ⋯
have dsimp : X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) sorry).op
Tactic: dsimp [σ, σ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
⊢ X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
have rw : X.map ((SimplexCategory.σ₀Iter i hi).op ≫ (SimplexCategory.σ j).op) = X.map (SimplexCategory.σ₀Iter (i + 1) sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.σ₀Iter i hi).op ≫ (SimplexCategory.σ j).op) = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
⊢ X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
have rw₁ : X.map (SimplexCategory.σ j ≫ SimplexCategory.σ₀Iter i hi).op = X.map (SimplexCategory.σ₀Iter (i + 1) sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.σ₀Iter i hi).op ≫ (SimplexCategory.σ j).op) = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
rw₁ : X.map (SimplexCategory.σ j ≫ SimplexCategory.σ₀Iter i hi).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
⊢ X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
have rw₂ : X.map (SimplexCategory.σ₀Iter (i + 1) sorry).op = X.map (SimplexCategory.σ₀Iter (i + 1) sorry).op
Tactic: rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]