mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁶ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝⁵ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
this : ObjectProperty.EssentiallySmall.{w, v, u} (Q.isoClosure.limitsClosure J)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)

Tactic:
exact .of_le (limitsClosure_monotone J hQ₂)

Goal state after:
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
a : A
⊢ (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a

Tactic:
ext

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
a : A
x✝ : C
⊢ (P ⊔ Q).shift a x✝ ↔ (P.shift a ⊔ Q.shift a) x✝
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
ι : Sort u_4
P : ι → ObjectProperty C
a : A
⊢ (⨆ i, P i).shift a = ⨆ i, (P i).shift a

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
ι : Sort u_4
P : ι → ObjectProperty C
a : A
x✝ : C
⊢ (⨆ i, P i).shift a x✝ ↔ (⨆ i, (P i).shift a) x✝
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ ↔ LeftFractionRel f g

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯ → LeftFractionRel f g

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
⊢ LeftFractionRel f g → (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
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✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁

Tactic:
← shiftMap_comp',

Goal state after:
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✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap (φ.hom₃ ≫ T'.mor₃) n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : X ⟶ Y
⊢ ∃ φ, e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map L ⋯

Tactic:
obtain ⟨g, rfl⟩ := MorphismProperty.LeftFraction.Localization.Hom.mk_surjective g

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : W.LeftFraction X Y
⊢ ∃ φ, e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk g) ≫ e.hom.app Y = φ.map L ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ LeftFractionRel φ ψ

Tactic:
constructor

Goal state after:
case mp
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → LeftFractionRel φ ψ

case mpr
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ LeftFractionRel φ ψ → φ.map L ⋯ = ψ.map L ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map f₁ = L.map f₂ ↔ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
constructor

Goal state after:
case mp
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map f₁ = L.map f₂ → ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

case mpr
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ (∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s) → L.map f₁ = L.map f₂
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 ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
constructor

Goal state after:
case mp
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 ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) → ∀ (n : ℤ), IsIso ((F.shift n).map f)

case mpr
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 ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ (∀ (n : ℤ), IsIso ((F.shift n).map f)) → ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ (φ.map L ⋯).op = (ψ.map L ⋯).op

Tactic:
constructor

Goal state after:
case mp
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → (φ.map L ⋯).op = (ψ.map L ⋯).op

case mpr
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ (φ.map L ⋯).op = (ψ.map L ⋯).op → φ.map L ⋯ = ψ.map L ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ ↔ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
constructor

Goal state after:
case mp
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ → ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

case mpr
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ (∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: case mpr
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 ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
a✝ : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n✝ : ℤ
⊢ Epi ((F.shift n✝).map f) ∧ Mono ((F.shift (n✝ + 1)).map f)

Tactic:
constructor

Goal state after:
case mpr.left
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 ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
a✝ : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n✝ : ℤ
⊢ Epi ((F.shift n✝).map f)

case mpr.right
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 ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
a✝ : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n✝ : ℤ
⊢ Mono ((F.shift (n✝ + 1)).map f)
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
⊢ (mk₀ m₀ hm₀ (𝟙 X)).comp f ⋯ = f

Tactic:
simp [mk₀_comp]

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

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

Tactic:
constructor

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

case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ 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.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
X Y Z : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms
a : M
β : ShiftedHom X Y a
b c : M
h : b + a = c
⊢ β ≫ (shiftFunctor C a).map 0 ≫ (shiftFunctorAdd' C b a c h).inv.app Z = 0

Tactic:
Functor.map_zero,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
X Y Z : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms
a : M
β : ShiftedHom X Y a
b c : M
h : b + a = c
⊢ β ≫ 0 ≫ (shiftFunctorAdd' C b a c h).inv.app Z = 0
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

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

Tactic:
constructor

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

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P ≤ Q → P.retracts ≤ Q
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
X Y Z : C
R : Type u_5
inst✝³ : Ring R
inst✝² : Preadditive C
inst✝¹ : Linear R C
inst✝ : ∀ (a : M), Functor.Linear R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α ≫ (r • (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z) =
    r • α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
Linear.comp_smul

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
X Y Z : C
R : Type u_5
inst✝³ : Ring R
inst✝² : Preadditive C
inst✝¹ : Linear R C
inst✝ : ∀ (a : M), Functor.Linear R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ r • α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    r • α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
X Y Z : C
R : Type u_5
inst✝³ : Ring R
inst✝² : Preadditive C
inst✝¹ : Linear R C
inst✝ : ∀ (a : M), Functor.Linear R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (r • β) h = r • α.comp β h

Tactic:
rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]

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:
constructor

Goal state after:
case mp
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

case mpr
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 ∈ L.essImageDistTriang → T ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q R : ObjectProperty C
inst✝ : IsTriangulated C
X : C
⊢ (P.extensionProduct Q).extensionProduct R X ↔ P.extensionProduct (Q.extensionProduct R) X

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q R : ObjectProperty C
inst✝ : IsTriangulated C
X : C
⊢ (P.extensionProduct Q).extensionProduct R X → P.extensionProduct (Q.extensionProduct R) X

case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q R : ObjectProperty C
inst✝ : IsTriangulated C
X : C
⊢ P.extensionProduct (Q.extensionProduct R) X → (P.extensionProduct Q).extensionProduct R X
Module: Mathlib.Algebra.Homology.ShortComplex.Retract

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        ⋯ ≫
      Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        ⋯ =
    𝟙 (Arrow.mk (homologyMap f₁))

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.Hom.left
      (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯ ≫
        Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (homologyMap f₁)))

case h₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.Hom.right
      (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯ ≫
        Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (homologyMap f₁)))
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i ↔ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i → ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) → QuasiIsoAt f i