mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
a : α
⊢ m₁✝ • a = m₂✝ • a

Tactic:
by injection h (inl a)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hfmodP
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
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    C ((algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff) * map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree

Tactic:
rw [← map_C, ← Polynomial.map_pow, ← Polynomial.map_mul]
    simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)),
      Quotient.algebraMap_eq, ← map_map]
    congr 1
    ext n
    simp only [coeff_map, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
    simp only [coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, sub_ite, sub_zero]
    split_ifs with hn
    · rw [hn, leadingCoeff, sub_self]
      exact zero_mem _
    · by_cases hn' : n < f.natDegree
      · exact hfP _ (coe_lt_degree.mpr hn')
      · rw [f.coeff_eq_zero_of_natDegree_lt]
        · exact P.zero_mem
        · simp [Nat.lt_iff_le_and_ne, ← Nat.not_lt, hn', Ne.symm hn]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun i ↦ ↑(i • t)) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
coe_smul_finset,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun i ↦ i • ↑t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ Δ_[1]^[P.natDegree] (fun x ↦ eval x P) x = (P.leadingCoeff • ↑P.natDegree !) x

Tactic:
P.eval_eq_sum_range,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ Δ_[1]^[P.natDegree] (fun x ↦ ∑ i ∈ range (P.natDegree + 1), P.coeff i * x ^ i) x = (P.leadingCoeff • ↑P.natDegree !) x
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
⊢ ∀ (b : Subgroup G), comap φ M < b → b = ⊤

Tactic:
intro K hK
    specialize hM (K.map φ)
    rw [← comap_lt_comap_of_surjective hφ, ← (comap_injective hφ).eq_iff] at hM
    rw [comap_map_eq_self ((M.ker_le_comap φ).trans hK.le), comap_top] at hM
    exact hM hK

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ x ∈ ⊥ ↔ IsUnit x

Tactic:
bot_def,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ x ∈ ⊥.saturation ↔ IsUnit x
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f'))

Tactic:
coe_invMonoidHom,

Goal state after:
case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (Inv.inv '' v '' IsMulIndecomposable.baseOf v f'))
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ x = (Units.mk0 (f r) hr)⁻¹ * Units.mk0 (f s) hs

Tactic:
eq_inv_mul_iff_mul_eq

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ Units.mk0 (f r) hr * x = Units.mk0 (f s) hs
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k

Tactic:
exact H.trans_lt hkj

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
⊢ x ≠ 0

Tactic:
by rintro (rfl : x = 0); simp at h'

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

Goal state before:
pp: X : SSet
x : X _⦋0⦌
⊢ x ∈ X.degenerate 0 ↔ x ∈ ∅

Tactic:
simp only [Set.mem_empty_iff_false, iff_false]

Goal state after:
X : SSet
x : X _⦋0⦌
⊢ x ∉ X.degenerate 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map (f₂.op ≫ hf₁.section_.op))) y₂ = ↑y₁

Tactic:
Functor.map_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map f₂.op ≫ X.map hf₁.section_.op)) y₂ = ↑y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map hf₁.section_.op)) ((ConcreteCategory.hom (X.map f₂.op)) y₂) = ↑y₁

Tactic:
← hy₂,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map hf₁.section_.op)) x = ↑y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ ofSimplex x ≤ (ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)).preimage f

Tactic:
ofSimplex_le_iff,

Goal state after:
case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ x ∈ ((ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)).preimage f).obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : (ConcreteCategory.hom (X.map ((image.ι (g hf₁ f₂)).op ≫ (factorThruImage (g hf₁ f₂)).op))) y₂ = ↑y₁
⊢ IsIso (factorThruImage (g hf₁ f₂))

Tactic:
Functor.map_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : (ConcreteCategory.hom (X.map (image.ι (g hf₁ f₂)).op ≫ X.map (factorThruImage (g hf₁ f₂)).op)) y₂ = ↑y₁
⊢ IsIso (factorThruImage (g hf₁ f₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : SimplexCategory
⊢ Finite (X.obj (Opposite.op n))

Tactic:
induction n using SimplexCategory.rec with | _ n
   =>  _ 

Goal state after:
case mk
X : SSet
inst✝ : X.Finite
n : ℕ
⊢ Finite (X _⦋n⦌)
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₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) h.simplex = (edgeMk f₁₂).edge
h₂ : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) h.simplex = (edgeMk f₀₁).edge
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex

Tactic:
have h'₀ := h'.d₀

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) h.simplex = (edgeMk f₁₂).edge
h₂ : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) h.simplex = (edgeMk f₀₁).edge
h'₀ : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) h'.simplex = (edgeMk f₁₂).edge
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h'.simplex =
    (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) h.simplex
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 j →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 0 j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

Tactic:
rcases j with - | j <;> dsimp [augment, truncate]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 0 = 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 (j + 1) = 0 ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 j →
    (match 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 1 j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

Tactic:
rcases j with - | j <;> dsimp [augment, truncate]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 0 =
      (match 1, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 (j + 1) =
      (match 1, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j n : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) j →
    (match n + 2 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d (n + 2) j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

Tactic:
rcases j with - | j <;> dsimp [augment, truncate]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) 0 =
      (match n + 2, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) (j + 1) =
      (match n + 2, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 j →
    (match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 j =
      C.d 0 j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
rcases j with - | j <;> dsimp [augment, truncate]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 (j + 1) ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 j →
    (match 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 j =
      C.d 1 j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
rcases j with - | j <;> dsimp [augment, truncate]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j n : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) j →
    (match n + 2 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) j =
      C.d (n + 2) j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
rcases j with - | j <;> dsimp [augment, truncate]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match n + 2, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d (n + 2) 0 ≫ 𝟙 (C.X 0)

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match n + 2, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d (n + 2) (j + 1) ≫ 𝟙 (C.X (j + 1))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Δ[n] _⦋1⦌

Tactic:
by
  refine objMk ⟨![a, b], ?_⟩
  rw [Fin.monotone_iff_le_succ]
  simp only [unop_op, len_mk, Fin.forall_fin_one]
  apply Fin.mk_le_mk.mpr hab

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ ed.s' ≫ X.left.map (SimplexCategory.σ₀Iter n ⋯).op = ed.s' ≫ X.left.map (SimplexCategory.isTerminalZero.from ⦋n⦌).op

Tactic:
congr 3

Goal state after:
case e_a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ SimplexCategory.σ₀Iter n ⋯ = SimplexCategory.isTerminalZero.from ⦋n⦌
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
⊢ (stdSimplex.obj n).Finite

Tactic:
induction n using SimplexCategory.rec with | _ n
   =>  _ 

Goal state after:
case mk
n : ℕ
⊢ Δ[n].Finite
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℕ
hpq : q + 1 = p
⊢ (down ℕ).Rel (p + r) (q + r)

Tactic:
dsimp; lia

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℕ
hpq : q + 1 = p
⊢ (down ℕ).Rel (r + p) (r + q)

Tactic:
dsimp; lia

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℤ
hpq : p + 1 = q
⊢ (up ℤ).Rel (p + r) (q + r)

Tactic:
dsimp; lia

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℤ
hpq : p + 1 = q
⊢ (up ℤ).Rel (r + p) (r + q)

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      (i + 1) =
    (((dNext (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f (i + 1)

Tactic:
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]

Goal state after:
case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      (i + 1) =
    (AlternatingFaceMapComplex.obj (drop.obj X)).d (i + 1) i ≫ Pi.single (i + 1) (-ed.s i) (i + 1) +
        Pi.single (i + 1 + 1) (-ed.s (i + 1)) (i + 1 + 1) ≫
          (AlternatingFaceMapComplex.obj (drop.obj X)).d (i + 1 + 1) (i + 1) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f (i + 1)
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'
⊢ c₁₂.Rel i₁₂ i₁₂'

Tactic:
by simpa only [← h, ← h₂] using ComplexShape.rel_π₁ c₂ c₁₂ h₁ i₂

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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
rw [totalAux.d₂_eq K c₁₂ i₁ h₃ i₁₂']; swap
        · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]
        by_cases h₄ : c₂.Rel (c₂.next i₂) (c₂.next (c₂.next i₂))
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul,
            HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, comp_zero, smul_zero]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + 1, q) = n₁

Tactic:
dsimp; lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + 1 + x, q) = n₁'

Tactic:
dsimp; lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p, q + 1) = n₁

Tactic:
dsimp; lia

Goal state after: