mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₁ ↔ IsIso T.mor₂

Tactic:
by
  rw [T.isZero₁_iff hT]
  constructor
  · intro ⟨h₁, h₃⟩
    have := T.epi₂ hT h₃
    obtain ⟨f, hf⟩ := yoneda_exact₂ T hT (𝟙 _) (by rw [h₁, zero_comp])
    exact ⟨f, hf.symm, by rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]⟩
  · intro
    rw [T.mor₁_eq_zero_iff_mono₂ hT, T.mor₃_eq_zero_iff_epi₂ hT]
    constructor <;> infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ inr φ ≫ (triangle φ).mor₃ = 0

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (Iso.refl (triangle φ).rotate.obj₁).hom =
    (Iso.refl (triangle φ).rotate.obj₃).hom ≫
      (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₃

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
⊢ (S.map (eval C c i)).f ≫ S.X₂.pOpcycles i ≫ k = 0

Tactic:
by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ of V ⋙q (lift φ).toPrefunctor = φ

Tactic:
by
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    rcases φ with ⟨φo, φm⟩
    dsimp [lift, Quiver.Hom.toPath]
    simp

Goal state after:
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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
this : Localization.Construction.lift W.Q ⋯ = 𝟭 W.Localization
⊢ (Localization.Construction.lift W.Q ⋯).IsEquivalence

Tactic:
rw [this]
      infer_instance

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
⊢ P = ⊤

Tactic:
by
  funext X Y f
  ext
  constructor
  · intro
    apply MorphismProperty.top_apply
  · intro
    let G : _ ⥤ W.Localization := Quotient.functor _
    have : G.Full := Quotient.full_functor _
    suffices ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f) by
      rcases X with ⟨⟨X⟩⟩
      rcases Y with ⟨⟨Y⟩⟩
      simpa only [Functor.map_preimage] using! this _ _ (G.preimage f)
    intro X₁ X₂ p
    induction p with
    | nil => simpa only [Functor.map_id] using! hP₁ (𝟙 X₁.obj)
    | @cons X₂ X₃ p g hp =>
      let p' : X₁ ⟶ X₂ := p
      rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
      refine P.comp_mem _ _ hp ?_
      rcases g with (g | ⟨g, hg⟩)
      · apply hP₁
      · apply hP₂

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁ = F₂

Tactic:
suffices F₁.rightOp = F₂.rightOp by
      rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
    have eq' := congr_arg Functor.rightOp eq
    exact h.uniq _ _ eq'

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

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₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor.asEquivalence.functor

Tactic:
rw [MorphismProperty.map_isoClosure]

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₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.map Φ.functor.asEquivalence.functor
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
| W f

Tactic:
rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
| W.inverseImage (shiftFunctor C a) f
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
a : A
⊢ W ≤ W.inverseImage (shiftFunctor C a)

Tactic:
MorphismProperty.IsCompatibleWithShift.condition

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
a : A
⊢ W ≤ W
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
E : Type u_3
inst✝¹ : Category.{v_2, u_3} E
inst✝ : HasShift E A
⊢ ∀ {X Y : C} (x : X ≅ Y), P.shiftClosure A X → P.shiftClosure A Y

Tactic:
rintro X Y i ⟨Z, a, i', hZ⟩

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
E : Type u_3
inst✝¹ : Category.{v_2, u_3} E
inst✝ : HasShift E A
X Y : C
i : X ≅ Y
Z : C
a : A
i' : X ≅ (shiftFunctor C a).obj Z
hZ : P Z
⊢ P.shiftClosure A 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 : C
hX : (⨆ x, P.shift x) X
a : G
ha : P.shift a X
⊢ P.shiftClosure G X

Tactic:
exact ⟨X⟦a⟧, -a, (shiftShiftNeg X a).symm, ha⟩

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (F.shift n₀).obj T.rotate.obj₁, X₂ := (F.shift n₀).obj T.rotate.obj₂, X₃ := (F.shift n₀).obj T.rotate.obj₃,
      f := (F.shift n₀).map T.rotate.mor₁, g := (F.shift n₀).map T.rotate.mor₂, zero := ⋯ } ≅
    { X₁ := (F.shift n₀).obj T.obj₂, X₂ := (F.shift n₀).obj T.obj₃, X₃ := (F.shift n₁).obj T.obj₁,
      f := (F.shift n₀).map T.mor₂, g := F.homologySequenceδ T n₀ n₁ h, zero := ⋯ }

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _)
    ((F.shiftIso 1 n₀ n₁ (by lia)).app _) (by simp) (by simp [homologySequenceδ, shiftMap])

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact

Tactic:
have hS := HomologicalComplex.shortExact_of_degreewise_shortExact S
      (fun n => (σ n).shortExact)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
hS : S.ShortExact
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
          inv (L.mapTriangle.map ψ)).hom₂ ≫
      (L.mapTriangle.map ψ).hom₂ =
    b ≫ (L.mapTriangle.map ψ).hom₂

Tactic:
← comp_hom₂,

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ ((L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
          inv (L.mapTriangle.map ψ)) ≫
        L.mapTriangle.map ψ).hom₂ =
    b ≫ (L.mapTriangle.map ψ).hom₂
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

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

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

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

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
L : C ⥤ D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁸ : Pretriangulated C
inst✝⁷ : HasShift D ℤ
inst✝⁶ : L.CommShift ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ distinguishedTriangles ↔ T ∈ L.essImageDistTriang

Tactic:
by
  constructor
  · intro hT
    let f := L.mapArrow.objPreimage T.mor₁
    obtain ⟨Z, g : f.right ⟶ Z, h : Z ⟶ f.left⟦(1 : ℤ)⟧, mem⟩ :=
      Pretriangulated.distinguished_cocone_triangle f.hom
    exact ⟨_, (exists_iso_of_arrow_iso T _ hT (L.map_distinguished _ mem)
      (L.mapArrow.objObjPreimageIso T.mor₁).symm).choose, mem⟩
  · rintro ⟨T₀, e, hT₀⟩
    exact isomorphic_distinguished _ (L.map_distinguished _ hT₀) _ e

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a a' : ℤ
ha' : n + a = a'
X Y : C
f : X ⟶ Y
⊢ (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map f ≫
      (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom ≫ (single C (ComplexShape.up ℤ) a).map f

Tactic:
by
      obtain rfl : a' = a + n := by lia
      ext
      simp [single]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
R : Type u_1
inst✝¹ : Ring R
n : ℤ
inst✝ : Linear R C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
r : R
⊢ ((singleFunctors C).functor n).map (r • f) = r • ((singleFunctors C).functor n).map f

Tactic:
dsimp [CochainComplex.singleFunctors, HomologicalComplex.single]
    aesop

Goal state after:
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'
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'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
cocone : CokernelCofork (hcone.lift (KernelFork.ofι (K.d i j) ⋯))
hcocone : IsColimit cocone
⊢ hcone.lift (KernelFork.ofι (K.d i j) ⋯) ≫ Cofork.π cocone = 0

Tactic:
exact cocone.condition

Goal state after:
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.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom ≫ K.d j' k' = 0

Tactic:
← cancel_mono (K.restrictionXIso e hk').inv,

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.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom ≫ K.d j' k') ≫ (K.restrictionXIso e hk').inv =
    0 ≫ (K.restrictionXIso e hk').inv
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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i✝ j k : ι
hi : c.prev j = i✝
hk : c.next j = k
i : ι
⊢ (K.truncGE' e).HasHomology i

Tactic:
by_cases hi : e.BoundaryGE i
  · exact ShortComplex.HasHomology.mk' (homologyData K e _ _ _ rfl rfl hi)
  · exact hasHomology_of_not_mem_boundary K e i hi

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✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
by
  rw [← quasiIso_opFunctor_map_iff]
  simp only [← quasiIsoAt_opFunctor_map_iff φ]
  apply quasiIso_truncGEMap_iff

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ 𝟙 A = (singleObjHomologySelfIso c j A).inv ≫ (singleObjHomologySelfIso c j A).hom

Tactic:
Iso.inv_hom_id

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ 𝟙 A = 𝟙 A
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
⊢ map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂ = descShortComplex S₁ ≫ f.τ₃

Tactic:
ext i
  simpa [mappingCone.ext_from_iff _ _ _ rfl, map] using
    congr_fun (congr_arg HomologicalComplex.Hom.f f.comm₂₃) i

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

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

Tactic:
← Ext.comp_assoc (a₁₂ := 1) _ _ _ (by lia) (by lia) (by lia),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ ((Ext.mk₀ S.g).comp hS.extClass comp_extClass_assoc._proof_1_1).comp γ ⋯ = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ hS.extClass.comp ((Ext.mk₀ S.f).comp γ ⋯) h = 0

Tactic:
← Ext.comp_assoc (a₁₂ := 1) _ _ _ (by lia) (by lia) (by lia),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ (hS.extClass.comp (Ext.mk₀ S.f) extClass_comp_assoc._proof_1_1).comp γ ⋯ = 0
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
a b : A
⊢ NatIso.removeOp (commShiftIso (OppositeShift.functor A F) (a + b)).symm =
    CommShift.isoAdd (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) a).symm)
      (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) b).symm)

Tactic:
by
    rw [commShiftIso_add]
    ext
    simp only [NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app,
      CommShift.isoAdd_inv_app, unop_comp, Category.assoc,
      CommShift.isoAdd_hom_app]
    erw [oppositeShiftFunctorAdd_hom_app, oppositeShiftFunctorAdd_inv_app]
    rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (opShiftFunctorEquivalence C p).unitIso.inv.app X =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          (opShiftFunctorEquivalence C n).unitIso.inv.app X

Tactic:
rw [← cancel_mono ((opShiftFunctorEquivalence C p).unitIso.hom.app X), Iso.inv_hom_id_app,
    opShiftFunctorEquivalence_add_unitIso_hom_app_eq _ _ _ _ h,
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc]
  apply Quiver.Hom.unop_inj
  dsimp
  simp only [Category.assoc,
    ← unop_comp, Iso.inv_hom_id_app, Functor.comp_obj, Functor.op_obj, unop_id,
    Functor.map_id, id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
⊢ iso adj 0 = Functor.CommShift.isoZero F A

Tactic:
refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso 0)
      (compatibilityUnit_iso adj 0) ?_

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.commShiftIso G 0)
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
⊢ (Pi.basisFun R ι).toMatrix = transpose

Tactic:
by
  ext M i j
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
x✝¹ x✝ : m → R
hxy : M *ᵥ x✝¹ = M *ᵥ x✝
⊢ M *ᵥ (x✝¹ - x✝) = 0

Tactic:
rw [mulVec_sub, hxy, sub_self]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℤ
⊢ (zpowGroupHom k).ker = rootsOfUnity k.natAbs M

Tactic:
ext; simp

Goal state after: