mathlib-initiative/mathlib-tactics huggingface dataset:
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a + b) = star a + star b

Tactic:
ext <;> simp [add_comm]; ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
rw [QuaternionAlgebra.re_star, zero_mul, add_zero]

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

Goal state before:
pp: 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
hfmodP2 : map (Ideal.Quotient.mk (ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0
g h : R[X]
h_eq : f = g * h
⊢ IsUnit g ∨ IsUnit h

Tactic:
set P : Ideal R := ker (algebraMap R K)
    obtain ⟨m, r, hg, hr, hm0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_right g h)
    obtain ⟨n, s, hh, hs, hn0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_left h g)
    by_cases hm : m = 0
    -- If `m = 0`, `generalizedEisenstein_aux` shows that `g` is a unit.
    · left; exact hm0 hm
    by_cases hn : n = 0
    -- If `n = 0`, `generalizedEisenstein_aux` shows that `h` is a unit.
    · right; exact hn0 hn
    -- Otherwise, we will get a contradiction by showing that `f %ₘ q` is zero mod `P ^ 2`.
    exfalso
    apply hfmodP2
    suffices f %ₘ q = (r * s) %ₘ q by
      -- Since the coefficients of `r` and `s` are in `P`, those of `r * s` are in `P ^ 2`
      suffices h : map (Ideal.Quotient.mk (P ^ 2)) (r * s) = 0 by
        simp [this, h, map_modByMonic, hq_monic]
      ext n
      have h (x : ℕ × ℕ) : (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0 := by
        rw [eq_zero_iff_mem, pow_two]
        apply mul_mem_mul
        · rw [mem_ker, ← coeff_map, hr, coeff_zero]
        · rw [mem_ker, ← coeff_map, hs, coeff_zero]
      simp [-Polynomial.map_mul, coeff_mul, h]
    -- It remains to prove the equality `f %ₘ q = (r * s) %ₘ q`, which is straightforward
    rw [h_eq, hg, hh]
    simp only [add_mul, mul_add, map_add, ← modByMonicHom_apply]
    simp only [← add_assoc, modByMonicHom_apply]
    iterate 3 rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]
    · simp
    · exact ((dvd_pow_self q hm).mul_left _).mul_right _
    · simp only [← mul_assoc]
      exact (dvd_pow_self q hn).mul_left _
    · exact ((dvd_pow_self q hn).mul_left _).mul_left _

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
k : ℕ
y : M
⊢ (shiftₗ M G h ^ k) f y = f (y + k • h)

Tactic:
induction k generalizing f with

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

Goal state before:
pp: M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (m * n) = (x ^ n) ^ m

Tactic:
by
  rw [mul_comm]
  exact ppow_mul x n m

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ closure {a, b} = zmultiples ↑(a.gcd b)

Tactic:
apply le_antisymm
  · grind [closure_le, mem_zmultiples_iff, SetLike.mem_coe, gcd_dvd_left, gcd_dvd_right]
  · simp [zmultiples_le, mem_closure_pair, gcd_eq_gcd_ab, mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (s.PairwiseDisjoint fun x ↦ x • t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (s.PairwiseDisjoint fun i ↦ i • ↑t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ (Fin.castSucc 0) ≫ X.δ 0 = 0

Tactic:
← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ (Fin.succ 0) ≫ X.δ 0 = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: a b : SimplexCategory
f g : a ⟶ b
h : f = g
x : Fin (a.len + 1)
⊢ (Hom.toOrderHom f) x = (Hom.toOrderHom g) x

Tactic:
rw [h]

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

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

Tactic:
rw [h]

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

Goal state before:
pp: case inl.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k < i

Tactic:
exact hjk.trans_lt H

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ ⦋n⦌ = ⦋m⦌

Tactic:
rw [h]

Goal state after:
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
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.predAbove ⟨↑k + (i + 1), ⋯⟩) = ↑⟨↑k + i, ⋯⟩

Tactic:
Fin.predAbove_of_castSucc_lt _ _ (by grind)

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(⟨↑k + (i + 1), ⋯⟩.pred ⋯) = ↑⟨↑k + i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ (X.σ j.succ ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ =
    (X.σ j.castSucc ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ

Tactic:
by
    have h₁ := Y.δ_comp_σ_self (i := j.succ)
    have h₂ := Y.δ_comp_σ_succ (i := j.castSucc)
    dsimp at h₁ h₂
    simp only [SimplicialObject.σ_naturality, Category.assoc, h₁, Category.comp_id, h₂]

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

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
⊢ A.toSSet.degenerate n = ⊤

Tactic:
ext x
    simp [A.mem_degenerate_iff, X.degenerate_eq_univ_of_hasDimensionLT d n hd]

Goal state after:
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₂
⊢ IsIso (factorThruImage (g hf₁ f₂))

Tactic:
by
  have := map_g_op_y₂ hf₁ hy₁ hy₂
  rw [← image.fac (g hf₁ f₂), op_comp, Functor.map_comp, comp_apply] at this
  exact X.isIso_of_nonDegenerate y₁ (factorThruImage (g hf₁ f₂)) _ this

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite ↑(Y.nonDegenerate i)

Tactic:
have : Finite (Y _⦋i⦌) := by
    rw [NatTrans.epi_iff_epi_app] at hf
    simp only [epi_iff_surjective] at hf
    exact Finite.of_surjective _ (hf _)

Goal state after:
X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this✝ : Y.HasDimensionLT d
i : ℕ
hi : i < d
this : Finite (Y _⦋i⦌)
⊢ Finite ↑(Y.nonDegenerate i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
trans ⟨⦋1⦌ₙ, ⟨⟨⟩⟩, mkOfLe (n := Δ.len) (f 0) (f' 0) hff'⟩

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }

n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
⊢ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } =
    𝟙 (truncate.obj (C.augment f w))

Tactic:
by
    ext (_ | i) <;> simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
⊢ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } = 𝟙 C

Tactic:
by
    ext (_ | i) <;> simp

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 : ℕ
⊢ X.left.δ₀Iter ↑(Fin.last n) ⋯ ≫ ed.s 0 ≫ X.left.δ 1 ≫ X.left.σ₀Iter ↑(Fin.last n) ⋯ =
    X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)

Tactic:
ed.s₀_comp_δ₁_assoc,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ X.left.δ₀Iter ↑(Fin.last n) ⋯ ≫ X.hom.app (op ⦋0⦌) ≫ ed.s' ≫ X.left.σ₀Iter ↑(Fin.last n) ⋯ =
    X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
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₁₂'
⊢ K.D₁ c₁₂ i₁₂ i₁₂' = 0

Tactic:
ext ⟨i₁, i₂⟩ h

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₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 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₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' = 0

Tactic:
ext ⟨i₁, i₂⟩ h

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₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0
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₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
ext ⟨i₁, i₂⟩ h

Goal state after:
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₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0
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₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
ext ⟨i₁, i₂⟩ h

Goal state after:
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₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0
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₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
ext ⟨i₁, i₂⟩ h

Goal state after:
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₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
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₁₂'
⊢ 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₁, zero_comp, zero_comp, neg_zero]

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₁₂
A : C
i₁₂ : I₁₂
f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ K.totalDesc f = f i₁ i₂ hi

Tactic:
simp [totalDesc, ιTotal]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
⊢ (CochainComplex.plus C).colimitsOfShape J ≤ CochainComplex.plus C

Tactic:
rintro K ⟨p⟩
    obtain ⟨n, hn⟩ : ∃ (n : ℤ), ∀ (j : J), (p.diag.obj j).IsStrictlyGE n := by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
    refine ⟨n, ?_⟩
    rw [isStrictlyGE_iff]
    intro i hi
    rw [IsZero.iff_id_eq_zero]
    exact (isColimitOfPreserves (HomologicalComplex.eval _ _ i) p.isColimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_src _ _)

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : toHom (mk x) = 0
⊢ ∃ m, m + 1 = n ∧ ∃ β, δ m n β = ↑x

Tactic:
rw [toHom_mk, HomotopyCategory.quotient_map_eq_zero_iff] at h

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : Nonempty (Homotopy (Cocycle.equivHomShift.symm x) 0)
⊢ ∃ m, m + 1 = n ∧ ∃ β, δ m n β = ↑x
Module: Mathlib.Algebra.Homology.BifunctorAssociator

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₂₃
inst✝²³ : HasZeroMorphisms C₁
inst✝²² : HasZeroMorphisms C₂
inst✝²¹ : HasZeroMorphisms C₃
inst✝²⁰ : Preadditive C₁₂
inst✝¹⁹ : Preadditive C₂₃
inst✝¹⁸ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ 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
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₂₃ : ι₂₃
j : ι₄
h₂₃ : c₂.π c₃ c₂₃ (i₂, i₃) = i₂₃
h : c₁.π c₂₃ c₄ (i₁, i₂₃) = j
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j

Tactic:
rw [← h, ← h₂₃, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]; rfl

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_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₂₃
inst✝²³ : HasZeroMorphisms C₁
inst✝²² : HasZeroMorphisms C₂
inst✝²¹ : HasZeroMorphisms C₃
inst✝²⁰ : Preadditive C₁₂
inst✝¹⁹ : Preadditive C₂₃
inst✝¹⁸ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ 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
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₂₃ : ι₂₃
j : ι₄
h₂₃ : c₂.π c₃ c₂₃ (i₂, i₃) = i₂₃
h : c₁.π c₂₃ c₄ (i₁, i₂₃) = j
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j

Tactic:
by rw [← h, ← h₂₃, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]; rfl

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
L : CochainComplex C ℤ
inst✝ : L.IsKInjective
⊢ (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)

Tactic:
by
  rwa [← isKInjective_iff_rightOrthogonal]

Goal state after: