mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (K.biprodXIso L i).hom ≫ biprod.fst = biprod.fst.f i

Tactic:
simp [biprodXIso]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (K.biprodXIso L i).hom ≫ biprod.snd = biprod.snd.f i

Tactic:
simp [biprodXIso]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'

Tactic:
by
  simp only [ofHom, ofHoms_v_comp_d]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hG : IsZero (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero (F.X j)
⊢ IsZero (X φ i)

Tactic:
by_cases h : c.Rel i (c.next i)
  · have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ h
    refine IsZero.of_iso ?_ (XIsoBiprod φ _ _ h)
    simp only [biprod_isZero_iff]
    exact ⟨hF _ h, hG⟩
  · exact hG.of_iso (XIso φ i h)

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫
      if h : c.Rel (c.next j) (c.next (c.next j)) then
        fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j) +
          sndX φ (c.next j) ≫ α.f (c.next j)
      else sndX φ (c.next j) ≫ α.f (c.next j)

Tactic:
have H := hα.comm (c.next j)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H : (φ ≫ α).f (c.next j) = (dNext (c.next j)) hα.hom + (prevD (c.next j)) hα.hom + Hom.f 0 (c.next j)
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫
      if h : c.Rel (c.next j) (c.next (c.next j)) then
        fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j) +
          sndX φ (c.next j) ≫ α.f (c.next j)
      else sndX φ (c.next j) ≫ α.f (c.next j)
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq = γ₂.v p q hpq

Tactic:
ext_to_iff φ q (q + 1) rfl

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by ext; dsimp; rw [smul_smul]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : Preadditive V
c : ComplexShape ι
inst✝ : HasZeroObject V
⊢ IsZero ((quotient V c).obj 0)

Tactic:
by
    rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
⊢ ∀ (a : P ⟶ Q), a + 0 = a

Tactic:
by rintro ⟨_⟩; exact congr_arg (functor r).map (add_zero _)

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.hom ≫ Quot.out i.inv) = (quotient V c).map (𝟙 C)

Tactic:
rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.inv ≫ Quot.out i.hom) = (quotient V c).map (𝟙 D)

Tactic:
by rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₁

Tactic:
subst h
        dsimp
        rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
          Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₂).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₂

Tactic:
subst h
        dsimp
        rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
          Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm]

Goal state after:
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 : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂

Tactic:
← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃),

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ (T₁.mor₂ ≫ c) ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃ =
    (a ≫ T₂.mor₂) ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃

Tactic:
rw [id_comp, comm]

Goal state after:
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₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
by
  refine (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_
  dsimp
  simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]
  tauto

Goal state after:
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
h : IsZero T.obj₁
⊢ T ∈ distinguishedTriangles ↔ IsIso T.mor₂

Tactic:
by
  rw [rotate_distinguished_triangle,
    distinguished_iff_of_isZero₃ _ (Functor.map_isZero (CategoryTheory.shiftFunctor C 1) h)]
  simp

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

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ δ 0 1 ((snd φ).shift n) +
      (↑(n.negOnePow • (fst φ).shift n)).comp
        (Cochain.ofHom ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)) ⋯ =
    0

Tactic:
by
    ext p q hpq
    dsimp
    simp only [Cochain.δ_shift, δ_snd, Cochain.shift_neg, smul_neg, Cochain.neg_v,
      shiftFunctor_obj_X', Cochain.units_smul_v, Cochain.shift_v', Cochain.comp_zero_cochain_v,
      Cochain.ofHom_v, Cochain.units_smul_comp, shiftFunctor_map_f', neg_add_cancel]

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
p : ℤ
r_f :
  (σ (p + 1 + 1)).r ≫ (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).f =
    𝟙 (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).X₂ -
      (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).g ≫ (σ (p + 1 + 1)).s
s_g : (σ (p + 1)).s ≫ (S.map (eval C (ComplexShape.up ℤ) (p + 1))).g = 𝟙 (S.map (eval C (ComplexShape.up ℤ) (p + 1))).X₃
⊢ (mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯).hom ≫
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₂).d p (p + 1) =
    (mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫
      (mappingConeHomOfDegreewiseSplitXIso S σ (p + 1) (p + 1 + { as := 1 }.as) ⋯).hom

Tactic:
dsimp at r_f s_g ⊢

Goal state after:
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
p : ℤ
r_f : (σ (p + 1 + 1)).r ≫ S.f.f (p + 1 + 1) = 𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ (σ (p + 1 + 1)).s
s_g : (σ (p + 1)).s ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
⊢ (mappingConeHomOfDegreewiseSplitXIso S σ p (p + 1) ⋯).hom ≫ (-1 • S.X₂.d (p + 1) (p + 1 + 1)) =
    (mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫
      (mappingConeHomOfDegreewiseSplitXIso S σ (p + 1) (p + 1 + 1) ⋯).hom
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃

Tactic:
rw [id_comp, comm]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : π.CommShift M
inst✝ : H.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ ((shiftFunctor C (m + n)).associator π (H.shift a)).symm ≪≫
      isoWhiskerRight (commShiftIso π (m + n)) (H.shift a) ≪≫
        π.associator (shiftFunctor D (m + n)) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso (m + n) a a'' ⋯) =
    isoWhiskerRight (shiftFunctorAdd C m n) (π ⋙ H.shift a) ≪≫
      (shiftFunctor C m).associator (shiftFunctor C n) (π ⋙ H.shift a) ≪≫
        (shiftFunctor C m).isoWhiskerLeft
            (((shiftFunctor C n).associator π (H.shift a)).symm ≪≫
              isoWhiskerRight (commShiftIso π n) (H.shift a) ≪≫
                π.associator (shiftFunctor D n) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso n a a' ha')) ≪≫
          ((shiftFunctor C m).associator π (H.shift a')).symm ≪≫
            isoWhiskerRight (commShiftIso π m) (H.shift a') ≪≫
              π.associator (shiftFunctor D m) (H.shift a') ≪≫ π.isoWhiskerLeft (H.shiftIso m a' a'' ha'')

Tactic:
ext K
    dsimp
    simp only [H.shiftIso_add_hom_app n m a a' a'' ha' ha'', assoc,
      commShiftIso_add, CommShift.isoAdd_hom_app, ← Functor.map_comp_assoc,
      id_comp, Iso.inv_hom_id_app, comp_obj, comp_id]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
h : LeftFractionRel φ.fst ψ.fst
h' : LeftFractionRel φ.snd ψ.snd
⊢ LeftFraction₂Rel φ ψ

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h

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
h' : LeftFractionRel φ.snd ψ.snd
Z : C
t₁ : φ.fst.Y' ⟶ Z
t₂ : ψ.fst.Y' ⟶ Z
hst : φ.fst.s ≫ t₁ = ψ.fst.s ≫ t₂
hft : φ.fst.f ≫ t₁ = ψ.fst.f ≫ t₂
ht : W (φ.fst.s ≫ t₁)
⊢ LeftFraction₂Rel φ ψ
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ LeftFractionRel z₂ z₁

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₂ z₁
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
inst✝¹ : Category.{v₄, u₄} D₁
inst✝ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
F : C₁ ⥤ C₂
hW : W₁ = W₂.inverseImage F
⊢ W₁ ≤ W₂.inverseImage F

Tactic:
hW

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
inst✝¹ : Category.{v₄, u₄} D₁
inst✝ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
F : C₁ ⥤ C₂
hW : W₁ = W₂.inverseImage F
⊢ W₂.inverseImage F ≤ W₂.inverseImage F
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
i : ULift.{max v w, u} ι
⊢ HasCardinalLT (ULift.{max u w, v} (α i.down)) (Cardinal.lift.{max u v, w} κ)

Tactic:
simpa using hα (ULift.down i)

Goal state after:
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
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ Qinv s hs ≫ (Q W).map s = 𝟙 ((Q W).obj Y)

Tactic:
by
    dsimp only [Qinv, Q_map]
    rw [homMk_comp_homMk (ofInv s hs) (ofHom W s) (ofHom W (𝟙 Y)) (by simp)]
    apply homMk_eq_of_leftFractionRel
    exact ⟨_, 𝟙 Y, 𝟙 Y, by simp, by simp, by simpa using W.id_mem Y⟩

Goal state after:
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
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ a₁.map F hF = a₂.map F hF

Tactic:
← cancel_mono (F.map (a₁.s ≫ t₁)),

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
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ a₁.map F hF ≫ F.map (a₁.s ≫ t₁) = a₂.map F hF ≫ F.map (a₁.s ≫ t₁)
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 ℤ
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₂
α : 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'
fac : L.map (T₁.mor₁ ≫ γ.f) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)

Tactic:
fac,

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
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₂
α : 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'
fac : L.map (T₁.mor₁ ≫ γ.f) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
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.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
h : LeftFractionRel (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h

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
Z : C
t₁ : (LeftFraction.ofHom W f₁).Y' ⟶ Z
t₂ : (LeftFraction.ofHom W f₂).Y' ⟶ Z
hst : (LeftFraction.ofHom W f₁).s ≫ t₁ = (LeftFraction.ofHom W f₂).s ≫ t₂
hft : (LeftFraction.ofHom W f₁).f ≫ t₁ = (LeftFraction.ofHom W f₂).f ≫ t₂
ht : W ((LeftFraction.ofHom W f₁).s ≫ t₁)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s
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.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (L.map φ.f).op ≫ (inv (L.map φ.s)).op = (L.map φ.f).op ≫ inv (L.map φ.s).op

Tactic:
rw [op_inv]

Goal state after:
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
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (inv (L.map φ.s)).op ≫ (L.map φ.f).op = inv (L.map φ.s).op ≫ (L.map φ.f).op

Tactic:
rw [op_inv]

Goal state after: