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

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ (C g.leadingCoeff).coeff (C g.leadingCoeff + r).natDegree + r.coeff (C g.leadingCoeff + r).natDegree ∈ P

Tactic:
← hg,

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ (C g.leadingCoeff).coeff g.natDegree + r.coeff g.natDegree ∈ P
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i

Tactic:
by
  intro i hi
  obtain ⟨k, hk⟩ := exists_add_of_le hi
  rw [hk, pow_add]
  obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf
  refine ⟨y * x ^ k, ?_, ?_⟩
  · exact Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)
  · rw [← mul_assoc _ y, H]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (Δ_[1]^[n] fun r ↦ ∑ k ∈ range n, P k * r ^ k) = 0

Tactic:
by
  simp_rw [← sum_apply _ _ (fun i x ↦ P i * x ^ i), fwdDiff_iter_finsetSum, sum_fn, ← smul_eq_mul,
    ← Pi.smul_def, fwdDiff_iter_const_smul, ← sum_fn]
  exact sum_eq_zero fun i hi ↦ smul_eq_zero_of_right _ <| fwdDiff_iter_pow_eq_zero_of_lt
    <| mem_range.mp hi

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
⊢ v i / v j ∉ range v

Tactic:
by_contra! ⟨k, hk⟩

Goal state after:
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
⊢ False
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by
  constructor
  · intro
    dsimp only [Function.Surjective]
    by_contra! ⟨m, hm⟩
    let Y := of (ULift (Fin 2))
    let p₁ : B ⟶ Y := ofHom
      ⟨fun b => if b < m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h => by
        simp only
        split_ifs with h₁ h₂ h₂
        any_goals apply Fin.zero_le
        · exfalso
          exact h₁ (lt_of_le_of_lt h h₂)
        · rfl⟩
    let p₂ : B ⟶ Y := ofHom
      ⟨fun b => if b ≤ m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h => by
        simp only
        split_ifs with h₁ h₂ h₂
        any_goals apply Fin.zero_le
        · exfalso
          exact h₁ (h.trans h₂)
        · rfl⟩
    have h : p₁ m = p₂ m := by
      congr
      rw [← cancel_epi f]
      ext a : 3
      simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]
      change ite _ _ _ = ite _ _ _
      split_ifs with h₁ h₂ h₂
      any_goals rfl
      · exfalso
        exact h₂ (le_of_lt h₁)
      · exfalso
        exact hm a (eq_of_le_of_not_lt h₂ h₁)
    simp [Y, p₁, p₂, ConcreteCategory.hom_ofHom] at h
  · intro h
    exact ConcreteCategory.epi_of_surjective f h

Goal state after:
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 ≤ j.predAbove k.castSucc

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]

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 < k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi' : Δ ≠ Δ'
⊢ Δ'.len < Δ.len

Tactic:
by
  grind [→ len_le_of_mono, SimplexCategory.ext]

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
x : A.toSSet _⦋n⦌
⊢ x ∈ A.toSSet.degenerate n ↔ x ∈ ⊤

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

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

Goal state before:
pp: case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]
    apply congr_fun; congr
    decide

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

Goal state before:
pp: case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]
    apply congr_fun; congr
    decide

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

Goal state before:
pp: case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]
    apply congr_fun; congr
    decide

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

Goal state before:
pp: case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]
    apply congr_fun; congr
    decide

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

Goal state before:
pp: case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]
    apply congr_fun; congr
    decide

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

Goal state before:
pp: case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
rw [← Functor.map_comp_apply, ← op_comp]
    apply congr_fun; congr
    decide

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

Goal state before:
pp: case refine_1
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
this : Mono f
⊢ objEquiv.symm f = objEquiv.symm (𝟙 ⦋n⦌)

Tactic:
simpa only [EmbeddingLike.apply_eq_iff_eq] using SimplexCategory.eq_id_of_mono f

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

Tactic:
K.d₁_eq_zero _ _ _ _ h₄,

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 (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ 0 = 0
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
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
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j' =
    0

Tactic:
ιMapBifunctorOrZero_eq_zero,

Goal state after:
case pos
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
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫ (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ 0 =
    0

case pos.h
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
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.π c₂ c (c₁.prev i₁, i₂) ≠ j'
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (NatIso.ofComponents (fun X ↦ t.z (a + b) c • (shiftFunctorAdd C (a + b) c).app X) ⋯).hom.app X ≫
      (shiftFunctor C c).map ((NatIso.ofComponents (fun X ↦ t.z a b • (shiftFunctorAdd C a b).app X) ⋯).hom.app X) =
    eqToHom ⋯ ≫
      (NatIso.ofComponents (fun X ↦ t.z a (b + c) • (shiftFunctorAdd C a (b + c)).app X) ⋯).hom.app X ≫
        (NatIso.ofComponents (fun X ↦ t.z b c • (shiftFunctorAdd C b c).app X) ⋯).hom.app ((shiftFunctor C a).obj X)

Tactic:
dsimp
    simp only [Functor.map_comp, Category.assoc, CatCenter.smul_iso_hom_eq]
    rw [CatCenter.naturality, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      CatCenter.naturality_assoc, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      t.shift_z_app, CatCenter.naturality, CatCenter.naturality_assoc,
      ← CatCenter.mul_app_assoc, ← CatCenter.mul_app_assoc,
      ← Units.val_mul, ← Units.val_mul, t.assoc a b c]
    simp [shiftFunctorAdd_assoc_hom_app (C := C) a b c X, shiftFunctorAdd']

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

Goal state before:
pp: case pos
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 : (up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
apply total.hom_ext
    intro p q hpq
    dsimp at h hpq
    dsimp [totalShift₁XIso]
    rw [ι_D₂_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, ι_D₂,
      ((shiftFunctor₁ C x).obj K).d₂_eq _ _ rfl _ (by dsimp; lia),
      K.d₂_eq _ _ rfl _ (by dsimp; lia), smul_smul,
      Linear.units_smul_comp, Category.assoc, ι_totalDesc]
    dsimp
    congr 1
    rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]

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

Goal state before:
pp: case pos.e_a
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'
⊢ c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) •
      (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)).app (K₃.X i₃) ≫
        (G.map (mapBifunctor.D₂ K₁ K₂ F₁₂ c₁₂ (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))).app (K₃.X i₃) ≫
          (K₁.mapBifunctor K₂ F₁₂ c₁₂).ιMapBifunctor K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂ =
    d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
· rw [← NatTrans.comp_app_assoc, ← Functor.map_comp,
          mapBifunctor.ι_D₂]
        by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
        · have h₄ := (ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃).symm
          rw [mapBifunctor.d₂_eq _ _ _ _ _ h₃ _ h₄,
            d₂_eq _ _ _ _ _ _ _ _ h₃,
            ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ (by rw [← h₂, ← h₄]; rfl),
            ι_eq _ _ _ _ _ _ _ _ _ _ (c₁₂.next i₁₂) _ h₄ h₂,
            Functor.map_units_smul, Functor.map_comp, NatTrans.app_units_zsmul,
            NatTrans.comp_app, Linear.units_smul_comp, assoc, smul_smul]
        · rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₃,
            mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₃,
            Functor.map_zero, zero_app, zero_comp, smul_zero]

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : biprod.inr ≫ biprod.desc inl inr ≫ m = biprod.inr ≫ s.π
⊢ inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
simp only [biprod.inr_desc_assoc] at hm

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
⊢ inr ≫ m = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯
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.X₁.d j k))) x₁ = 0

Tactic:
apply (Preadditive.mono_iff_injective (S.f.f k)).1 inferInstance

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 ((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
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0

Tactic:
hL ((HomotopyCategory.quotient _ _).map f) hK,

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
⊢ 0 = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullback f g
inst✝² : (trivialFibrations C).IsStableUnderBaseChange
inst✝¹ : Fibration f
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (pullback.snd f g)

Tactic:
by
  rw [weakEquivalence_iff]
  exact (MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g)
    (mem_trivialFibrations f)).2

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
⊢ cofibrations C P'.i

Tactic:
by rw [← cofibration_iff]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝ : A.IsVerdierLeftLocalizing B
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hX : B.op X✝
hY : A.op Y✝
⊢ ∃ Z a b, A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
by
    obtain ⟨Z, a, b, h₁, h₂, fac⟩ :=
      IsVerdierLeftLocalizing.fac f.unop hY hX
    exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
inst✝ : t.IsGE X n₁
⊢ IsZero ((t.truncLE n₀).obj X)

Tactic:
← t.isGE_iff_isZero_truncLE_obj _ _ h X

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
inst✝ : t.IsGE X n₁
⊢ t.IsGE X n₁