mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left✝ : Epi f
hf : Injective (kernel f)
this : Epi f'
⊢ kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯ ≫
      kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯ =
    𝟙 (kernel f')

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left✝ : Epi f
hf : Injective (kernel f)
this : Epi f'
⊢ (kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯ ≫
        kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯) ≫
      equalizer.ι f' 0 =
    𝟙 (kernel f') ≫ equalizer.ι f' 0
Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ Fibration h.p ∧ WeakEquivalence h.p

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ Fibration h.p

case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ WeakEquivalence h.p
Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ Cofibration h.i ∧ WeakEquivalence h.i

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ Cofibration h.i

case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ WeakEquivalence h.i
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f

Tactic:
by
      have := sq.fac_right =≫ prod.fst
      rw [Category.assoc, Q.p_fst, prod.lift_fst] at this
      simp [this]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
⊢ W = (W.quotient homRel).inverseImage (Quotient.functor homRel)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W f✝ ↔ (W.quotient homRel).inverseImage (Quotient.functor homRel) f✝
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this : Q.i₀ ≫ sq.lift = coprod.inl ≫ coprod.desc (f ≫ P.ι) h.h
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = f

Tactic:
coprod.inl_desc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this : Q.i₀ ≫ sq.lift = f ≫ P.ι
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = 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 ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.fst.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.fst.f i ∧
    ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.snd.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.snd.f i

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.fst.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.fst.f i

case right
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ i : ℤ
hi : i ≠ n₁
⊢ ((π K L n₁).f i ≫ biprod.inr.f i) ≫ biprod.snd.f i = 𝟙 ((mid K L n₁).X i) ≫ biprod.snd.f i
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Bijective fun f ↦ f.postcomp g

Tactic:
constructor

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Injective fun f ↦ f.postcomp g

case right
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Surjective fun f ↦ f.postcomp g
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
this : P.i₀ ≫ sq.lift = coprod.inl ≫ coprod.desc f₀ f₁
⊢ P.i₀ ≫ sq.lift = f₀

Tactic:
coprod.inl_desc

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
this : P.i₀ ≫ sq.lift = f₀
⊢ P.i₀ ≫ sq.lift = f₀
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ Function.Bijective fun g ↦ g.precomp f

Tactic:
constructor

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ Function.Injective fun g ↦ g.precomp f

case right
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ Function.Surjective fun g ↦ g.precomp f
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝² : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝ : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
left✝¹ : Mono i
left✝ : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ Cofibration (ObjectProperty.homMk i)

Tactic:
cofibration_iff,

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝² : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝ : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
left✝¹ : Mono i
left✝ : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ Mono (ObjectProperty.homMk 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
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝ : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝² : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
w✝¹ : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w✝ : QuasiIso p
fac : i ≫ p = f
⊢ Cofibration (ObjectProperty.homMk i)

Tactic:
cofibration_iff,

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝ : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝² : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
w✝¹ : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w✝ : QuasiIso p
fac : i ≫ p = f
⊢ Mono (ObjectProperty.homMk i)
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : Cylinder X.obj
left✝ : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject C ⥤ (weakEquivalences (FibrantObject C)).Localization := (weakEquivalences (FibrantObject C)).Q
⊢ weakEquivalences (FibrantObject C) (homMk P.π)

Tactic:
simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Tactic:
constructor

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α → ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Tactic:
constructor

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α → ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : 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} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α
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₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact

Tactic:
constructor

Goal state after:
case mp
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₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact

case mpr
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₂
α : L ≅ L'
β : R ≅ R'
⊢ w.GuitartExact → (w.whiskerVertical α.hom β.inv).GuitartExact
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
⊢ (w ≫ᵥ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
constructor

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
⊢ (w ≫ᵥ w'.hom).GuitartExact → w.GuitartExact

case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
⊢ w.GuitartExact → (w ≫ᵥ w'.hom).GuitartExact
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

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 : B.op.obj X₃ ⟶ R.op.obj X₂
f f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
⊢ (w.structuredArrowDownwards (Opposite.unop X₂)).map
        (StructuredArrow.homMk (StructuredArrow.Hom.right φ.unop).left.unop ⋯) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f')).left)
          (StructuredArrow.right (Opposite.unop f')).hom.unop (StructuredArrow.hom (Opposite.unop f')).left.unop ⋯) =
    CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left)
        (StructuredArrow.right (Opposite.unop f)).hom.unop (StructuredArrow.hom (Opposite.unop f)).left.unop ⋯)

Tactic:
ext

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 : B.op.obj X₃ ⟶ R.op.obj X₂
f f' : (w.op.StructuredArrowRightwards g)ᵒᵖ
φ : f ⟶ f'
⊢ StructuredArrow.Hom.right
      ((w.structuredArrowDownwards (Opposite.unop X₂)).map
          (StructuredArrow.homMk (StructuredArrow.Hom.right φ.unop).left.unop ⋯) ≫
        CostructuredArrow.hom
          (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f')).left)
            (StructuredArrow.right (Opposite.unop f')).hom.unop (StructuredArrow.hom (Opposite.unop f')).left.unop ⋯)) =
    StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g.unop (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left)
          (StructuredArrow.right (Opposite.unop f)).hom.unop (StructuredArrow.hom (Opposite.unop f)).left.unop ⋯))
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

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 : B.op.obj X₃ ⟶ R.op.obj X₂
f f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ StructuredArrow.hom
        (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
          (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op ⋯) ≫
      (w.op.costructuredArrowRightwards X₂).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left).op ⋯) =
    StructuredArrow.hom
      (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
        (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)

Tactic:
ext

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 : B.op.obj X₃ ⟶ R.op.obj X₂
f f' : w.CostructuredArrowDownwards g.unop
φ : f ⟶ f'
⊢ (StructuredArrow.hom
          (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f').right)
            (StructuredArrow.Hom.right (CostructuredArrow.hom f')).op (CostructuredArrow.left f').hom.op ⋯) ≫
        (w.op.costructuredArrowRightwards X₂).map
          (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left).op ⋯)).left =
    (StructuredArrow.hom
        (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right)
          (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)).left
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

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
⊢ w.op.GuitartExact ↔ w.GuitartExact

Tactic:
constructor

Goal state after:
case mp
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
⊢ w.op.GuitartExact → w.GuitartExact

case mpr
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
⊢ w.GuitartExact → w.op.GuitartExact
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'
⊢ ((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 =
    (CostructuredArrow.mk (StructuredArrow.homMk ((isoOfHom L W₂ R.w ⋯).inv ≫ y) ⋯)).hom

Tactic:
ext

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'
⊢ 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