mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
⊢ neg' W f = φ.neg.map L ⋯

Tactic:
obtain ⟨φ₀, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction X Y)
    (_ : f = φ₀.map L (inverts L W)),
      neg' W f = φ₀.neg.map L (inverts L W) :=
    ⟨_, (exists_leftFraction L W f).choose_spec, rfl⟩

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction X Y
hφ : φ₀.map L ⋯ = φ.map L ⋯
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z✝
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s
Z : C
p : u.Y' ⟶ Z
hp : W p
fac₄ : z₁.f ≫ w₁.f ≫ u.f ≫ p = z₂.f ≫ w₂.f ≫ u.s ≫ p
⊢ a.comp b₁ = a.comp b₂

Tactic:
rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z✝
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s
Z : C
p : u.Y' ⟶ Z
hp : W p
fac₄ : z₁.f ≫ w₁.f ≫ u.f ≫ p = z₂.f ≫ w₂.f ≫ u.s ≫ p
⊢ mk (a.comp₀ b₁ z₁) = mk (a.comp₀ b₂ z₂)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
⊢ a₁.comp b = a₂.comp b

Tactic:
rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
⊢ mk (a₁.comp₀ b z₁) = mk (a₂.comp₀ b z₂)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
κ' : Cardinal.{v}
hκ' : κ ≤ κ'
⊢ Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ'

Tactic:
simpa only [Cardinal.lift_le] using hκ'

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ = a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁
ha₂₃ : (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ = a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂
⊢ (P.extensionProduct Q).retractClosure X

Tactic:
obtain ⟨b₂ : X' ⟶ X, hb₁₂, hb₂₃⟩ :=
    complete_distinguished_triangle_morphism₂ _ _ hT' hT b₁ b₃ (by dsimp; grind)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ = a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁
ha₂₃ : (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ = a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂
b₂ : X' ⟶ X
hb₁₂ : (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁ ≫ b₂ = b₁ ≫ (Triangle.mk f₁ f₂ f₃).mor₁
hb₂₃ : (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂ ≫ b₃ = b₂ ≫ (Triangle.mk f₁ f₂ f₃).mor₂
⊢ (P.extensionProduct Q).retractClosure X
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : IsIso (homologyMap φ i)
hφφ' : IsIso (homologyMap (φ ≫ φ') i)
⊢ IsIso (homologyMap φ' i)

Tactic:
homologyMap_comp

Goal state after:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : IsIso (homologyMap φ i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ' i)
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap (φ ≫ φ') i)
⊢ IsIso (homologyMap φ i)

Tactic:
homologyMap_comp

Goal state after:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ i)
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
n✝ : ℕ
⊢ ⊥.extensionProductIter (n✝ + 1) = ⊥

Tactic:
case succ n => rw [extensionProductIter_succ, extensionProduct_bot_left]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P T.obj₃ → P.trW T.mor₁

Tactic:
· intro h
    exact ⟨_, _, _, hT, h⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹⁷ : Category.{v_1, u_1} C
inst✝¹⁶ : HasZeroObject C
inst✝¹⁵ : HasShift C ℤ
inst✝¹⁴ : Preadditive C
inst✝¹³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹² : Pretriangulated C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasZeroObject D
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁶ : Pretriangulated D
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : HasShift E ℤ
P : ObjectProperty C
inst✝³ : P.IsTriangulated
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
n : ℤ
⊢ F.essImage ≤ F.essImage.shift n

Tactic:
rintro Y ⟨X, ⟨e⟩⟩

Goal state after:
C : Type u_1
inst✝¹⁷ : Category.{v_1, u_1} C
inst✝¹⁶ : HasZeroObject C
inst✝¹⁵ : HasShift C ℤ
inst✝¹⁴ : Preadditive C
inst✝¹³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹² : Pretriangulated C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasZeroObject D
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁶ : Pretriangulated D
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : HasShift E ℤ
P : ObjectProperty C
inst✝³ : P.IsTriangulated
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
n : ℤ
Y : D
X : C
e : F.obj X ≅ Y
⊢ F.essImage.shift n Y
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
⊢ Cochain.ofHom (lift φ α β hαβ) = liftCochain φ (Cochain.ofHom α) β lift._proof_1

Tactic:
by
  simp [lift]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
p : ℤ
⊢ (lift φ α β hαβ).f p ≫ (fst φ).f p = α.f p

Tactic:
by
  simp [lift]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
p q : ℤ
hpq : p + -1 = q
⊢ (lift φ α β hαβ).f p ≫ (snd φ).v p q hpq = β.v p q hpq

Tactic:
by
  simp [lift]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ ((K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ opcyclesMap φ (e.f i) ≫ (L.truncGE'XIsoOpcycles e ⋯ hi).inv) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ (K.truncGE'XIso e ⋯ ⋯).hom ≫ φ.f (e.f j) ≫ (L.truncGE'XIso e ⋯ ⋯).inv

Tactic:
simp [truncGE'_d_eq_fromOpcycles _ e hij rfl rfl hi,
        ← cancel_epi (K.pOpcycles (e.f i))]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
by
  by_cases hij : c.Rel i j
  · by_cases hi : e.BoundaryGE i
    · rw [f_eq_iso_hom_pOpcycles_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq_fromOpcycles e hij rfl rfl hi]
      simp [restrictionXIso]
    · rw [f_eq_iso_hom_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq e hij rfl rfl hi]
      simp [restrictionXIso]
  · simp [HomologicalComplex.shape _ _ _ hij]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
⊢ IsIso ((singleFunctor C n).map φ)

Tactic:
change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
⊢ IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ (equiv W L) (chgUniv ((equiv W W.Q).symm f)) = (equiv W L) ((equiv W W.Q).symm f)

Tactic:
dsimp [chgUniv]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ (equiv W L) ((equiv W W.Q).symm ((equiv W W.Q) ((equiv W W.Q).symm f))) = (equiv W L) ((equiv W W.Q).symm f)
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (equiv W L) (f.shift n a' h) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((equiv W L) f) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
by
  dsimp [equiv]
  erw [equiv_shift']
  simp only [Functor.comp_obj, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝⁹ : AddMonoid M
inst✝⁸ : HasShift C₁ M
inst✝⁷ : HasShift C₂ M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
inst✝¹ : W₁.IsCompatibleWithShift M
inst✝ : W₂.IsCompatibleWithShift M
m₀ : M
hm₀ : m₀ = 0
f : X₁ ⟶ Y₁
⊢ Φ.smallShiftedHomMap eX eY (SmallShiftedHom.mk₀ W₁ m₀ hm₀ f) =
    SmallShiftedHom.mk₀ W₂ m₀ hm₀ (eX.inv ≫ Φ.functor.map f ≫ eY.hom)

Tactic:
by
  simp [SmallShiftedHom.mk₀]

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

Goal state before:
pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.g =
    0

Tactic:
simp [← cancel_mono (HomologicalComplex.homologyMap S.g j),
        ← HomologicalComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯
h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯
⊢ α = β

Tactic:
let := HasDerivedCategory.standard C
  rw [Ext.ext_iff] at h₁ h₂ ⊢
  simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂
  apply BinaryCofan.IsColimit.hom_ext
    (isBinaryBilimitOfPreserves (singleFunctor C 0)
      (BinaryBiproduct.isBilimit X₁ X₂)).isColimit
  all_goals assumption

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ hS.singleδ ≫ (shiftFunctor (DerivedCategory C) ↑1).map ((singleFunctor C 0).map S.f) = 0

Tactic:
exact comp_distTriang_mor_zero₃₁ _ hS.singleTriangle_distinguished

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
⊢ (NatIso.op (commShiftIso F 0)).symm = CommShift.isoZero (OppositeShift.functor A F) A

Tactic:
rw [commShiftIso_zero]
    ext
    simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app,
      CommShift.isoZero_inv_app, op_comp, CommShift.isoZero_hom_app]
    erw [oppositeShiftFunctorZero_inv_app, oppositeShiftFunctorZero_hom_app]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
⊢ e₂.inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
have := h (G.obj Y)

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)) ≫ e₂.hom.app (F.obj (G.obj Y))
⊢ e₂.inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : F.CommShift A
inst✝⁶ : G.CommShift A
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝⁴ : HasShift E A
inst✝³ : F'.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : adj.CommShift A
inst✝ : adj'.CommShift A
⊢ NatTrans.CommShift (adj.comp adj').unit A

Tactic:
rw [comp_unit]

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : F.CommShift A
inst✝⁶ : G.CommShift A
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝⁴ : HasShift E A
inst✝³ : F'.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : adj.CommShift A
inst✝ : adj'.CommShift A
⊢ NatTrans.CommShift
    (adj.unit ≫
      Functor.whiskerRight F.rightUnitor.inv G ≫
        Functor.whiskerRight (F.whiskerLeft adj'.unit) G ≫
          Functor.whiskerRight (F.associator F' G').inv G ≫ ((F ⋙ F').associator G' G).hom)
    A
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (opEquiv c).symm (f.comp g h) = ((opEquiv b).symm g).comp ((opEquiv a).symm f) ⋯

Tactic:
rw [opEquiv_symm_apply, opEquiv_symm_apply,
    opShiftFunctorEquivalence_add_unitIso_inv_app_eq _ _ _ _ (show a + b = c by lia), comp, comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop).op ≫
          ((shiftFunctorAdd' C a b c ⋯).inv.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X)))).op ≫
            ((shiftFunctor C b).map
                  ((opShiftFunctorEquivalence C a).unitIso.inv.app
                      ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop).op ≫
              (opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C c).map
        (f ≫ (shiftFunctor Cᵒᵖ a).map g ≫ (shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z