mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
⊢ IsMulTorsionFree M

Tactic:
by
  refine .mk' fun x hx y hy n hn hxy ↦ ?_
  obtain ⟨u, hu⟩ : Associated x y := by
    have := (Associated.of_eq hxy).normalizedFactors_eq
    rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
  replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
  rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy
  rwa [hxy, Units.val_one, mul_one] at hu

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
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ 𝟙 X

Tactic:
← φ.hom_inv_id

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j

Tactic:
simp only [Fin.lt_def, Fin.dite_val, Fin.ite_val, Fin.val_pred]

Goal state after:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else ↑((if j < i then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯)) =
    j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j
k : Fin (⦋m⦌.len + 1)
⊢ (Hom.toOrderHom (factor_δ f j ≫ δ j)) k = (Hom.toOrderHom f) k

Tactic:
cases j using Fin.cases <;> simp_all [factor_δ, δ, σ]

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

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
← epi_iff_surjective

Goal state after:
x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ Epi f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Function.Surjective ⇑(Hom.toOrderHom θ)

Tactic:
← epi_iff_surjective

Goal state after:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Epi θ
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, (ConcreteCategory.hom (F.map f)) x = y) → ∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y) → ∃ f, (ConcreteCategory.hom (F.map f)) x = y

Tactic:
· rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y) → ∃ f, (ConcreteCategory.hom (F.map f)) x = y
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U → ∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y) → y ∈ (ofSection x).obj U

Tactic:
· rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y) → y ∈ (ofSection x).obj U
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
ι : Type u_1
A : ι → X.Subcomplex
d : ℕ
⊢ (⨆ i, A i).toSSet.HasDimensionLT d ↔ ∀ (i : ι), (A i).toSSet.HasDimensionLT d

Tactic:
by
  simp only [hasDimensionLT_iff, Subcomplex.degenerate_eq_top_iff]
  aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₁.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ ((equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x ≫ WidePullback.base fun x ↦ F.hom) =
    A.left.app x ≫ WidePullback.base fun x ↦ F.hom

Tactic:
simpa using congr_app A.w.symm x

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x ↦ f✝.right) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x ↦ g.right) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (n.len + 1)
⊢ f.hom ≫ Hom.right F ≫ WidePushout.ι (fun x ↦ g.hom) i = Hom.left F ≫ WidePushout.head fun x ↦ g.hom

Tactic:
by rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f) j✝)) =
    (Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j✝)) ≫ X.right.map f

Tactic:
rw [Category.assoc, ← X.right.map_comp]

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f) j✝)) =
    Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j✝ ≫ f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
← epi_iff_surjective

Goal state after:
case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Epi (f.app X✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ ⊤.image f ≤ range f

Tactic:
image_top

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ range f ≤ range f
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ x₀ = y₀

Tactic:
rw [← hom.src_eq, hhom, hom'.src_eq]

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id x₀).edge = (id y₀).edge

Tactic:
rw [← hom.src_eq, hhom, hom'.src_eq]

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x✝ : ↥{a, b}
x : α
hx : x ∈ {a, b}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x✝ : ↥{a, b}
x : α
hx✝ : x ∈ {a, b}
hx : x = a ∨ x = b
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩] a_1 = ⟨x, hx✝⟩
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
b x : α
hab : x < b
x✝ : ↥{x, b}
hx : x ∈ {x, b}
⊢ ∃ a, ![⟨x, ⋯⟩, ⟨b, ⋯⟩] a = ⟨x, hx⟩

Tactic:
exact ⟨0, rfl⟩

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x✝ : ↥{a, b, c}
x : α
hx : x ∈ {a, b, c}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x✝ : ↥{a, b, c}
x : α
hx✝ : x ∈ {a, b, c}
hx : x = a ∨ x = b ∨ x = c
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx✝⟩
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
b c : α
hbc : b < c
x : α
hab : x < b
x✝ : ↥{x, b, c}
hx : x ∈ {x, b, c}
⊢ ∃ a, ![⟨x, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a = ⟨x, hx⟩

Tactic:
exact ⟨0, rfl⟩

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 + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter (↑i + 1) ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑i + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i ⋯ ≫ ed.s (↑k + 1) ≫ X.left.σ₀Iter ↑i ⋯ ≫ X.left.δ i.castSucc.succ

Tactic:
rw [X.left.δ₀Iter_succ'_assoc _ (by grind),
      X.left.σ₀Iter_δ' i.castSucc.succ i.val (m := k.val + 1)
        (i' := 1) (by grind) (by grind) (by simp; grind),
      dsimp% ed.s_comp_δ_assoc k.val 0, X.left.σ₀Iter_δ _ _ (by grind)]

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 j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯ ≫ X.left.σ i.castSucc =
    X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑j + 1) ⋯

Tactic:
X.left.σ₀Iter_σ _ _ (by grind)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑j + 1) ⋯ = X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑j + 1) ⋯
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
x✝¹ : c₁.Rel i₁ i₁'
x✝ : c₁.Rel i₁' i₁''
i₂ : I₂
⊢ ({ f := fun i₂ ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } ≫ { f := fun i₂ ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ }).f i₂ = Hom.f 0 i₂

Tactic:
apply d₁_comp_d₁

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₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₁ c₁₂ i₁₂ i₁₂' = 0

Tactic:
ext ⟨i₁, i₂⟩ h
  simp only [totalAux.ιMapObj_D₁, comp_zero]
  by_cases h₁ : c₁.Rel i₁ (c₁.next i₁)
  · rw [K.d₁_eq_zero' c₁₂ h₁ i₂ i₁₂']
    intro h₂
    exact h₁₂ (by simpa only [← h, ← h₂] using ComplexShape.rel_π₁ c₂ c₁₂ h₁ i₂)
  · exact d₁_eq_zero _ _ _ _ _ h₁

Goal state after:
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
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next 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 = 0

Tactic:
HomologicalComplex₂.d₂_eq _ _ _ h₄ _ (by rw [← ComplexShape.next_π₂ c₁ c i₁ h₄, h]),

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
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next j)
⊢ (c₁.ε₂ c₂ c (i₁, i₂) •
        ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).d i₂ (c₂.next i₂) ≫
          (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ (c₂.next i₂) (c.next j) ⋯) ≫
      hom₁ h₁ f₂ F c (c.next j) j =
    0
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 : Cofork.π sq.cokernelCofork ≫ m = s.π
⊢ (PushoutCocone.mk inl inr ⋯).inr ≫ m =
    (PushoutCocone.mk inl inr ⋯).inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
· replace hm := biprod.inr ≫= hm
          dsimp at hm ⊢
          simp only [biprod.inr_desc_assoc] at hm
          rw [hm]
          symm
          apply PushoutCocone.IsColimit.inr_desc h

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

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

Tactic:
· rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁, comp_zero,
      d₁_eq_zero, d₂_eq_zero, zero_add]
    · intro h₂
      apply h₁
      have := ComplexShape.rel_π₂ c₁ c₁₂ i₁ h₂
      rw [c₁₂.next_eq' this]
      exact this
    · intro h₂
      apply h₁
      have := ComplexShape.rel_π₁ c₂ c₁₂ h₂ i₂
      rw [c₁₂.next_eq' this]
      exact this

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Q.map (K.shortComplexTruncLE 0).g ≫
      Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13) =
    e₂.hom ≫ e₂.inv ≫ Q.map (K.πTruncGE 1)

Tactic:
rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE ..,
        Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : (sq.lift ≫ Q.p) ≫ prod.snd = prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p) ≫ prod.snd
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : sq.lift ≫ Q.p₁ = P.p₁ ≫ p
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
A : Type u_3
inst✝² : Category.{v_3, u_3} A
inst✝¹ : Abelian A
inst✝ : HasZeroObject C
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj 0)

Tactic:
simp only [plus_quotient_obj_iff]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
A : Type u_3
inst✝² : Category.{v_3, u_3} A
inst✝¹ : Abelian A
inst✝ : HasZeroObject C
⊢ CochainComplex.plus C 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone f))

Tactic:
simp only [plus_quotient_obj_iff]

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ CochainComplex.plus C (CochainComplex.mappingCone f)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : Plus C
⊢ ∃ a, (quotient C).obj a = K

Tactic:
obtain ⟨L, hL⟩ := HomotopyCategory.quotient_obj_surjective K.obj
    refine ⟨⟨L, ?_⟩, by ext; exact hL⟩
    rw [← HomotopyCategory.plus_quotient_obj_iff, hL]
    exact K.property

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
a b : ℤ
h : a + 1 = b
⊢ t.truncGTπ a ≫ (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b

Tactic:
subst h
  dsimp [truncGTIsoTruncGE, truncGTπ]
  rw [Category.comp_id]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ IsIso ((t.truncLT n).map f)

Tactic:
· obtain ⟨e, he⟩ := t.triangle_iso_exists
      mem (t.triangleLTGE_distinguished n Y) (Iso.refl _) (n - 1) n
      (by dsimp; infer_instance) (by dsimp; infer_instance)
      (by dsimp; infer_instance) (by dsimp; infer_instance)
    suffices ((t.truncLT n).map f) = e.hom.hom₁ by rw [this]; infer_instance
    exact t.to_truncLT_obj_ext (Eq.trans (by cat_disch) e.hom.comm₁)

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))

Tactic:
rw [← t.truncLT_map_truncGE_map_truncLTι_app_fac a b X]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X)