mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (mk (List.replicate n (a, true))).toWord = List.replicate n (a, true)

Tactic:
toWord

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
x : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
hn : n < f.natDegree + f'.natDegree
⊢ False

Tactic:
linarith

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : IsGCDMonoid R
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
⊢ ∃ y, (algebraMap R (FractionRing R)) y = X

Tactic:
cases h

Goal state after:
case intro
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
⊢ ∃ y, (algebraMap R (FractionRing R)) y = X
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).re =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).re

Tactic:
simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imI =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imI

Tactic:
simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imJ =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imJ

Tactic:
simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imK =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imK

Tactic:
simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
fst✝ : ι
snd✝ : α fst✝
⊢ ⟨fst✝, 1 • snd✝⟩ = ⟨fst✝, snd✝⟩

Tactic:
one_smul

Goal state after:
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
fst✝ : ι
snd✝ : α fst✝
⊢ ⟨fst✝, snd✝⟩ = ⟨fst✝, snd✝⟩
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : n < f.natDegree
⊢ f.coeff n ∈ P

Tactic:
exact hfP _ (coe_lt_degree.mpr hn')

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ (Δ_[1]^[n + 1] fun r ↦ r ^ j) = 0

Tactic:
iterate_succ_apply,

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ Δ_[1]^[n] (Δ_[1] fun r ↦ r ^ j) = 0
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ (Δ_[1]^[n + 1] fun r ↦ r ^ (n + 1)) = ↑(n + 1)!

Tactic:
iterate_succ_apply,

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
⊢ Δ_[1]^[n] (Δ_[1] fun r ↦ r ^ (n + 1)) = ↑(n + 1)!
Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : Preorder α
inst✝³ : DecidableEq α
inst✝² : MulLeftMono α
inst✝¹ : MulRightMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Icc a b * Icc c d) ⊆ ↑(Icc (a * c) (b * d))

Tactic:
by simpa using Set.Icc_mul_Icc_subset' _ _ _ _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
b : Bˣ
hb : ↑b ∈ range ⇑f
⊢ b ∈ f.valueMonoid

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
x : ↑X.1
⊢ x ∈ ⊤ ∧ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
e : X ⟶ I := ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom f) x, ⋯⟩, monotone' := ⋯ }
⊢ Monotone fun y ↦ ↑y

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ Monotone fun x ↦ i

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (f + 0).f = f.f

Tactic:
apply add_zero

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ f.left.app (op ⦋0⦌) ≫
      ((((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj Y)).symm
            ⟨Y.hom.app (op ⦋0⦌), ⋯⟩).f
        0 =
    ((((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj X)).symm
            ⟨X.hom.app (op ⦋0⦌), ⋯⟩).f
        0 ≫
      ((ChainComplex.single₀ C).map f.right).f 0

Tactic:
rw [ChainComplex.toSingle₀Equiv_symm_apply_f_zero,
      ChainComplex.toSingle₀Equiv_symm_apply_f_zero,
      ChainComplex.single₀_map_f_zero]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ f.left.app (op ⦋0⦌) ≫ Y.hom.app (op ⦋0⦌) = X.hom.app (op ⦋0⦌) ≫ f.right
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject.Augmented C)ᵒᵖ).map f ≫ (unop Y✝).rightOpLeftOpIso.op.hom =
    (unop X✝).rightOpLeftOpIso.op.hom ≫
      (simplicialToCosimplicialAugmented C ⋙ cosimplicialToSimplicialAugmented C).map f

Tactic:
dsimp
      rw [← f.op_unop]
      simp_rw [← op_comp]
      congr 1
      cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter (i + 1) h)) k) =
    ↑((ConcreteCategory.hom (σ 0)) ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))

Tactic:
rw [σ₀Iter_coe_eq_of_ge .., coe_σ,
      Fin.predAbove_of_castSucc_lt _ _ ?_, Fin.val_pred,
      σ₀Iter_coe_eq_of_ge .., Nat.sub_add_eq]

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ Fin.castSucc 0 < (ConcreteCategory.hom (σ₀Iter i ⋯)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ (Hom.toOrderHom θ) x =
    (i.succAboveOrderEmb.toOrderHom.comp (((Fin.last n).predAbove i).predAboveOrderHom.comp (Hom.toOrderHom θ))) x

Tactic:
exact .symm <| this _ (hi _)

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : C
f : yoneda.obj X ⟶ F
⊢ range f = ofSection (yonedaEquiv f)

Tactic:
by
  rw [ofSection_eq_range, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
n k : ℕ
hk : n ≤ k
x : X _⦋k⦌
hx : x ∈ ⊥.obj (op ⦋k⦌)
⊢ ⟨x, hx⟩ ∈ ⊥.toSSet.degenerate k ↔ ⟨x, hx⟩ ∈ ⊤

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
⊢ (∃ f, (ConcreteCategory.hom (X.map f)) t.simplex = s.simplex) ↔
    ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
⊢ ∃ f_1,
    (ConcreteCategory.hom (X.map f_1.op)) { dim := n, simplex := x }.simplex =
      { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x }.simplex

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝¹ x✝ : ⊥.toSSet ⟶ Y
n✝ : SimplexCategoryᵒᵖ
val✝ : X.obj n✝
h : val✝ ∈ ⊥.obj n✝
⊢ (ConcreteCategory.hom (x✝¹.app n✝)).toFun ⟨val✝, h⟩ = (ConcreteCategory.hom (x✝.app n✝)).toFun ⟨val✝, h⟩

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝¹ : SimplexCategoryᵒᵖ
x✝ : ⊥.toSSet.obj x✝¹
val✝ : X.obj x✝¹
h : val✝ ∈ ⊥.obj x✝¹
⊢ Y.obj x✝¹

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
val✝ : X.obj x✝²
h : val✝ ∈ ⊥.obj x✝²
⊢ (ConcreteCategory.hom
          (⊥.toSSet.map x✝ ≫
            ↾fun x ↦
              match x with
              | ⟨val, h⟩ => ⋯.elim)).toFun
      ⟨val✝, h⟩ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              match x with
              | ⟨val, h⟩ => ⋯.elim) ≫
            Y.map x✝)).toFun
      ⟨val✝, h⟩

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.N
⊢ (∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) →
    ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
⊢ ⊤ ≤ ⨆ s, s.subcomplex

Tactic:
rw [← Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top X, iSup_le_iff]

Goal state after:
X : SSet
⊢ ∀ (i : (p : ℕ) × ↑(X.nonDegenerate p)), Subcomplex.ofSimplex ↑i.snd ≤ ⨆ s, s.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) ((ConcreteCategory.hom (X.map f.op)) y.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex ↔
    (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
exact (e.app _).toEquiv.apply_eq_iff_eq

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ (N.mk ↑y ⋯).subcomplex ≤ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]
      have := isSplitEpi_of_epi f
      have : Function.Injective (X.map f.op) := by
        rw [← mono_iff_injective]
        infer_instance
      refine ⟨(section_ f).op, this ?_⟩
      dsimp
      rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) ↔ f₀₁ ≫ f₁₂ = f₀₂

Tactic:
let h' : Edge.CompStruct (edgeMk f₀₁) (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
      Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂)
        (by cat_disch) (by cat_disch) (by cat_disch)
  refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨by rwa [← h]⟩⟩
  rw [← Arrow.mk_inj]
  apply ComposableArrows.arrowEquiv.symm.injective
  convert_to! (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex
  · exact (h'.d₁).symm
  · exact (h.d₁).symm
  · have h₀ := h.d₀
    have h₂ := h.d₂
    have h'₀ := h'.d₀
    have h'₂ := h'.d₂
    simp only [δ₂_zero, δ₂_two, edgeMk_edge] at h₀ h₂ h'₀ h'₂
    exact congr_arg _ (ComposableArrows.ext₂_of_arrow
      (ComposableArrows.arrowEquiv.symm.injective
        (by simp [-Edge.CompStruct.d₂, h'₂, ← h₂]))
      (ComposableArrows.arrowEquiv.symm.injective
        (by simp [-Edge.CompStruct.d₀, h'₀, ← h₀])))

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ (facePairComplIso i j h).hom ≫ (face {i, j}ᶜ).ι = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i

Tactic:
facePairComplIso_hom_ι

Goal state after:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ stdSimplex.δ (i.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
i : Fin (d + 1)
f : ↑(Δ[n].nonDegenerate d)
⊢ ∃ a, (Hom.toOrderHom (objEquiv ↑f)) a = ↑f i

Tactic:
exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk hij : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel 0 0
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ ((match n✝ + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) 0
hij : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) 0
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ ((match n✝ + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
hij : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ ((match 0, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ ((match n✝ + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel 0 (0 + 1)
hij : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel 0 (0 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ ((match n✝ + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (0 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (0 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ ((match n✝ + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (0 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ ((match 0, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (0 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ ((match n✝ + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)
hij : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ ((match n✝ + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ.succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (k + 1 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

Goal state after: