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

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
⊢ τ = τ'

Tactic:
ext 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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
Y : D
⊢ τ.app Y = τ'.app Y
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (X : W.FunctorsInverting D), (inverse W D ⋙ functor W D).obj X = (𝟭 (W.FunctorsInverting D)).obj X

Tactic:
rintro ⟨G, hG⟩

Goal state after:
case refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG✝ : W.IsInvertedBy G✝
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ (inverse W D ⋙ functor W D).obj { obj := G, property := hG } =
    (𝟭 (W.FunctorsInverting D)).obj { obj := G, property := hG }
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac :
  { X' := z₂.Y', s := z₃.s, hs := ⋯, f := z₃'.s }.f ≫ z₄.s = { X' := z₂.Y', s := z₃.s, hs := ⋯, f := z₃'.s }.s ≫ z₄.f
⊢ LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')

Tactic:
dsimp at fac

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
⊢ LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT (↑(S i)) κ
⊢ HasCardinalLT (↑(⋃ i, S i)) κ

Tactic:
convert! show HasCardinalLT (Set.ofPred ((⨆ i, S i))) κ from hasCardinalLT_subtype_iSup S hι hS

Goal state after:
ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT (↑(S i)) κ
⊢ ⋃ i, S i = Set.ofPred (⨆ i, S i)
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ P Y

Tactic:
let h : IsColimit (BinaryCofan.mk (initial.to Y) e.hom) :=
      BinaryCofan.IsColimit.mk _ (fun _ f ↦ e.inv ≫ f) (by cat_disch) (by simp) (by cat_disch)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
h : IsColimit (BinaryCofan.mk (initial.to Y) e.hom) :=
  BinaryCofan.IsColimit.mk (BinaryCofan.mk (initial.to Y) e.hom) (fun {T} x f ↦ e.inv ≫ f) ⋯ ⋯ ⋯
⊢ P Y
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ ⨆ x, P.shift x ≤ P.shiftClosure G

Tactic:
· intro X hX
    obtain ⟨a, ha⟩ := (prop_iSup_iff _ _).mp hX
    exact ⟨X⟦a⟧, -a, (shiftShiftNeg X a).symm, ha⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P.shiftClosure G = ⨆ x, P.shift x

Tactic:
apply le_antisymm
  · rw [shiftClosure_le_iff]
    conv_lhs => rw [← P.shift_zero G]
    exact le_iSup P.shift (0 : G)
  · intro X hX
    obtain ⟨a, ha⟩ := (prop_iSup_iff _ _).mp hX
    exact ⟨X⟦a⟧, -a, (shiftShiftNeg X a).symm, ha⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone retracts

Tactic:
intro _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ : MorphismProperty C
⊢ ∀ ⦃b : MorphismProperty C⦄, a✝ ≤ b → a✝.retracts ≤ b.retracts
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q ↔ P ≤ Q

Tactic:
constructor
  · exact le_trans P.le_retracts
  · intro h
    exact le_trans (retracts_monotone h) Q.retracts_le

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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ (f.map F).comp (mk₀ 0 ⋯ (τ.app Y)) ⋯ = (mk₀ 0 ⋯ (τ.app X)).comp (f.map G) ⋯

Tactic:
rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]

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 : ObjectProperty C
⊢ ⊥.extensionProduct P ≤ ⊥

Tactic:
intro _

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 : ObjectProperty C
i✝ : C
⊢ ⊥.extensionProduct P i✝ ≤ ⊥ i✝
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 : ObjectProperty C
⊢ P.extensionProduct ⊥ ≤ ⊥

Tactic:
intro _

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 : ObjectProperty C
i✝ : C
⊢ P.extensionProduct ⊥ i✝ ≤ ⊥ i✝
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₁ P₂ Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h₁ : P₁ ≤ Q
h₂ : P₂ ≤ Q
⊢ P₁.extensionProduct P₂ ≤ Q.isoClosure

Tactic:
intro _

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₁ P₂ Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h₁ : P₁ ≤ Q
h₂ : P₂ ≤ Q
i✝ : C
⊢ P₁.extensionProduct P₂ i✝ ≤ Q.isoClosure i✝
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₁ P₂ Q : ObjectProperty C
inst✝¹ : Q.IsTriangulatedClosed₂
inst✝ : Q.IsClosedUnderIsomorphisms
h₁ : P₁ ≤ Q
h₂ : P₂ ≤ Q
⊢ P₁.extensionProduct P₂ ≤ Q

Tactic:
intro _

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₁ P₂ Q : ObjectProperty C
inst✝¹ : Q.IsTriangulatedClosed₂
inst✝ : Q.IsClosedUnderIsomorphisms
h₁ : P₁ ≤ Q
h₂ : P₂ ≤ Q
i✝ : C
⊢ P₁.extensionProduct P₂ i✝ ≤ Q i✝
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 : ObjectProperty C
n✝ : P.ContainsZero
n m✝ m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter n ≤ P.extensionProductIter (m + 1)

Tactic:
refine le_trans h ?_
    rw [extensionProductIter_succ]
    exact le_extensionProduct_right P

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 : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : P.trW f
n : ℤ
⊢ P.trW ((shiftFunctor C n).map f)

Tactic:
rw [← smul_mem_trW_iff _ _ (n.negOnePow)]
  obtain ⟨X₃, g, h, hT, mem⟩ := hf
  exact ⟨_, _, _, Pretriangulated.Triangle.shift_distinguished _ hT n, P.le_shift _ _ mem⟩

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✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.trW f → P.trW g → P.trW (f ≫ g)

Tactic:
rw [← trW_isoClosure]
    rintro X₁ X₂ X₃ u₁₂ u₂₃ ⟨Z₁₂, v₁₂, w₁₂, H₁₂, mem₁₂⟩ ⟨Z₂₃, v₂₃, w₂₃, H₂₃, mem₂₃⟩
    obtain ⟨Z₁₃, v₁₃, w₁₂, H₁₃⟩ := distinguished_cocone_triangle (u₁₂ ≫ u₂₃)
    exact ⟨_, _, _, H₁₃, P.isoClosure.ext_of_isTriangulatedClosed₂
      _ (someOctahedron rfl H₁₂ H₂₃ H₁₃).mem mem₁₂ mem₂₃⟩

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
J : Type
x✝ : Finite J
⊢ ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), P.isoClosure.trW (f j)) → P.isoClosure.trW (Limits.Pi.map f)

Tactic:
intro _

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
J : Type
x✝ : Finite J
X₁✝ : J → C
⊢ ∀ (X₂ : J → C) [inst : HasProduct X₁✝] [inst_1 : HasProduct X₂] (f : (j : J) → X₁✝ j ⟶ X₂ j),
    (∀ (j : J), P.isoClosure.trW (f j)) → P.isoClosure.trW (Limits.Pi.map f)
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
K.extend_d_eq e hi hj,

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' =
    ((K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv) ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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 k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
have : (K.restriction e).HasHomology j :=
    restriction.hasHomology K e i j k hi hk rfl rfl rfl
      (e.prev_f_of_not_boundaryGE hi hj) (e.next_f hk)

Goal state after:
ι : 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 k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this : (K.restriction e).HasHomology j
⊢ ((K.truncGE' e).sc' i j k).HasHomology
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv =
    (K.extendXIso e hj').hom ≫ (K.sc' i j k).g ≫ (K.extendXIso e hk'').inv

Tactic:
shortComplexFunctor'_obj_g

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv =
    (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.homologyπ j' ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ≫ (K.restriction e).homologyπ j

Tactic:
← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,

Goal state after:
ι : 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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ (K.homologyπ j' ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv) ≫
      (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom =
    ((K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ≫ (K.restriction e).homologyπ j) ≫
      (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case mp
ι : 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'
inst✝ : HasZeroObject C
⊢ (K.truncGE e).Acyclic → K.IsSupportedOutside e

Tactic:
intro hK
    exact ⟨fun i ↦ by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)⟩

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

Goal state before:
pp: case mpr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
⊢ K.IsStrictlySupported e₂ → K.IsStrictlySupportedOutside e₁

Tactic:
intro _

Goal state after:
case mpr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
a✝ : K.IsStrictlySupported e₂
⊢ K.IsStrictlySupportedOutside e₁
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case mpr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
⊢ K.IsSupported e₂ → K.IsSupportedOutside e₁

Tactic:
intro _

Goal state after:
case mpr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
a✝ : K.IsSupported e₂
⊢ K.IsSupportedOutside e₁
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyGE n → ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)

Tactic:
intro _

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero (K.X i)

Tactic:
intro _

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyLE n
⊢ ∀ (i : ℤ), n < i → IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n → ∀ i < n, ExactAt K i

Tactic:
intro _

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsGE n
⊢ ∀ i < n, ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i

Tactic:
intro _

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsLE n
⊢ ∀ (i : ℤ), n < i → ExactAt K i
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomotopyCategory C (ComplexShape.up ℤ)
s : X' ⟶ { as := X }
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
g : X' ⟶ { as := Y }
hφ : f = { X' := X', s := s, hs := hs, f := g }.map Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X' ⟶ { as := X }
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X' ⟶ { as := Y }
hφ : f = { X' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X', s := s, hs := hs, f := g }.map Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomotopyCategory C (ComplexShape.up ℤ)
g : { as := X } ⟶ X'
s : { as := Y } ⟶ X'
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
hφ : f = { Y' := X', f := g, s := s, hs := hs }.map Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
g : { as := X } ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X'
s : { as := Y } ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X'
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
hφ : f = { Y' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X', f := g, s := s, hs := hs }.map Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
⊢ IsIso (Q.map (CochainComplex.truncGEMap s n))

Tactic:
rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i