mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁵ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁴ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
X✝ Y : C₁
inst✝¹ : HasSmallLocalizedHom W₁ X✝ Y
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X✝) (Φ.functor.obj Y)
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X✝ ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor.associator W₂.Q E₂ ≪≫
          Φ.functor.isoWhiskerLeft α₂ ≪≫ e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
X : C₁
⊢ γ.hom.app (W₁.Q.obj X) = E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁵ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁴ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
X Y : C₁
inst✝¹ : HasSmallLocalizedHom W₁ X Y
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
⊢ (SmallHom.equiv W₂ L₂) (Φ.smallHomMap f) = e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) f) ≫ e.inv.app Y

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝² : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y : C₁
inst✝¹ : HasSmallLocalizedHom W₁ X Y
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
f : X ⟶ Y
⊢ Φ.smallHomMap (SmallHom.mk W₁ f) = SmallHom.mk W₂ (Φ.functor.map f)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁵ : HasSmallLocalizedHom W₁ X Y
inst✝⁴ : HasSmallLocalizedHom W₁ Y Z
inst✝³ : HasSmallLocalizedHom W₁ X Z
inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁸ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁷ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁶ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁵ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝⁴ : L₂.IsLocalization W₂
X Y : C₁
inst✝³ : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst✝² : HasSmallLocalizedHom W₂ X' X'
inst✝¹ : HasSmallLocalizedHom W₂ X' Y'
inst✝ : HasSmallLocalizedHom W₂ Y' Y'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
⊢ (SmallHom.equiv W₂ L₂) (Φ.smallHomMap' eX eY f) =
    L₂.map eX.inv ≫ e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) f) ≫ e.inv.app Y ≫ L₂.map eY.hom

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁴ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y : C₁
inst✝³ : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst✝² : HasSmallLocalizedHom W₂ X' X'
inst✝¹ : HasSmallLocalizedHom W₂ X' Y'
inst✝ : HasSmallLocalizedHom W₂ Y' Y'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
f : X ⟶ Y
⊢ Φ.smallHomMap' eX eY (SmallHom.mk W₁ f) = SmallHom.mk W₂ (eX.inv ≫ Φ.functor.map f ≫ eY.hom)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Φ.smallHomMap' eX eZ (f.comp g) = (Φ.smallHomMap' eX eY f).comp (Φ.smallHomMap' eY eZ g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
L : C ⥤ D
inst✝¹ : L.IsLocalization W
inst✝ : L.CommShift M
X Y : C
⊢ HasSmallLocalizedShiftedHom W M X Y ↔
    ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (SmallHom.equiv W L) (f.shift n a' h) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y) ≫
          (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (Functor.commShiftIso L a').inv.app Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (equiv W L) (f.shift n a' h) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((equiv W L) f) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁹ : AddMonoid M
inst✝⁸ : HasShift C M
inst✝⁷ : HasShift D M
L : C ⥤ D
inst✝⁶ : L.IsLocalization W
inst✝⁵ : L.CommShift M
X Y Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ (equiv W L) (f.comp g h) = ((equiv W L) f).comp ((equiv W L) g) h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
L : C ⥤ D
inst✝² : L.IsLocalization W
inst✝¹ : L.CommShift M
X Y : C
inst✝ : HasSmallLocalizedShiftedHom W M X Y
m : M
f : ShiftedHom X Y m
⊢ (SmallHom.equiv W L) (mk W f) = ((Functor.commShiftIso L m).app Y).homToEquiv.symm (f.map L)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
L : C ⥤ D
inst✝² : L.IsLocalization W
inst✝¹ : L.CommShift M
X Y : C
inst✝ : HasSmallLocalizedShiftedHom W M X Y
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
⊢ (equiv W L) (mk₀ W m₀ hm₀ f) = ShiftedHom.mk₀ m₀ hm₀ (L.map f)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
inst✝¹ : HasSmallLocalizedShiftedHom W M Y X
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
⊢ (equiv W L) (mk₀Inv m₀ hm₀ f hf) = ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝¹¹ : AddMonoid M
inst✝¹⁰ : HasShift C M
inst✝⁹ : HasShift D M
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₂₃ + a₁ = a

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C M
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y Y
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ m₀ + m₀ = m₀

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y Y
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk₀ W m₀ hm₀ f).comp (mk₀Inv m₀ hm₀ f hf) ⋯) = (equiv W W.Q) (mk₀ W m₀ hm₀ (𝟙 Y))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M X X
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ m₀ + m₀ = m₀

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
⊢ (composableArrows₂ S₁ i).map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ homologyMap φ.τ₂ i =
    homologyMap φ.τ₁ i ≫ (composableArrows₂ S₂ i).map' 0 1 homMk₁._proof_4 _proof_246✝

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
⊢ (composableArrows₂ S₁ i).map' 1 2 _proof_246✝ _proof_247✝ ≫ homologyMap φ.τ₃ i =
    homologyMap φ.τ₂ i ≫ (composableArrows₂ S₂ i).map' 1 2 _proof_246✝ _proof_247✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M X X
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk₀Inv m₀ hm₀ f hf).comp (mk₀ W m₀ hm₀ f) ⋯) = (equiv W W.Q) (mk₀ W m₀ hm₀ (𝟙 X))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
inst✝² : HasSmallLocalizedShiftedHom W M X Y
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ m₀ + m = m

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
X Y : C
inst✝² : HasSmallLocalizedShiftedHom W M X Y
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ (equiv W W.Q) (α.comp (mk₀ W m₀ hm₀ (𝟙 Y)) ⋯) = (equiv W W.Q) α

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
X Y : C
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M X X
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ m + m₀ = m

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
X Y : C
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M X X
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ (equiv W W.Q) ((mk₀ W m₀ hm₀ (𝟙 X)).comp α ⋯) = (equiv W W.Q) α

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C M
inst✝⁸ : HasShift D M
X Y Z : C
inst✝⁷ : W.RespectsIso
inst✝⁶ : W.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M X Z
inst✝² : HasSmallLocalizedShiftedHom W M Z Y
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
f : Y ⟶ Z
hf : W f
a : M
α : SmallShiftedHom W X Y a
⊢ (fun β ↦ β.comp (mk₀Inv 0 ⋯ f hf) ⋯) ((fun α ↦ α.comp (mk₀ W 0 ⋯ f) ⋯) α) = α

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C M
inst✝⁸ : HasShift D M
X Y Z : C
inst✝⁷ : W.RespectsIso
inst✝⁶ : W.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M X Z
inst✝² : HasSmallLocalizedShiftedHom W M Z Y
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
f : Y ⟶ Z
hf : W f
a : M
β : SmallShiftedHom W X Z a
⊢ (fun α ↦ α.comp (mk₀ W 0 ⋯ f) ⋯) ((fun β ↦ β.comp (mk₀Inv 0 ⋯ f hf) ⋯) β) = β

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝¹¹ : AddMonoid M
inst✝¹⁰ : HasShift C M
inst✝⁹ : HasShift D M
X Y Z : C
inst✝⁸ : W.RespectsIso
inst✝⁷ : W.IsCompatibleWithShift M
inst✝⁶ : HasSmallLocalizedShiftedHom W M X X
inst✝⁵ : HasSmallLocalizedShiftedHom W M Y Y
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y X
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
f : X ⟶ Y
hf : W f
a : M
α : SmallShiftedHom W Y Z a
⊢ (fun β ↦ (mk₀Inv 0 ⋯ f hf).comp β ⋯) ((fun α ↦ (mk₀ W 0 ⋯ f).comp α ⋯) α) = α

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝¹¹ : AddMonoid M
inst✝¹⁰ : HasShift C M
inst✝⁹ : HasShift D M
X Y Z : C
inst✝⁸ : W.RespectsIso
inst✝⁷ : W.IsCompatibleWithShift M
inst✝⁶ : HasSmallLocalizedShiftedHom W M X X
inst✝⁵ : HasSmallLocalizedShiftedHom W M Y Y
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y X
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
f : X ⟶ Y
hf : W f
a : M
β : SmallShiftedHom W X Z a
⊢ (fun α ↦ (mk₀ W 0 ⋯ f).comp α ⋯) ((fun β ↦ (mk₀Inv 0 ⋯ f hf).comp β ⋯) β) = β

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
⊢ Mono (homologyMap φ.τ₃ i)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₂.g
eq : homologyMap φ.τ₂ i ≫ homologyMap S₂.g i = homologyMap S₁.g i ≫ homologyMap φ.τ₃ i
⊢ ∀ (j : ι), ¬c.Rel i j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono (homologyMap φ.τ₁ j)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
⊢ Epi (homologyMap φ.τ₁ j)

Tactic:
by

Goal state after: