mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.nonDegenerate n → x ∈ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)

Tactic:
hx

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ x ∈ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
⊢ (Equiv.ofBijective (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯) a ≤
      (Equiv.ofBijective (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯) b ↔
    a ≤ b

Tactic:
simp only [Equiv.ofBijective_apply, Subtype.mk_le_mk, OrderEmbedding.le_iff_le]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
by
        cases j <;> simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
by
        cases j <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
⊢ (↾fun x ↦ objMk ((OrderHom.const (Fin ((unop (op ⦋0⦌)).len + 1))) 0)) ≫ (stdSimplex.obj Δ).hom.app (op ⦋0⦌) =
    𝟙 (stdSimplex.obj Δ).right

Tactic:
dsimp
    subsingleton

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ↑({ toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨x, ⋯⟩) = ↑⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩

Tactic:
← yonedaEquiv.right_inv x

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ↑({ toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨yonedaEquiv.toFun (yonedaEquiv.invFun x), ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (X.map u)) (yonedaEquiv.toFun (yonedaEquiv.invFun x)), ⋯⟩
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)

Tactic:
apply Associative.ε₂_eq_mul

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

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • K.d₁ c i₁ i₂ j' =
    K.flip.d₂ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
K.d₁_eq _ h₂ _ _ h₄,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₁ c₂ c (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    K.flip.d₂ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫
      (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) =
    (x * y).negOnePow •
      ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫
        (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫
          (shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F)

Tactic:
ext1
  dsimp [mapBifunctorShift₁Iso, mapBifunctorShift₂Iso]
  rw [Functor.map_comp, Functor.map_comp, assoc, assoc, assoc,
    ← HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc,
    HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom,
    ← HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc,
    Linear.comp_units_smul, Linear.comp_units_smul,
    smul_left_cancel_iff,
    ← HomologicalComplex₂.total.map_comp_assoc,
    ← HomologicalComplex₂.total.map_comp_assoc,
    ← HomologicalComplex₂.total.map_comp_assoc]
  congr 2
  ext a b
  dsimp [HomologicalComplex₂.shiftFunctor₁₂CommIso]
  simp only [id_comp]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
this : Mono S.f
⊢ (ConcreteCategory.hom 0) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f k))) 0

Tactic:
map_zero

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
this : Mono S.f
⊢ (ConcreteCategory.hom 0) x₂ = 0
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos.h
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₁₂ : ι₁₂ := ⋯
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'

Tactic:
rw [← h₄, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : mk x = 0
⊢ toHom 0 = 0

Tactic:
map_zero

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : mk x = 0
⊢ 0 = 0
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
n : ℤ
X : C
i : ℤ
h✝ : t.IsLE X i
⊢ t.minus.shift n X

Tactic:
exact ⟨i - n, t.isLE_shift _ i _ _ (by omega)⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n i : ℤ
hi : i < n
hX : X.IsGE n
⊢ IsZero ((homologyFunctor C i).obj X)

Tactic:
rw [isGE_iff] at hX

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n i : ℤ
hi : i < n
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
⊢ IsZero ((homologyFunctor C i).obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type w
⊢ T.colimitsOfShape (Discrete J) ≤ T.rlp.llp

Tactic:
by
  intro A B i hi
  exact MorphismProperty.colimitsOfShape_le _ (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : ∃ J, T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i

Tactic:
obtain ⟨J, hi⟩ := hi

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
J : Type w
hi : T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
⊢ LeftHomotopyRel.FactorsThroughLocalization (weakEquivalences C)

Tactic:
by
  rintro X Y f g ⟨P, ⟨h⟩⟩
  let L := (weakEquivalences C).Q
  rw [areEqualizedByLocalization_iff L]
  suffices L.map P.i₀ = L.map P.i₁ by
    simp only [← h.h₀, ← h.h₁, L.map_comp, this]
  have := Localization.inverts L (weakEquivalences C) P.π (by
    rw [← weakEquivalence_iff]
    infer_instance)
  simp [← cancel_mono (L.map P.π), ← L.map_comp, P.i₀_π, P.i₁_π]

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
P : PathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ ∃ P', P'.IsGood ∧ Nonempty (P'.RightHomotopy f g)

Tactic:
by
  let d := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
  exact
   ⟨{ P := d.Z
      p₀ := d.p ≫ prod.fst
      p₁ := d.p ≫ prod.snd
      ι := P.ι ≫ d.i }, ⟨by
        rw [fibration_iff]
        convert! d.hp
        aesop⟩, ⟨{ h := h.h ≫ d.i }⟩⟩

Goal state after:
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
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ (singleFunctor C n).Additive

Tactic:
dsimp [singleFunctor, singleFunctors]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ (singleFunctor C n).Additive

Tactic:
dsimp [singleFunctor, singleFunctors]
  infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
φ' : (A.ι ⋙ L₂).obj X₁ ⟶ (A.ι ⋙ L₂).obj X₂
hφ' : φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂
f : B.trW.LeftFraction (A.ι.obj X₁) (A.ι.obj X₂)
hf : φ' = f.map L₂ ⋯
X₃ : C
s' : A.ι.obj X₂ ⟶ X₃
a : f.Y' ⟶ X₃
hX₃ : A X₃
hs' : (A ⊓ B).trW s'
fac : f.s ≫ a = s'
⊢ (B.inverseImage A.ι).trW (homMk s')

Tactic:
by rwa [trW_inverseImage_ι_iff]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝² : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝¹ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := homMk t
⊢ (B.inverseImage A.ι).trW t'

Tactic:
by rwa [trW_inverseImage_ι_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
⊢ ∀ ⦃X Y : ℕ⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
by
    intro i j φ
    obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le (leOfHom φ)
    obtain rfl := Subsingleton.elim φ (homOfLE (by lia))
    revert i j
    induction k with
    | zero =>
        intro i j hk
        obtain rfl : j = i := by lia
        simp
    | succ k hk =>
        intro i j hk'
        obtain rfl : j = i + k + 1 := by lia
        simp only [← homOfLE_comp (show i ≤ i + k by lia) (show i + k ≤ i + k + 1 by lia),
          Functor.map_comp, assoc, naturality, reassoc_of% (hk rfl)]

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
this : QuasiIsoAt f i
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.g i,
        g := ⋯.δ i (i + 1) ⋯, zero := ⋯ }.f =
    0

Tactic:
← ((shortExact f).homology_exact₂ i).epi_f_iff

Goal state after:
case refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
this : QuasiIsoAt f i
⊢ Epi
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        f := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.f i,
        g := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.g i, zero := ⋯ }.f
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution X₂)
inst✝² : Φ.arrow.HasLeftResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
this✝ : Φ.op.arrow.HasRightResolutions
this : ∀ (X₂ : C₂ᵒᵖ), IsConnected (Φ.op.RightResolution X₂)
⊢ Φ.op.IsRightDerivabilityStructure

Tactic:
exact IsRightDerivabilityStructure.mk' _

Goal state after:
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
F : C₁ ⥤ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) := (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
⊢ IsConnected ((mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g)

Tactic:
have φ : ∀ (X : Z), X₀ ⟶ X := fun X =>
    StructuredArrow.homMk (CostructuredArrow.homMk X.hom.left
      (by simpa using! CostructuredArrow.w X.hom))

Goal state after:
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
F : C₁ ⥤ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) := (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
⊢ IsConnected ((mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g)
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ W.Q.HasLeftKanExtension F ↔ F'.HasRightDerivedFunctor W

Tactic:
hasRightDerivedFunctor_iff F' W.Q W,

Goal state after:
C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F'
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₂
X : C₁
⊢ IsIso (α₁.app X) ↔ IsIso (α₂.app (Φ.functor.obj X))

Tactic:
rw [← isIso_comp_right_iff (α₁.app X)
    ((Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂).app (L₁.obj X)),
    rightDerivedFunctorComparison_fac_app, isIso_comp_right_iff]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
obtain ⟨Y, ⟨eY⟩⟩ := DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE (Q.obj L) b

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
Y : C
eY : Q.obj L ≅ (singleFunctor C b).obj Y
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i j : β
h : (ComplexShape.up' b).Rel i j
⊢ f.f i ≫
      { X := fun i ↦ Y.obj i, d := fun i j ↦ if h : i + b = j then Y.d i ≫ Y.objEqToHom ⋯ else 0, shape := ⋯,
            d_comp_d' := ⋯ }.d
        i j =
    { X := fun i ↦ X.obj i, d := fun i j ↦ if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0, shape := ⋯,
            d_comp_d' := ⋯ }.d
        i j ≫
      f.f j

Tactic:
dsimp at h ⊢
        subst h
        have : f.f i ≫ Y.d i = X.d i ≫ f.f _ := (congr_fun f.comm i).symm
        simp only [dite_true, Category.assoc, eqToHom_f', reassoc_of% this]

Goal state after: