mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ C g.leadingCoeff * q ^ m * (C h.leadingCoeff * q ^ n) %ₘ q + r * (C h.leadingCoeff * q ^ n) %ₘ q +
        C g.leadingCoeff * q ^ m * s %ₘ q +
      r * s %ₘ q =
    r * s %ₘ q

Tactic:
(modByMonic_eq_zero_iff_dvd hq_monic).mpr

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ 0 + r * (C h.leadingCoeff * q ^ n) %ₘ q + C g.leadingCoeff * q ^ m * s %ₘ q + r * s %ₘ q = r * s %ₘ q

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ C g.leadingCoeff * q ^ m * (C h.leadingCoeff * q ^ n)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: 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
x : ℍ[R,c₁,c₂,c₃]
⊢ star (star x) = x

Tactic:
by simp [Star.star]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ + 0 * -1 * a.imJ * b.imK - -1 * -1 * a.imK * b.imK =
    a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK

Tactic:
simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑x✝.num / ↑↑x✝.den = ↑x✝.num / ↑x✝.den

Tactic:
coe_natCast

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑x✝.num / ↑x✝.den = ↑x✝.num / ↑x✝.den
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ * x✝

Tactic:
rw [← coe_nnratCast, coe_mul_eq_smul]

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ • x✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑x✝.num / ↑↑x✝.den = ↑x✝.num / ↑x✝.den

Tactic:
coe_natCast

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑x✝.num / ↑x✝.den = ↑x✝.num / ↑x✝.den
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
⊢ v i = 1 ∨ 1 < f (v i)

Tactic:
refine closure_induction (by grind) (by simp) (fun x y _ _ hx hy ↦ ?_) hi

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hx : x = 1 ∨ 1 < f x
hy : y = 1 ∨ 1 < f y
⊢ x * y = 1 ∨ 1 < f (x * y)
Module: Mathlib.CategoryTheory.Idempotents.Basic

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

Tactic:
intro h X p hp

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasKernel p
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

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Tactic:
· apply Hom.ext

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f.f = g.f
⊢ f = g

Tactic:
by
  simpa [hom_ext_iff] using h

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Y.map x✝ ≫ equalizer.ι (𝟙 (F.obj x✝¹)) (p.app x✝¹) = equalizer.ι (𝟙 (F.obj x✝²)) (p.app x✝²) ≫ F.map x✝

Tactic:
equalizer.lift_ι

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ equalizer.ι (𝟙 (F.obj x✝²)) (p.app x✝²) ≫ F.map x✝ = equalizer.ι (𝟙 (F.obj x✝²)) (p.app x✝²) ≫ F.map x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ j.predAbove k.castSucc

pp: case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i ≤ j.predAbove k.castSucc

Tactic:
· rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i ≤ j.predAbove k.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
by
  dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]

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

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) =
    𝟙 X

Tactic:
ext; apply f.apply_symm_apply

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

Goal state before:
pp: x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x

Tactic:
by
  have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)
  have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)
  have eq₂ :=
    Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)
  ext : 4
  exact DFunLike.congr_fun (eq₁.trans eq₂.symm) _

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

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

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (by lia),
        σ₀Iter_coe_eq_of_lt .., tsub_self]

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

Goal state before:
pp: X : SSet
n m : ℕ
x✝ : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (X.op.map (SimplexCategory.rev.map f).op)) (opObjEquiv.symm y) =
    opObjEquiv.symm ((ConcreteCategory.hom (X.map f.op)) y)

Tactic:
simp [op_map]

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

Goal state before:
pp: X : SSet
n m : ℕ
x✝ : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X.op _⦋m⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.rev.map f).op)) (opObjEquiv y) =
    opObjEquiv ((ConcreteCategory.hom (X.op.map f.op)) y)

Tactic:
simp [op_map]

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

Goal state before:
pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ

Tactic:
Set.mem_iUnion

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ (∃ i, s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: 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

Tactic:
rcases n with - | n
    · exact ⟨⟨alternatingConstHomologyDataZero X _ rfl⟩⟩
    · exact ⟨⟨alternatingConstHomologyDataEvenNEZero X _ h (by simp)⟩⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : { x // x ≠ i }
x : Fin (n + 1 + 1)
hx : x ≠ i
⊢ x ∈ {i}ᶜ

Tactic:
simpa using hx

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : ↥{i}ᶜ
x : Fin (n + 2)
hx : x ∈ {i}ᶜ
⊢ x ≠ i

Tactic:
simpa using hx

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 : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ X.left.δ₀Iter ↑j.castSucc ⋯ ≫ ed.s (↑k + 1) ≫ X.left.σ₀Iter ↑j.castSucc ⋯ ≫ X.left.δ i.succ = X.left.δ i ≫ h ed j

Tactic:
h_eq _ _ k,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ X.left.δ₀Iter ↑j.castSucc ⋯ ≫ ed.s (↑k + 1) ≫ X.left.σ₀Iter ↑j.castSucc ⋯ ≫ X.left.δ i.succ =
    X.left.δ i ≫ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_2
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x = objEquiv.symm (𝟙 ⦋n⦌) → x ∈ Δ[n].nonDegenerate n

Tactic:
· rintro rfl
    apply objEquiv_symm_id_mem_nonDegenerate

Goal state after:
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₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
dsimp [d₂]

Goal state after:
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₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ =
    0
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₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h'

Tactic:
rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Associator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
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✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ (((mapTrifunctorMapNatTrans associator.hom I₁ I₂ I₃).app X₁).app X₂).app X₃ (i₁, i₂, i₃) ≫
      (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).ιMapObj r (i₁, i₂, i₃) j h ≫
        (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
mapTrifunctorMapNatTrans_app_app_app

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
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✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ((associator.hom.app (X₁ (i₁, i₂, i₃).1)).app (X₂ (i₁, i₂, i₃).2.1)).app (X₃ (i₁, i₂, i₃).2.2) ≫
      (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).ιMapObj r (i₁, i₂, i₃) j h ≫
        (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

pp: case neg
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₁)
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₁]
          rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]

Goal state after:
case neg
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₁)
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case neg
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₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
rw [K.D₁_shape c₁₂ _ _ h₂, K.D₂_shape c₁₂ _ _ h₂, comp_zero, comp_zero, neg_zero]

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

Goal state before:
pp: 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₄
i₁ i₁' : ι₁
h₁ : c₁.Rel i₁ i₁'
i₂ : ι₂
i₃ : ι₃
j : ι₄
⊢ d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) •
      (G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃) ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j

Tactic:
obtain rfl := c₁.next_eq' h₁
  rfl

Goal state after: