awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : Isδ₀ i
⊢ n' = n + 1

Tactic:
have h' : n' = n + 1 := hi.left
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : Isδ₀ i
h' : n' = n + 1
pos :
  ∀ (i : ⦋n⦌ ⟶ ⦋n + 1⦌) [inst_3 : Mono i] (h : ¬n = n + 1) (hi : Isδ₀ i),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n + 1⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n + 1⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)

Tactic:
subst h'
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (HomologicalComplex.d K[X] (n + 1) n : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n + 1⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)

Tactic:
simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀'
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (HomologicalComplex.d K[X] (n + 1) n : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)

Tactic:
rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]

Premises used: AlgebraicTopology.DoldKan.PInfty, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, HomologicalComplex.Hom.comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (∑ j : Fin (n + 2), HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)

Tactic:
simp only [Preadditive.comp_sum]

Premises used: CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
pos₁ :
  ∀ (b : Fin (n + 2)),
    Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b →
      b ≠ 0 →
        Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
          (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
pos₂ :
  0 ∉ Finset.univ →
    Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0))
      0
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (∑ j : Fin (n + 2), HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)

Tactic:
rw [Finset.sum_eq_single (0 : Fin (n + 2))]

Premises used: Finset.sum_eq_single, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
pos :
  Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b →
    b ≠ 0 →
      Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
⊢ Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b →
    b ≠ 0 →
      Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
rw : ¬b = 0
⊢ ¬Isδ₀ (SimplexCategory.δ b)

Tactic:
rw [Isδ₀.iff]

Premises used: AlgebraicTopology.DoldKan.Isδ₀.iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
⊢ ¬b = 0

Tactic:
hb
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
⊢ ¬b = 0

Tactic:
exact hb
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
pos :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ b) =
    0
pos₁ :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ b).op) =
    0
pos₂ :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      0 =
    0
pos₃ pos₄ : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) 0 0
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0

Tactic:
rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]

Premises used: zsmul_zero, SimplexCategory.δ, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ →
    Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0))
      0

Tactic:
simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]

Premises used: Finset.mem_univ, not_true, IsEmpty.forall_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ 0 : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := X _⦋n + 1⦌)
      (HomologicalComplex.Hom.f PInfty (n + 1) : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
      (X.map (Quiver.Hom.op (SimplexCategory.δ 0))))
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)

Tactic:
simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]

Premises used: AlgebraicTopology.DoldKan.Isδ₀.eq_δ₀, pow_zero, one_zsmul, Fin.val_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ 0 : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := X _⦋n + 1⦌)
      (HomologicalComplex.Hom.f PInfty (n + 1) : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
      (X.map (Quiver.Hom.op (SimplexCategory.δ 0))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
neg :
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌) (0 : X _⦋n'⦌ ⟶ X _⦋n⦌) (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
rw : ⦋n'⦌ ≠ ⦋n⦌
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)

Tactic:
rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
by_contra : ∀ (h' : ⦋n'⦌ = ⦋n⦌), False
⊢ ⦋n'⦌ ≠ ⦋n⦌

Tactic:
by_contra h'
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : ⦋n'⦌ = ⦋n⦌
⊢ False

Tactic:
h (congr_arg SimplexCategory.len h'.symm)

Premises used: congr_arg, Eq.symm, SimplexCategory.len
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : ⦋n'⦌ = ⦋n⦌
⊢ False

Tactic:
exact h (congr_arg SimplexCategory.len h'.symm)

Premises used: congr_arg, Eq.symm, SimplexCategory.len
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
neg : ⦋n⦌.len ≠ n'
neg₁ : ¬Isδ₀ i
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌) (0 : X _⦋n'⦌ ⟶ X _⦋n⦌) (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)

Tactic:
rw [PInfty_comp_map_mono_eq_zero]

Premises used: AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n⦌.len ≠ n'

Tactic:
h
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n⦌.len ≠ n'

Tactic:
exact h
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
h :
  ∀ (A : Splitting.IndexSet Δ),
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
        (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X.map θ ≫
          Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
              X.map A.e.op)
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
          (Splitting.cofan (Γ₀.splitting K[X]) Δ))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
        ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
              X.map A.e.op) ≫
          (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))
⊢ ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X.map θ ≫
      Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
          X.map A.e.op) =
    (Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
          X.map A.e.op) ≫
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ

Tactic:
apply (Γ₀.splitting K[X]).hom_ext'

Premises used: AlgebraicTopology.DoldKan.Γ₀.splitting, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.SimplicialObject.Splitting.hom_ext'
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
      (Γ₀.obj K[X]).map θ ≫
        Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
            X.map A.e.op)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
        (Splitting.cofan (Γ₀.splitting K[X]) Δ))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
      ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
      (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X.map θ ≫
        Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
            X.map A.e.op)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
        (Splitting.cofan (Γ₀.splitting K[X]) Δ))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
      ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))

Tactic:
change _ ≫ (Γ₀.obj K[X]).map θ ≫ _ = _

Premises used: AlgebraicTopology.DoldKan.Γ₀.obj, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.Functor.map
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h :
  CategoryStruct.comp (Y := HomologicalComplex.X K[X] (image (θ.unop ≫ A.e)).len)
      (Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)))
      (HomologicalComplex.Hom.f PInfty
          (unop ((A.pull θ).fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
        X.map (A.pull θ).e.op) =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
      (Γ₀.obj K[X]).map θ ≫
        Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
            X.map A.e.op)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
        (Splitting.cofan (Γ₀.splitting K[X]) Δ))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
      ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))

Tactic:
simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc,
              Splitting.ι_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.ι_desc, CategoryTheory.SimplicialObject.Splitting.ι_desc_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h :
  HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
⊢ CategoryStruct.comp (Y := HomologicalComplex.X K[X] (image (θ.unop ≫ A.e)).len)
      (Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)))
      (HomologicalComplex.Hom.f PInfty
          (unop ((A.pull θ).fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
        X.map (A.pull θ).e.op) =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ

Tactic:
erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]

Premises used: Quiver.Hom.unop, CategoryTheory.Limits.image.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.SimplicialObject.Splitting.IndexSet.e, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc