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

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z✝
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s
Z : C
p : u.Y' ⟶ Z
hp : W p
fac₄ : z₁.f ≫ w₁.f ≫ u.f ≫ p = z₂.f ≫ w₂.f ≫ u.s ≫ p
⊢ (a.f ≫ z₁.f) ≫ w₁.f ≫ u.f ≫ p = (a.f ≫ z₂.f) ≫ w₂.f ≫ u.s ≫ p

Tactic:
simp only [assoc, fac₄]

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀

Tactic:
rw [← transfiniteIterate_succ φ i₀ j₁ hj₁]

Goal state after:
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isSuccLimit
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : Order.IsSuccLimit b
hb' : ∀ b_1 < b, P.strictLimitsClosureIter J b_1 ≤ P.limitsClosure J
⊢ P.strictLimitsClosureIter J b ≤ P.limitsClosure J

Tactic:
simp only [transfiniteIterate_limit _ _ _ hb,
      iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro c hc
    exact hb' _ hc

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case inr
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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
hF : ∀ (j : J a), ∃ a_1 < κ.ord, transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) a_1 P (F.obj j)
⊢ P.strictLimitsClosureIter J κ.ord (limit F)

Tactic:
choose o ho ho' using hF

Goal state after:
case inr
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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
⊢ P.strictLimitsClosureIter J κ.ord (limit F)
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) κ
a : α
| (P.strictLimitsClosureIter J κ.ord).isoClosure

Tactic:
rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]

Goal state after:
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) κ
a : α
| ((P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J).isoClosure
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_3.refine_2
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
Z : C
u : w₂.Y' ⟶ Z
hu : W u
fac₄ : z₂.f ≫ w₂.s ≫ u = t₂ ≫ w₂.f ≫ u
⊢ (a₂.f ≫ t₂ ≫ w₂.f) ≫ u = (a₂.f ≫ z₂.f) ≫ w₂.s ≫ u

Tactic:
simp only [assoc, fac₄]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((Limits.pair X Y).obj j)

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.left })

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.right })
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
i : X ≅ Y
Z : C
a : A
i' : X ≅ (shiftFunctor C a).obj Z
hZ : P Z
⊢ P.shiftClosure A Y

Tactic:
exact ⟨Z, a, i.symm.trans i', hZ⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((Limits.pair X Y).obj j)

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.left })

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.right })
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
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯ ↔ LeftFractionRel f g

Tactic:
simp only [← Hom.map_mk _ (Q W)]

Goal state after:
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
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
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map L₂ ⋯) = (Localization.uniq L₂ L₁ W).functor.map (φ₂.map L₂ ⋯)

Tactic:
map_compatibility φ₁ L₂ L₁,

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
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.compUniqFunctor L₂ L₁ W).hom.app X ≫ φ₁.map L₁ ⋯ ≫ (Localization.compUniqFunctor L₂ L₁ W).inv.app Y =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map L₂ ⋯)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: 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

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ f.comp (mk₀ m₀ hm₀ g) ⋯ = f ≫ (shiftFunctor C a).map g

Tactic:
by
  subst hm₀
  simp only [comp, shiftFunctorAdd'_zero_add_inv_app, mk₀, shiftFunctorZero',
    eqToIso_refl, Iso.refl_trans, ← Functor.map_comp, assoc, Iso.inv_hom_id_app,
    Functor.id_obj, comp_id]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
⊢ W₂ ≤ W₂'.inverseImage E₂.functor

Tactic:
have eq := W₂.isoClosure.inverseImage_map_eq_of_isEquivalence E₂.functor
        rw [MorphismProperty.map_isoClosure] at eq
        rw [eq]
        apply W₂.le_isoClosure

Goal state after:
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
⊢ ⊥.extensionProductIter 0 = ⊥

Tactic:
rw [extensionProductIter_zero]

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

Goal state before:
pp: case zero
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 : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P.extensionProductIter 0 ≤ Q.isoClosure

Tactic:
rw [extensionProductIter_zero]

Goal state after:
case zero
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 : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P ≤ Q.isoClosure
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
e : HomotopyEquiv K L
n : ι
inst✝¹ : K.HasHomology n
inst✝ : L.HasHomology n
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c n).map e.hom))

Tactic:
exact (e.toHomologyIso n).isIso_hom

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ ((homologyFunctor C (up ℤ) 0).shiftIso n a a' ha').hom.app ((quotient C (up ℤ)).obj K) =
    (homologyFunctor C (up ℤ) a).map ((Functor.commShiftIso (quotient C (up ℤ)) n).inv.app K) ≫
      (homologyFunctorFactors C (up ℤ) a).hom.app ((shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K) ≫
        ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso n a a' ha').hom.app K ≫
          (homologyFunctorFactors C (up ℤ) a').inv.app K

Tactic:
apply Functor.ShiftSequence.induced_shiftIso_hom_app_obj

Goal state after:
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
T₁ T₂ : Triangle P.FullSubcategory
hT₁ : T₁ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
hT₂ : T₂ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a = c ≫ T₂.mor₃

Tactic:
obtain ⟨c, ⟨hc₁, hc₂⟩⟩ := complete_distinguished_triangle_morphism (P.ι.mapTriangle.obj T₁)
      (P.ι.mapTriangle.obj T₂) hT₁ hT₂ (P.ι.map a) (P.ι.map b)
      (by simpa using P.ι.congr_map comm)
    refine ⟨P.fullyFaithfulι.preimage c, ⟨by cat_disch, ?_⟩⟩
    ext
    have := P.ι.commShiftIso_hom_naturality a (1 : ℤ)
    rw [← cancel_mono ((Functor.commShiftIso P.ι (1 : ℤ)).hom.app T₂.obj₁)]
    cat_disch

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

Goal state before:
pp: case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
· obtain rfl := c.next_eq' hij
    exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv

Goal state after:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j 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✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncLE' e).HasHomology j
⊢ QuasiIsoAt (K.truncLE'ToRestriction e) j

Tactic:
dsimp only [truncLE'ToRestriction]
  have : (K.op.restriction e.op).HasHomology j :=
    inferInstanceAs ((K.restriction e).op.HasHomology j)
  rw [quasiIsoAt_unopFunctor_map_iff]
  exact truncGE'.quasiIsoAt_restrictionToTruncGE' K.op e.op j (by simpa)

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
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using 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:
rw [← quasiIso_opFunctor_map_iff]

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 : 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 ((opFunctor C c').map (truncLEMap φ e).op) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y

Tactic:
· intro h
    exact ⟨small_map (homEquiv W W.Q L)⟩

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
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
⊢ (SmallHom.equiv W₂ L₂) (Φ.smallHomMap ((SmallHom.equiv W₁ W₁.Q).symm g)) =
    e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) ((SmallHom.equiv W₁ W₁.Q).symm g)) ≫ e.inv.app Y

Tactic:
simp only [smallHomMap, Equiv.apply_symm_apply]

Goal state after:
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
⊢ (SmallHom.equiv W₂ L₂)
      ((SmallHom.equiv W₂ W₂.Q).symm
        ((((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr
            ((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y))
          ((Φ.localizedFunctor W₁.Q W₂.Q).map g))) =
    e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) ((SmallHom.equiv W₁ W₁.Q).symm g)) ≫ e.inv.app Y
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 G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (OppositeShift.functor A G) x✝¹).hom ≫
            Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift D A) x✝¹)).app
        x✝ ≫
      (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).inv.app x✝ =
    ((shiftFunctor (OppositeShift C A) x✝¹).whiskerLeft (OppositeShift.natTrans A τ) ≫
            (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).hom).app
        x✝ ≫
      (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).inv.app x✝

Tactic:
← cancel_epi (((OppositeShift.functor A G).commShiftIso _).inv.app _)

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
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
F G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝¹ : A
x✝ : OppositeShift C A
⊢ (Functor.commShiftIso (OppositeShift.functor A G) x✝¹).inv.app x✝ ≫
      ((Functor.commShiftIso (OppositeShift.functor A G) x✝¹).hom ≫
              Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift D A) x✝¹)).app
          x✝ ≫
        (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).inv.app x✝ =
    (Functor.commShiftIso (OppositeShift.functor A G) x✝¹).inv.app x✝ ≫
      ((shiftFunctor (OppositeShift C A) x✝¹).whiskerLeft (OppositeShift.natTrans A τ) ≫
              (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).hom).app
          x✝ ≫
        (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).inv.app x✝
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).hom.app X =
    (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
      (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
          (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Tactic:
by
  rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X), Iso.inv_hom_id_app,
    pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc,
    Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
  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ᵒᵖ
⊢ (opShiftFunctorEquivalence C 0).unitIso.hom.app X =
    ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.hom.app X).unop =
    (((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫
        ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op).unop