mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ : C
⊢ ∀ {Z W : C} {f : X✝ ⟶ Y✝} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ : C
⊢ ∀ {W : C} {f : X✝ ⟶ Y✝} {g : Z✝ ⟶ W} (h : RetractArrow f g), P g → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ : C
⊢ ∀ {W : C} {f : X✝ ⟶ Y✝} {g : Z✝ ⟶ W} (h : RetractArrow f g), P g → P f

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
⊢ ∀ {f : X✝ ⟶ Y✝} {g : Z✝ ⟶ W✝} (h : RetractArrow f g), P g → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
⊢ ∀ {f : X✝ ⟶ Y✝} {g : Z✝ ⟶ W✝} (h : RetractArrow f g), P g → P f

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ∀ {g : Z✝ ⟶ W✝} (h : RetractArrow f✝ g), P g → P f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ∀ {g : Z✝ ⟶ W✝} (h : RetractArrow f✝ g), P g → P f✝

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
⊢ ∀ (h : RetractArrow f✝ g✝), P g✝ → P f✝
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₁✝ : 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)

Tactic:
_

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₁✝ 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 inl
ι : 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 : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj' : e.r j' = none
⊢ (K.extend e).d i' j' = 0

pp: case inr
ι : 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 : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extend e).d i' j' = 0

Tactic:
· exact extend.d_none_eq_zero' _ _ _ hj'

Goal state after:
case inr
ι : 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 : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extend e).d i' j' = 0
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
⊢ 0 = K.d i' j' ≫ f φ j'

Tactic:
have : f φ j' = 0 := by
          apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this✝ : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
this : f φ j' = 0
⊢ 0 = K.d i' j' ≫ f φ j'
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
i : ι
hi : e.f i = i'
⊢ (e.liftExtend φ hφ).f i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv

Tactic:
by
  apply liftExtend.f_eq

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

Goal state before:
pp: case neg
ι : 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 : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d k k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
rw [shape _ _ _ hjk, zero_comp, comp_zero,
        K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hk' hj]

Goal state after:
case neg
ι : 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 : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ 0 =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫
        ((K.restrictionXIso e hk').hom ≫ K.pOpcycles (c'.next j') ≫ (K.truncGE'XIsoOpcycles e hk' hj).inv) ≫
          ((K.truncGE' e).extendXIso e hk').inv
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'
j : ι
hj : e.BoundaryGE j
i' : ι'
⊢ c'.Rel i' (e.f j) → K.d i' (e.f j) ≫ (K.restrictionToTruncGE' e).f j = 0

Tactic:
_

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'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionToTruncGE' e).f j = 0
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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝² : ∀ (j : ι), K.HasHomology j
inst✝¹ : ∀ (j : ι), L.HasHomology j
inst✝ : QuasiIso φ
⊢ QuasiIso (extendMap φ e)

Tactic:
by
  rwa [quasiIso_extendMap_iff]

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 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'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
⊢ IsIso (K.πTruncGE e)

Tactic:
suffices ∀ (i' : ι'), IsIso ((K.πTruncGE e).f i') by
    apply Hom.isIso_of_components

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 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'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
⊢ ∀ (i' : ι'), IsIso ((K.πTruncGE e).f i')
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ Mono (K.shortComplexTruncLE e).f

Tactic:
dsimp [shortComplexTruncLE]
  infer_instance

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ Epi (K.shortComplexTruncLE e).g

Tactic:
dsimp [shortComplexTruncLE]
  infer_instance

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

Goal state before:
pp: case hL
ι : 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 L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ L.IsStrictlySupportedOutside e₁

Tactic:
rw [ac.isStrictlySupportedOutside₁_iff]

Goal state after:
case hL
ι : 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 L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ L.IsStrictlySupported e₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HasExt C ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
dsimp [HasExt]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C),
      HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ
        ((CochainComplex.singleFunctor C 0).obj X) ((CochainComplex.singleFunctor C 0).obj Y)) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))
⊢ ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
X

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))
X : C
⊢ ∀ (Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
⊢ ∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
X

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X : C
⊢ ∀ (Y : C) (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))
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
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i b✝ : J
⊢ b✝ ∈ Finset.univ → b✝ ≠ i → (mk₀ (c.ι i ≫ c.π b✝)).comp (x✝ b✝) ⋯ = 0

Tactic:
_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i b✝ : J
a✝ : b✝ ∈ Finset.univ
⊢ b✝ ≠ i → (mk₀ (c.ι i ≫ c.π b✝)).comp (x✝ b✝) ⋯ = 0
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
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i b✝ : J
⊢ b✝ ∈ Finset.univ → b✝ ≠ i → (x✝ b✝).comp (mk₀ (c.ι b✝ ≫ c.π i)) ⋯ = 0

Tactic:
_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i b✝ : J
a✝ : b✝ ∈ Finset.univ
⊢ b✝ ≠ i → (x✝ b✝).comp (mk₀ (c.ι b✝ ≫ c.π i)) ⋯ = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
⊢ ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)

Tactic:
X

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X : C
⊢ ∀ (Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)
⊢ ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
X

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)
X : C
⊢ ∀ (Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ {
      X₁ :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                mono_of_epi_of_mono_of_mono'._proof_4)
              ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                mono_of_epi_of_mono_of_mono'._proof_7)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rw [ShortComplex.exact_iff_epi _ (by simp)]
    exact hR₁'

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
a : R
f : X ⟶ Y
⊢ a • f = f ≫ (φ a).app Y

Tactic:
by
  rw [smulOfRingMorphism_smul_eq]
  exact ((φ a).naturality f).symm

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
⊢ Functor.Linear R G

Tactic:
rw [Functor.linear_iff]

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
⊢ ∀ (X : D) (r : R), G.map (r • 𝟙 X) = r • 𝟙 (G.obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : QuasiIso π
g : K ⟶ L
⊢ IsSplitEpi π

Tactic:
exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.postcomp X h) = 0

Tactic:
by
        ext x
        dsimp
        simp only [comp_assoc_of_second_deg_zero, ShortComplex.ShortExact.comp_extClass,
          comp_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ y ∈ Submodule.orthogonalBilin B (K ∙ x) ↔ y ∈ (B x).ker

Tactic:
simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]

Goal state after:
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → (B n) y = 0) ↔ (B x) y = 0