mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Associator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ((associator.hom.app (X₁ (i₁, i₂, i₃).1)).app (X₂ (i₁, i₂, i₃).2.1)).app (X₃ (i₁, i₂, i₃).2.2) ≫
      (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).ιMapObj r (i₁, i₂, i₃) j h ≫
        (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
ι_mapBifunctorComp₂₃MapObjIso_hom

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ((associator.hom.app (X₁ (i₁, i₂, i₃).1)).app (X₂ (i₁, i₂, i₃).2.1)).app (X₃ (i₁, i₂, i₃).2.2) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: 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
⊢ hom₁ h₁ f₂ F c j j' = 0

Tactic:
ext i₁ i₂ h'
  dsimp [hom₁]
  rw [comp_zero, HomologicalComplex₂.ι_totalDesc]
  by_cases h₃ : c₁.Rel (c₁.prev i₁) i₁
  · rw [ιMapBifunctorOrZero_eq_zero, comp_zero, comp_zero, smul_zero]
    intro h₄
    apply h
    rw [← h', ← h₄]
    exact ComplexShape.rel_π₁ c₂ c h₃ i₂
  · rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]

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

Goal state before:
pp: 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
⊢ biprod.lift f (-g) ≫ biprod.desc inl inr = 0

Tactic:
simp [sq.w]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (HomologicalComplex.sc' ((opEquivalence C).functor.obj (op K)) (m - 1) m (m + 1)).Exact

Tactic:
← ShortComplex.exact_unop_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (HomologicalComplex.sc' ((opEquivalence C).functor.obj (op K)) (m - 1) m (m + 1)).unop.Exact
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
⊢ biprod.lift fst snd ≫ biprod.desc f (-g) = 0

Tactic:
simp [sq.w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
⊢ α ∈ coboundaries K L n ↔ ∃ β, δ m n β = ↑α

Tactic:
by
  simp only [coboundaries, AddSubgroup.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk]
  grind

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

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 : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
let T := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)

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
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
⊢ H c

Tactic:
n

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.le n ≤ t.le (n + ↑c)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
⊢ H c

Tactic:
n

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.ge (n + ↑c) ≤ t.ge n
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case e_a
ι : 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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
⊢ (prevD (e.f i)) h.hom =
    (K.extendXIso e ⋯).hom ≫
      ((prevD i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) ≫
        (L.extendXIso e ⋯).inv

Tactic:
· by_cases hi : c.Rel (c.prev i) i
      · have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
        simp [prevD_eq _ hi, prevD_eq _ hi', L.extend_d_eq _ rfl rfl]
      · rw [prevD_eq_zero _ _ hi]
        by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
        · simp [prevD_eq _ hi', extend_d_to_eq_zero _ _ _ _ _ rfl hi]
        · simp [prevD_eq_zero _ _ hi']

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasCoproduct A
inst✝¹ : HasCoproduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty (f j) p
t : ∐ A ⟶ X
b : ∐ B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
j : J
⊢ (Sigma.ι A j ≫ t) ≫ p = f j ≫ Sigma.ι B j ≫ b

Tactic:
simp [sq.w]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
i : X ⟶ Y
p : Y ⟶ Z
h : i ≫ p = f
inst✝ : HasLiftingProperty f p
⊢ i ≫ p = f ≫ 𝟙 Z

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
i : X ⟶ Y
p : Y ⟶ Z
h : i ≫ p = f
inst✝ : HasLiftingProperty i f
⊢ 𝟙 X ≫ f = i ≫ p

Tactic:
by simp [h]

Goal state after:
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
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
J : Type w
⊢ (trivialFibrations C).IsStableUnderProductsOfShape J

Tactic:
rw [← cofibrations_rlp]
  apply MorphismProperty.rlp_isStableUnderProductsOfShape

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ L.map P.i₀ = L.map P.i₁

Tactic:
have := Localization.inverts L (weakEquivalences C) P.π (by
    rw [← weakEquivalence_iff]
    infer_instance)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
this : IsIso (L.map P.π)
⊢ L.map P.i₀ = L.map P.i₁
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
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ CochainComplex.plus C L

Tactic:
← HomotopyCategory.plus_quotient_obj_iff,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : Plus C
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
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
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc = triangleFunctorNatTransOfLE t a c ⋯

Tactic:
apply NatTrans.ext

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
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app =
    (triangleFunctorNatTransOfLE t a c ⋯).app
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
a : ℤ
⊢ triangleFunctorNatTransOfLE t a a ⋯ = 𝟙 (triangleFunctor t a)

Tactic:
apply NatTrans.ext

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
a : ℤ
⊢ (triangleFunctorNatTransOfLE t a a ⋯).app = (𝟙 (triangleFunctor t a)).app
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case mp
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
n : ℤ
X : C
⊢ t.IsGE X n → IsIso ((t.truncGEπ n).app X)

pp: case mpr
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
n : ℤ
X : C
⊢ IsIso ((t.truncGEπ n).app X) → t.IsGE X n

Tactic:
· intro h
    obtain ⟨e, he⟩ := t.triangle_iso_exists
      (inv_rot_of_distTriang _ (contractible_distinguished X))
      (t.triangleLTGE_distinguished n X) (Iso.refl X) (n - 1) n
      (t.isLE_of_iso (shiftFunctor C (-1 : ℤ)).mapZeroObject.symm _)
      (by dsimp; infer_instance) (by dsimp; infer_instance) (by dsimp; infer_instance)
    dsimp at he
    have : (truncGEπ t n).app X = e.hom.hom₃ := by
      have := e.hom.comm₂
      dsimp at this
      rw [← cancel_epi e.hom.hom₂, ← this, he]
    rw [this]
    infer_instance

Goal state after:
case mpr
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
n : ℤ
X : C
⊢ IsIso ((t.truncGEπ n).app X) → t.IsGE X n
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
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
this : ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0
⊢ f₁ = f₂

Tactic:
by
    rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]

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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
this : ∀ (f : Y ⟶ (t.truncLT n).obj X), f ≫ (t.truncLTι n).app X = 0 → f = 0
⊢ f₁ = f₂

Tactic:
by
    rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]

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 : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ (t.triangleLTLTGELT a b h).obj X ≅ (t.triangleLTGE a).obj ((t.truncLT b).obj X)

Tactic:
refine Triangle.isoMk _ _ ((asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm)
    (Iso.refl _) (Iso.refl _) ?_ (by simp) (by simp)

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 : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ ((t.triangleLTLTGELT a b h).obj X).mor₁ ≫ (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₂).hom =
    (asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm.hom ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case pos
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
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
rw [← eq']

Goal state after:
case pos
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
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ IsIso (t.liftTruncLT m₁ (b - 1) b ⋯)
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₂ : C₂
⊢ (w.structuredArrowDownwards X₂).Initial

Tactic:
rw [guitartExact_iff_initial] at hw
  apply hw

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
⊢ Mono ((ι f n₀).f i)

Tactic:
obtain ⟨q, _⟩ : ∃ (q : ℕ), IsIso ((midπ f n₀ q).f i) :=
      ⟨(i - n₀).natAbs, isIso_midπ_f f n₀ _ i⟩
    exact mono_of_mono_fac (ι_midπ_f f n₀ q i)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
⊢ Φ.IsRightDerivabilityStructure ↔ Φ.op.IsLeftDerivabilityStructure

Tactic:
have eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom :=
    TwoSquare.guitartExact_op_iff _

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
⊢ Φ.IsRightDerivabilityStructure ↔ Φ.op.IsLeftDerivabilityStructure
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + ↑q
⊢ epiWithInjectiveKernel ((midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i)

Tactic:
have := isIso_midπ_f f n₀ q i

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + ↑q
this : IsIso ((midπ f n₀ q).f i)
⊢ epiWithInjectiveKernel ((midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i)
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} C₁
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
⊢ IsIso (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)

Tactic:
have : F.HasPointwiseRightDerivedFunctor W₂ := by
    rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]
    infer_instance

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} C₁
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ IsIso (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)