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

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
x : (i : ι) × α i
⊢ (a * b) • x = a • b • x

Tactic:
cases x
    rw [smul_mk, smul_mk, smul_mk, mul_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ (a * star a + a * star b + (b * star a + b * star b)).re =
    (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)

Tactic:
re_add

Goal state after:
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
⊢ f.coeff n - f.leadingCoeff ∈ P

Tactic:
hn,

Goal state after:
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
⊢ f.coeff f.natDegree - f.leadingCoeff ∈ P
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case one
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ ∃ a, 1 = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
use 0

Goal state after:
case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case one
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ ∃ a, 1 = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
use 0

Goal state after:
case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₂ * (x₁ * y) ∈ s

Tactic:
by rwa [mul_left_comm, ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : 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
⊢ ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f

Tactic:
rw [image_comp, IsMulIndecomposable.image_baseOf_inv_comp_eq v hv_inv f, image_comp,
        ← image_comp]

Goal state after:
ι : 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
⊢ ⇑invMonoidHom ∘ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ ∃ a, (restrict₀ f) a = 0

Tactic:
use 0

Goal state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ (restrict₀ f) 0 = 0
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
y c d : Bˣ
hc : c ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
hd : d ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
u : A
hu : f u ≠ 0
a : A
ha : f u * ↑c = f a
v : A
hv : f v ≠ 0
b : A
hb : f v * ↑d = f b
⊢ f (u * v) ≠ 0

Tactic:
simp [hu, hv]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
· intro h X p hp
    have : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    apply Preadditive.hasEqualizer_of_hasKernel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C ↔ IsIdempotentComplete D

Tactic:
constructor
  · exact Equivalence.isIdempotentComplete ε
  · exact Equivalence.isIdempotentComplete ε.symm

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 : SimplicialObject.Augmented C
⊢ X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 0 + -X.left.δ 1 ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
SimplicialObject.δ_naturality

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 0 +
      -X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 1 =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (CosimplicialObject C)

Tactic:
dsimp [CosimplicialObject]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory ⥤ C)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (CosimplicialObject C)

Tactic:
dsimp [CosimplicialObject]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory ⥤ C)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ δ₀Iter (i + 1) hi ≫ σ j = δ₀Iter i ⋯

Tactic:
by
  refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter (i + 1)) (σ j),
    δ₀Iter_apply .., δ₀Iter_apply .., coe_σ,
    Fin.predAbove_of_castSucc_lt _ _ (by grind)]
  dsimp

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

Goal state before:
pp: case mpr.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
a : A.toSSet _⦋m⦌
ha : a ∈ A.toSSet.nonDegenerate m
hx : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ A.obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ B.obj (op ⦋n⦌)

Tactic:
mem_nonDegenerate_iff

Goal state after:
case mpr.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
a : A.toSSet _⦋m⦌
ha : ↑a ∈ X.nonDegenerate m
hx : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ A.obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ B.obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
⊢ A = ⊤ ↔ ∀ (n : ℕ), X.nonDegenerate n ⊆ A.obj (op ⦋n⦌)

Tactic:
simpa using! le_iff_contains_nonDegenerate ⊤ A

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

Tactic:
rcases n.even_or_odd with h | h

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
rcases n.even_or_odd with h | h

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
i : Fin (n + 1)
h : obj₀Equiv.symm i ∈ (face S).obj (op ⦋0⦌)
⊢ i ∈ S

Tactic:
by simpa using! h

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ range (yonedaEquiv.symm x) ≤ ofSimplex x

Tactic:
simp [range_eq_ofSimplex]

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ (ConcreteCategory.hom
          ((↾fun f ↦
              objEquiv.symm
                (SimplexCategory.Hom.mk
                  { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
            SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)).toFun
      x =
    (ConcreteCategory.hom
          (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0))).toFun
      x

Tactic:
apply objEquiv.injective

Goal state after:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ objEquiv
      ((ConcreteCategory.hom
            ((↾fun f ↦
                objEquiv.symm
                  (SimplexCategory.Hom.mk
                    { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
              SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)).toFun
        x) =
    objEquiv
      ((ConcreteCategory.hom
            (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0))).toFun
        x)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ (ConcreteCategory.hom ((↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ 0)).toFun φ =
    (ConcreteCategory.hom (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ

Tactic:
apply objEquiv.injective

Goal state after:
Δ : SimplexCategory
n : ℕ
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ objEquiv
      ((ConcreteCategory.hom ((↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ 0)).toFun φ) =
    objEquiv ((ConcreteCategory.hom (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ (ConcreteCategory.hom ((↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ i.succ)).toFun φ =
    (ConcreteCategory.hom ((stdSimplex.obj Δ).left.δ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f)))).toFun φ

Tactic:
apply objEquiv.injective

Goal state after:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ objEquiv
      ((ConcreteCategory.hom ((↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ i.succ)).toFun
        φ) =
    objEquiv
      ((ConcreteCategory.hom ((stdSimplex.obj Δ).left.δ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f)))).toFun φ)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ (ConcreteCategory.hom ((↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.σ i.succ)).toFun φ =
    (ConcreteCategory.hom ((stdSimplex.obj Δ).left.σ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f)))).toFun φ

Tactic:
apply objEquiv.injective

Goal state after:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ objEquiv
      ((ConcreteCategory.hom ((↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.σ i.succ)).toFun
        φ) =
    objEquiv
      ((ConcreteCategory.hom ((stdSimplex.obj Δ).left.σ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f)))).toFun φ)
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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x✝ : ↑(c₂.π c₁ c₁₂ ⁻¹' {j})
i₂ : I₂
i₁ : I₁
h : (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}
⊢ (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}

Tactic:
by simpa [π_symm] using h

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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x✝ : ↑(c₁.π c₂ c₁₂ ⁻¹' {j})
i₁ : I₁
i₂ : I₂
h : (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}
⊢ (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}

Tactic:
by simpa [π_symm] using h

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
have hj' : ComplexShape.π c₁ c₂ c ⟨i₁, i₂'⟩ = j := by
    rw [← hj, ← ComplexShape.next_π₂ c₁ c i₁ hi₂, ComplexShape.next_π₁ c₂ c hi₁ i₂]
  rw [HomologicalComplex₂.d₂_eq _ _ _ hi₂ _ hj', HomologicalComplex₂.d₂_eq _ _ _ hi₂ _
        (by rw [← c.next_eq' (ComplexShape.rel_π₂ c₁ c i₁' hi₂), hj]),
    Linear.comp_units_smul, Linear.comp_units_smul, Linear.units_smul_comp, assoc,
    ιMapBifunctor_hom₁ _ _ _ _ _ _ _ _ _ _ (c₁.prev_eq' hi₁),
    ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ hj',
    Linear.comp_units_smul, smul_smul, smul_smul,
    Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
    Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
    NatTrans.naturality_assoc, ComplexShape.ε₁_ε₂ c hi₁ hi₂, neg_mul, Units.neg_smul, neg_inj,
    smul_left_cancel_iff, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, f₂.comm]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
this : Mono S.f
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f k))) ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.d j k))) x₁) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f k))) 0

Tactic:
rw [← ConcreteCategory.forget₂_comp_apply, ← HomologicalComplex.Hom.comm,
    ConcreteCategory.forget₂_comp_apply, hx₁, ← ConcreteCategory.forget₂_comp_apply,
    HomologicalComplex.d_comp_d, Functor.map_zero, map_zero]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
this : Mono S.f
⊢ (ConcreteCategory.hom 0) x₂ = 0
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃) = j'
⊢ False

Tactic:
apply h₂

Goal state after:
case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := ⋯
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = j'
⊢ False

Tactic:
apply h₂

Goal state after:
case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := ⋯
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'