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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i : ι
⊢ a • ((dNext i) h.hom + (prevD i) h.hom + g.f i) =
    (C.dFrom i ≫ (fromNext i) fun i j ↦ a • h.hom i j) + ((toPrev i) fun i j ↦ a • h.hom i j) ≫ D.dTo i + a • g.f i

Tactic:
dsimp [fromNext, toPrev]

Goal state after:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i : ι
⊢ a • (C.dFrom i ≫ h.hom (c.next i) i + h.hom i (c.prev i) ≫ D.dTo i + g.f i) =
    C.dFrom i ≫ (a • h.hom (c.next i) i) + (a • h.hom i (c.prev i)) ≫ D.dTo i + a • g.f i
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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (XIso φ i hi).inv]
  simpa only [inrX, dif_neg hi] using h

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0
i : ι
⊢ (nullHomotopicMap hom).f i = (dNext i) hom + (prevD i) hom + Hom.f 0 i

Tactic:
HomologicalComplex.zero_f_apply,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0
i : ι
⊢ (nullHomotopicMap hom).f i = (dNext i) hom + (prevD i) hom + 0
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 : ℤ
α β : Cochain F G n
⊢ δ n m (α + β) = δ n m α + δ n m β

Tactic:
by
    by_cases h : n + 1 = m
    · ext p q hpq
      dsimp
      simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.add_v, add_comp, comp_add, smul_add]
      abel
    · simp only [δ_shape _ _ h, add_zero]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ (dNext (i + 1)) f = P.d (i + 1) i ≫ f i (i + 1)

Tactic:
dsimp [dNext]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) =
    P.d (i + 1) i ≫ f i (i + 1)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ (dNext 0) f = 0

Tactic:
dsimp [dNext]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ P.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
⊢ f = g ↔ (inl φ).v i j ⋯ ≫ f = (inl φ).v i j ⋯ ≫ g ∧ (inr φ).f j ≫ f = (inr φ).f j ≫ g

Tactic:
constructor
  · rintro rfl
    tauto
  · rintro ⟨h₁, h₂⟩
    exact ext_from φ i j hij h₁ h₂

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ (inl φ).comp (descCochain φ α β h) ⋯ = α

Tactic:
simp [descCochain]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ (Cochain.ofHom (inr φ)).comp (descCochain φ α β h) ⋯ = β

Tactic:
simp [descCochain]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (dNext j) f = P.d j (j + 1) ≫ f (j + 1) j

Tactic:
dsimp [dNext]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ P.d j ((ComplexShape.up ℕ).next j) ≫ f ((ComplexShape.up ℕ).next j) j = P.d j (j + 1) ≫ f (j + 1) j
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case mk.mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
L : C ⥤ D
as✝¹ as✝ : C
a₁✝ : { as := as✝¹ } ⟶ { as := as✝ }
a✝¹ : { as := as✝¹ }.as ⟶ { as := as✝ }.as
a₂✝ : { as := as✝¹ } ⟶ { as := as✝ }
a✝ : { as := as✝¹ }.as ⟶ { as := as✝ }.as
h :
  (Quotient.lift L.homRel L ⋯).map (Quot.mk (HomRel.CompClosure L.homRel) a✝¹) =
    (Quotient.lift L.homRel L ⋯).map (Quot.mk (HomRel.CompClosure L.homRel) a✝)
⊢ Quot.mk (HomRel.CompClosure L.homRel) a✝¹ = Quot.mk (HomRel.CompClosure L.homRel) a✝

Tactic:
exact Quotient.sound _ h

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
⊢ n.negOnePow • K.d (i + n) (j + n) = 0

Tactic:
rw [K.shape, smul_zero]
        intro hij'
        apply hij
        dsimp at hij' ⊢
        lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f p ≫
      ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p =
    (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_hom_app_f']

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case refine_2
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
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
x₁ : A ⟶ T.obj₁
hx₁ : x₁ ≫ φ.hom₁ = y₁
⊢ ∃ a, (fun x ↦ x ≫ φ.hom₂) a = y₂

Tactic:
refine ⟨x₂ + x₁ ≫ T.mor₁, ?_⟩

Goal state after:
case refine_2
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
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
x₁ : A ⟶ T.obj₁
hx₁ : x₁ ≫ φ.hom₁ = y₁
⊢ (fun x ↦ x ≫ φ.hom₂) (x₂ + x₁ ≫ T.mor₁) = y₂
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g'.cons p) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (g'.cons p)

Tactic:
have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons

Goal state after:
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g'.cons p) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (g'.cons p)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Tactic:
by
  obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ f₂
  obtain ⟨β, hβ⟩ := exists_leftFraction L W g
  obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.f).exists_leftFraction
  dsimp at hγ
  rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W (f₁ ≫ g) (f₂ ≫ g)
    (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s)
    (W.comp_mem _ _ β.hs γ.hs))]; rotate_left
  · rw [h₁, hβ]
    exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _
  · rw [h₂, hβ]
    exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _
  rw [hβ, LeftFraction.map_comp_map_eq_map _ _ γ hγ]
  dsimp [LeftFraction₂.add]
  rw [add_comp]

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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f' ≫ L.map (β.s ≫ γ.s) = L.map ψ.snd.f

Tactic:
hα',

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ α.snd.map L ⋯ ≫ L.map (β.s ≫ γ.s) = L.map ψ.snd.f
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst.map L ⋯) = F.map (φ.snd.map L ⋯)
⊢ φ.fst.map L ⋯ ≫ L.map φ.s = φ.snd.map L ⋯ ≫ L.map φ.s

Tactic:
φ.fst.map_comp_map_s 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
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst.map L ⋯) = F.map (φ.snd.map L ⋯)
⊢ L.map φ.fst.f = φ.snd.map L ⋯ ≫ L.map φ.s
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ F.map (L.map (f - g)) = 0

Tactic:
L.map_sub,

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
inst✝⁷ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ F.map (L.map f - L.map g) = 0
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
⊢ W (((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))).s ≫ 𝟙 Y)

Tactic:
by simpa using W.id_mem Y

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 ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
obtain ⟨Z₂, σ, hσ, fac⟩ := (MorphismProperty.map_eq_iff_postcomp L W
    (α.f ≫ β.f ≫ γ.s) (T₁.mor₁ ≫ γ.f)).1 (by
      rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac
      rw [fac, ← Functor.map_comp_assoc, hβ, Functor.map_comp, Functor.map_comp,
        Functor.map_comp, assoc, MorphismProperty.LeftFraction.map_comp_map_s_assoc])

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₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : (α.f ≫ β.f ≫ γ.s) ≫ σ = (T₁.mor₁ ≫ γ.f) ≫ σ
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
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₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
hT₃ : Triangle.mk (β.f ≫ γ.s ≫ σ) g h ∈ distinguishedTriangles
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
let T₃ := Triangle.mk (β.f ≫ γ.s ≫ σ) g h

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₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
hT₃ : Triangle.mk (β.f ≫ γ.s ≫ σ) g h ∈ distinguishedTriangles
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

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
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
a : M
⊢ induced.shiftIso L G M F' e' 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor

Tactic:
by
    ext1
    apply ((whiskeringLeft C D A).obj L).map_injective
    ext K
    dsimp
    simp only [induced.shiftIso_hom_app_obj, shiftIso_zero_hom_app, id_obj,
      NatTrans.naturality, comp_map, Iso.hom_inv_id_app_assoc,
      comp_id, ← Functor.map_comp, L.commShiftIso_zero, CommShift.isoZero_inv_app, assoc,
      Iso.inv_hom_id_app, Functor.map_id]

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
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 Q R : ObjectProperty C
inst✝ : P.Nonempty
⊢ (P.extensionProductIter 0).Nonempty

Tactic:
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
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 Q R : ObjectProperty C
inst✝ : P.Nonempty
⊢ P.Nonempty
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 M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Tactic:
← quasiIso_iff_comp_left φ φ'

Goal state after:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')
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:
extensionProductIter_zero

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