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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝² : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝¹ : ∀ (n : ℤ), Injective ((kernel p).X n)
this✝ : (kernel p).IsKInjective
h✝ : QuasiIso i
this : { X₁ := A, X₂ := B, X₃ := cokernel i, f := i, g := cokernel.π i, zero := ⋯ }.ShortExact
⊢ QuasiIso { X₁ := A, X₂ := B, X₃ := cokernel i, f := i, g := cokernel.π i, zero := ⋯ }.f

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝² : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝¹ : ∀ (n : ℤ), Injective ((kernel p).X n)
this✝ : (kernel p).IsKInjective
h✝ : QuasiIso i
this : { X₁ := A, X₂ := B, X₃ := cokernel i, f := i, g := cokernel.π i, zero := ⋯ }.ShortExact
⊢ QuasiIso i
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝³ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝² : ∀ (n : ℤ), Injective ((kernel p).X n)
this✝¹ : (kernel p).IsKInjective
h✝ : QuasiIso p
this✝ : Epi p
this : { X₁ := kernel p, X₂ := X, X₃ := Y, f := kernel.ι p, g := p, zero := ⋯ }.ShortExact
⊢ QuasiIso { X₁ := kernel p, X₂ := X, X₃ := Y, f := kernel.ι p, g := p, zero := ⋯ }.g

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝³ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝² : ∀ (n : ℤ), Injective ((kernel p).X n)
this✝¹ : (kernel p).IsKInjective
h✝ : QuasiIso p
this✝ : Epi p
this : { X₁ := kernel p, X₂ := X, X₃ := Y, f := kernel.ι p, g := p, zero := ⋯ }.ShortExact
⊢ QuasiIso p
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ WeakEquivalence (toHoCat.map { hom := HoCat.iResolutionObj X.obj })
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ 𝟙 T.X₂ ≫ (homologyShortComplex f n).g = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ 𝟙 T.X₂ ≫ homologyMap (α f n) n = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ IsFibrant ((localizerMorphism C).functor.obj X)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ IsFibrant X.obj
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
f : StructuredArrow X₂ T
⊢ (((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).obj f).hom ≫ B.map (α.symm.app f.right).hom =
    ((w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor).obj f).hom

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
f : StructuredArrow X₂ T
⊢ (R'.map f.hom ≫ β.inv.app (T.obj f.right) ≫ w.natTrans.app f.right ≫ B.map (α.hom.app f.right)) ≫
      B.map (α.inv.app f.right) =
    β.inv.app X₂ ≫ R.map f.hom ≫ w.app f.right
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this : Mono (homologyMap (π f n) n)
⊢ Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this : Mono (homologyMap (π f n) n)
⊢ Mono (homologyMap (mappingCocone.fst (α f n)) n)
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
a : X₂ ⟶ T.obj X₁
b : L.obj X₁ ⟶ X₃
comm : R.map a ≫ w.app X₁ ≫ B.map b = g
⊢ ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom

Tactic:
by simpa using comm

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
inst✝ : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right✝ : Mono (homologyMap F₁.obj.ι n₁)
F₂ : (cofFib F₁.obj.ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
⊢ Mono { mid := F₂.obj.mid, ι := F₂.obj.ι, π := F₂.obj.π ≫ F₁.obj.π, ι_π := ⋯ }.ι

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
inst✝ : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right✝ : Mono (homologyMap F₁.obj.ι n₁)
F₂ : (cofFib F₁.obj.ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
⊢ Mono F₂.obj.ι
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)).left.hom ≫
      T.map (StructuredArrow.Hom.right φ).left =
    (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)).left.hom

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (StructuredArrow.hom f₁).left ≫ T.map (StructuredArrow.Hom.right φ).left = (StructuredArrow.hom f₂).left
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ StructuredArrow.Hom.right
      (((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).structuredArrowDownwards
              X₂).map
          (StructuredArrow.homMk φ.f ⋯) ≫
        (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ R'.w ⋯).inv ≫ y) ⋯)).hom) =
    StructuredArrow.Hom.right (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ R.w ⋯).inv ≫ y) ⋯)).hom

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ L.map (Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = (isoOfHom L W₂ R.w ⋯).inv ≫ y
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫
      (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)).right.hom =
    (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)).right.hom

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right (CostructuredArrow.hom f₁)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
inst✝ : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right✝ : Mono (homologyMap F₁.obj.ι n₁)
F₂ : (cofFib F₁.obj.ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
this✝ : IsIso (F₁.obj.π.f i)
this : IsIso (F₂.obj.π.f i)
⊢ IsIso ({ obj := { mid := F₂.obj.mid, ι := F₂.obj.ι, π := F₂.obj.π ≫ F₁.obj.π, ι_π := ⋯ }, property := ⋯ }.obj.π.f i)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
inst✝ : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right✝ : Mono (homologyMap F₁.obj.ι n₁)
F₂ : (cofFib F₁.obj.ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
this✝ : IsIso (F₁.obj.π.f i)
this : IsIso (F₂.obj.π.f i)
⊢ IsIso (F₂.obj.π.f i ≫ F₁.obj.π.f i)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + ↑0
⊢ QuasiIsoAt { obj := { mid := L, ι := f, π := 𝟙 L, ι_π := ⋯ }, property := ⋯ }.obj.ι i

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + ↑0
⊢ QuasiIsoAt f i
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ (CostructuredArrow.left
          (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
            (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯)).hom ≫
      T.map (StructuredArrow.Hom.right φ.left) =
    (CostructuredArrow.left
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯)).hom

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ (γ ≫ (CostructuredArrow.left A).hom) ≫ T.map (StructuredArrow.Hom.right φ.left) = γ ≫ (CostructuredArrow.left A').hom
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ StructuredArrow.Hom.right
      ((w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) ≫
        CostructuredArrow.hom
          (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
            (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯)) =
    StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯))

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A') =
    StructuredArrow.Hom.right (CostructuredArrow.hom A)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
F₁₂ : (cofFib F.obj.obj.ι).FullSubcategory
h₁ : quasiIsoLE n₁ F₁₂
h₂ : isIsoLE n₀ F₁₂
⊢ Mono { mid := F₁₂.obj.mid, ι := F₁₂.obj.ι, π := F₁₂.obj.π ≫ F.obj.obj.π, ι_π := ⋯ }.ι

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
F₁₂ : (cofFib F.obj.obj.ι).FullSubcategory
h₁ : quasiIsoLE n₁ F₁₂
h₂ : isIsoLE n₀ F₁₂
⊢ Mono F₁₂.obj.ι
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
⊢ (midπ f n₀ q₂).f i ≫ ((functor f n₀).map (homOfLE hq).op).hom.h.f i =
    (midπ f n₀ q₂ ≫ ((functor f n₀).map (homOfLE hq).op).hom.h).f i

Tactic:
dsimp

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q : ℕ
i : ℤ
⊢ (ι f n₀).f i ≫ (midπ f n₀ q).f i = (ι f n₀ ≫ midπ f n₀ q).f i

Tactic:
dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (Iso.refl ((id W₁).functor ⋙ W₁.Q)).hom

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (𝟙 (𝟭 C₁ ⋙ W₁.Q))
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q : ℕ
i : ℤ
⊢ (midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i = (midπ f n₀ q ≫ ((functor f n₀).obj (op q)).obj.π).f i

Tactic:
dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (Iso.refl ((id W₁).functor ⋙ W₁.Q)).inv

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ TwoSquare.GuitartExact (𝟙 (𝟭 C₁ ⋙ W₁.Q))
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
W : MorphismProperty C
L : C ⥤ D
L' : C ⥤ D'
inst✝¹ : L.IsLocalization W
inst✝ : L'.IsLocalization W
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ (fun f ↦ StructuredArrow.mk ((homEquiv W L' L) f.hom))
      ((fun f ↦ StructuredArrow.mk ((homEquiv W L L') f.hom)) (StructuredArrow.mk f)) =
    StructuredArrow.mk f

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
W : MorphismProperty C
L : C ⥤ D
L' : C ⥤ D'
inst✝¹ : L.IsLocalization W
inst✝ : L'.IsLocalization W
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ StructuredArrow.mk ((homEquiv W L' L) ((homEquiv W L L') f)) = StructuredArrow.mk f