mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case e_β
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ iR.hom =
    (G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
      whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
        ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
          (𝟭 B).whiskerLeft
              (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                whiskerRight iR.hom (𝟭 T') ≫
                  ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫ (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
            ((𝟭 B).associator (𝟭 B ⋙ R) H).inv

Tactic:
ext

Goal state after:
case e_β
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝¹ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
x✝ : B
⊢ iR.hom.app x✝ =
    ((G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
          whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
            ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
              (𝟭 B).whiskerLeft
                  (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                    whiskerRight iR.hom (𝟭 T') ≫
                      ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫
                        (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
                ((𝟭 B).associator (𝟭 B ⋙ R) H).inv).app
      x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
⊢ (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j

Tactic:
ext

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
x✝ : Opposite.unop (limit K) ⟶ i.left
⊢ (ConcreteCategory.hom ((yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j))).toFun x✝ =
    (ConcreteCategory.hom
          (((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
            (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
              ((coyoneda ⋙
                          (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj
                            (CostructuredArrow.proj yoneda A)).map
                      (limit.π K j)).app
                  i ≫
                ((functorToInterchangeIso A K).inv.app j).app i ≫
                  ((flipFunctorToInterchange A K).hom.app i).app j ≫
                    (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j)).toFun
      x✝
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
⊢ IsIndObject = leftExactFunctor Cᵒᵖ (Type u)

Tactic:
ext

Goal state after:
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
x✝ : Cᵒᵖ ⥤ Type u
⊢ IsIndObject x✝ ↔ leftExactFunctor Cᵒᵖ (Type u) x✝
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst✝¹ : (i : α) → Category.{v_1, u_2} (I i)
inst✝ : HasProductsOfShape α C
F : (i : α) → I i ⥤ C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
⊢ (Pi.map ((NatTrans.pi fun i ↦ (c i).ι).app i) ≫ 𝟙 (∏ᶜ fun i ↦ (c i).pt)) ≫
      (Pi.mapIso fun i ↦ (Cocone.forget (F i)).mapIso (e i)).hom =
    Pi.map ((NatTrans.pi fun i ↦ (c' i).ι).app i) ≫ 𝟙 (∏ᶜ fun i ↦ (c' i).pt)

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst✝¹ : (i : α) → Category.{v_1, u_2} (I i)
inst✝ : HasProductsOfShape α C
F : (i : α) → I i ⥤ C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
b✝ : α
⊢ ((Pi.map ((NatTrans.pi fun i ↦ (c i).ι).app i) ≫ 𝟙 (∏ᶜ fun i ↦ (c i).pt)) ≫
        (Pi.mapIso fun i ↦ (Cocone.forget (F i)).mapIso (e i)).hom) ≫
      Pi.π (fun i ↦ (c' i).pt) b✝ =
    (Pi.map ((NatTrans.pi fun i ↦ (c' i).ι).app i) ≫ 𝟙 (∏ᶜ fun i ↦ (c' i).pt)) ≫ Pi.π (fun i ↦ (c' i).pt) b✝
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst✝¹ : (i : α) → Category.{?u.15, u_4} (I i)
inst✝ : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
X : D
c : (i : α) → Cocone (F i)
j : (i : α) → I i
⊢ ((Pi.map ((NatTrans.pi fun i ↦ (c i).ι).app j)).app X ≫ 𝟙 ((∏ᶜ fun i ↦ (c i).pt).obj X)) ≫
      (piObjIso (fun i ↦ (c i).pt) X).hom =
    (piObjIso ((Functor.pi F).obj j) X).hom ≫
      Pi.map ((NatTrans.pi fun i ↦ (((evaluation D C).obj X).mapCocone (c i)).ι).app j) ≫ 𝟙 (∏ᶜ fun i ↦ (c i).pt.obj X)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst✝¹ : (i : α) → Category.{?u.15, u_4} (I i)
inst✝ : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
X : D
c : (i : α) → Cocone (F i)
j : (i : α) → I i
b✝ : α
⊢ (((Pi.map ((NatTrans.pi fun i ↦ (c i).ι).app j)).app X ≫ 𝟙 ((∏ᶜ fun i ↦ (c i).pt).obj X)) ≫
        (piObjIso (fun i ↦ (c i).pt) X).hom) ≫
      Pi.π (fun i ↦ (c i).pt.obj X) b✝ =
    ((piObjIso ((Functor.pi F).obj j) X).hom ≫
        Pi.map ((NatTrans.pi fun i ↦ (((evaluation D C).obj X).mapCocone (c i)).ι).app j) ≫
          𝟙 (∏ᶜ fun i ↦ (c i).pt.obj X)) ≫
      Pi.π (fun i ↦ (c i).pt.obj X) b✝
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
constructor

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ IsColimit (coconePointwiseProduct c)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_1
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂

Tactic:
ext

Goal state after:
case refine_1
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₁
⊢ (ConcreteCategory.hom
          ((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂)).toFun
      x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_2
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫ ((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₃

Tactic:
ext

Goal state after:
case refine_2
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₁
⊢ (ConcreteCategory.hom
          ((sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫ ((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₃)).toFun
      x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_3
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₂₄

Tactic:
ext

Goal state after:
case refine_3
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₂
⊢ (ConcreteCategory.hom
          ((sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₂₄)).toFun
      x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_4
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₃₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄

Tactic:
ext

Goal state after:
case refine_4
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₃
⊢ (ConcreteCategory.hom
          ((sq₁.map uliftFunctor.{max u v, v}).f₃₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄)).toFun
      x✝
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ J.ι.f 0 ≫ descFZero f I J ≫ I.cocomplex.d 0 1 = 0

Tactic:
simp only [← assoc, descFZero]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ (J.ι.f 0 ≫ factorThru (f ≫ I.ι.f 0) (J.ι.f 0)) ≫ I.cocomplex.d 0 1 = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ (J.ι ≫ desc f I J).f 0 = ((CochainComplex.single₀ C).map f ≫ I.ι).f 0
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) ↔ IsZero (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) → IsZero (Ψ.r.obj (Φ.quotient.obj X))

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsZero (Ψ.r.obj (Φ.quotient.obj X)) → IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.ι'

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ QuasiIso R.ι'
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
this : HasDerivedCategory C
x y : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
this : HasDerivedCategory C
x y : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y)).hom =
    (R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)).hom
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ = R.extMk (g ≫ f) m hm ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ ((Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯).hom = (R.extMk (g ≫ f) m hm ⋯).hom
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
⊢ (R.extMk f m hm hf).comp (Ext.mk₀ g) ⋯ = R'.extMk (f ≫ φ.hom.f n) m hm ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
⊢ ((R.extMk f m hm hf).comp (Ext.mk₀ g) ⋯).hom = (R'.extMk (f ≫ φ.hom.f n) m hm ⋯).hom
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.π'

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
⊢ QuasiIso R.π'
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
this : HasDerivedCategory C
x y : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
this : HasDerivedCategory C
x y : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y)).hom =
    (R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯ = 𝟙 (kernel t)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ (kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0 = 𝟙 (kernel t) ≫ equalizer.ι t 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ = 𝟙 (cokernel b)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    coequalizer.π b 0 ≫ 𝟙 (cokernel b)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ P.isoModSerre.IsMultiplicative

Tactic:
by
  dsimp only [isoModSerre]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Abelian D
P : ObjectProperty C
inst✝ : P.IsSerreClass
⊢ P.isoModSerre.IsStableUnderRetracts

Tactic:
by
  dsimp only [isoModSerre]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.isoModSerre f

Tactic:
constructor

Goal state after:
case left
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.monoModSerre f

case right
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.epiModSerre f