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

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✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso F).hom = (S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ)

Tactic:
by
  dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso,
    LeftHomologyData.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl]
  simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.Exact → S₂.Exact

Tactic:
rintro ⟨h₁, z₁⟩

Goal state after:
case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₁ : S₁.HomologyData
z₁ : IsZero h₁.left.H
⊢ S₂.Exact
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
this : IsIso (η.app (i.obj ((reflector i).obj A)))
⊢ Epi (retraction (η.app A) ≫ η.app A)

Tactic:
rw [show retraction _ ≫ η.app A = _ from η.naturality (retraction (η.app A))]

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
this : IsIso (η.app (i.obj ((reflector i).obj A)))
⊢ Epi (η.app ((reflector i ⋙ i).obj A) ≫ (reflector i ⋙ i).map (retraction (η.app A)))
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Mono S.g ↔ S.f = 0

Tactic:
constructor
  · intro
    rw [← cancel_mono S.g, zero, zero_comp]
  · exact hS.mono_g

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ Mono (ofMkLE f X h)

Tactic:
dsimp only [ofMkLE]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ f ≫ i₂ = i₁

Tactic:
fac

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ i₁ = i₁
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ ((pullback X✝.arrow ⋙ map X✝.arrow).obj g).obj.left ⟶ ((pullback Y✝.arrow ⋙ map Y✝.arrow).obj g).obj.left

Tactic:
apply pullback.lift (pullback.fst _ _) (pullback.snd _ _ ≫ k.hom.left) _
          rw [pullback.condition, assoc, w k]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂

Tactic:
apply le_antisymm
  · refine le_inf _ _ _ (Limits.prod.fst.le) (Limits.prod.snd.le)
  · apply leOfHom
    exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact

Tactic:
intro S

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
⊢ S.Exact → (S.map L).Exact
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
⊢ ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact

Tactic:
intro S

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
⊢ S.Exact → (S.map L).Exact
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ∀ (X : C), IsIso ((coimageImageComparison α).app X)

Tactic:
intros

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X X✝ : C
⊢ IsIso ((coimageImageComparison α).app X✝)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
⊢ ∀ (S : Subobject X), S = mk (𝟙 X)

Tactic:
intro S

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
S : Subobject X
⊢ S = mk (𝟙 X)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
⊢ ∀ (j : Finset (Discrete α)),
    (colimit.cocone (liftToFinsetObj (Discrete.functor f))).ι.app j ≫
        ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
            (colimit.isColimit (Discrete.functor f))).hom =
      (finiteSubcoproductsCocone f).ι.app j

Tactic:
intro S

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
⊢ (colimit.cocone (liftToFinsetObj (Discrete.functor f))).ι.app S ≫
      ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
          (colimit.isColimit (Discrete.functor f))).hom =
    (finiteSubcoproductsCocone f).ι.app S
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
⊢ ∀ (j : (Finset (Discrete α))ᵒᵖ),
    (limit.cone (liftToFinsetObj (Discrete.functor f))).π.app j =
      ((liftToFinsetLimitCone (Discrete.functor f)).isLimit.conePointUniqueUpToIso
            (limit.isLimit (Discrete.functor f))).hom ≫
        (finiteSubproductsCone f).π.app j

Tactic:
intro S

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
⊢ (limit.cone (liftToFinsetObj (Discrete.functor f))).π.app S =
    ((liftToFinsetLimitCone (Discrete.functor f)).isLimit.conePointUniqueUpToIso
          (limit.isLimit (Discrete.functor f))).hom ≫
      (finiteSubproductsCone f).π.app S
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
⊢ L.lanUnit.app F₁ ≫ L.whiskerLeft (((L.lan.obj F₁).homEquivOfIsLeftKanExtension (L.lanUnit.app F₁) G).symm (f ≫ α)) =
    L.lanUnit.app F₁ ≫
      L.whiskerLeft (L.lan.map f ≫ ((L.lan.obj F₂).homEquivOfIsLeftKanExtension (L.lanUnit.app F₂) G).symm α)

Tactic:
ext X
          dsimp [homEquivOfIsLeftKanExtension]
          rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
          have h := congr_app (L.lanUnit.naturality f) X
          dsimp at h ⊢
          rw [← h, assoc, descOfIsLeftKanExtension_fac_app]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (yonedaCollectionPresheaf A F).map f ≫ ↾YonedaCollection.map₁ η =
      ↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).map f

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (yonedaCollectionPresheaf A F).map f✝ ≫ ↾YonedaCollection.map₁ η =
    ↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).map f✝
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
⊢ IsColimit ((prod.functor.obj F).mapCocone c)

Tactic:
apply evaluationJointlyReflectsColimits _ fun {k} => ?_
            change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)
            let :=
              isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
            apply IsColimit.mapCoconeEquiv _ this
            apply (NatIso.ofComponents _ _).symm
            · intro G
              apply asIso (prodComparison ((evaluation C D).obj k) F G)
            · intro G G'
              apply prodComparison_natural ((evaluation C D).obj k) (𝟙 F)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
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_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
hb_fac_app :
  (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (hb.desc u)).app (L.obj x) =
    (StructuredArrow.hom u).app (L.obj x)
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u)).app x =
    (StructuredArrow.hom y).app x

Tactic:
have hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
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_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
hb_fac_app :
  (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (hb.desc u)).app (L.obj x) =
    (StructuredArrow.hom u).app (L.obj x)
hα_fac_app :
  (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (hα.desc
              (mk (L' ⋙ StructuredArrow.right y)
                (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))).app
      x =
    (StructuredArrow.hom
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
      x
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u)).app x =
    (StructuredArrow.hom y).app x
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
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_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
⊢ F₁.IsLeftKanExtension α.hom

Tactic:
refine ⟨⟨?_⟩⟩

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
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_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₁ α.hom)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
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_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
⊢ F₁.IsRightKanExtension α.hom

Tactic:
refine ⟨⟨?_⟩⟩

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
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_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
⊢ CostructuredArrow.IsUniversal (RightExtension.mk F₁ α.hom)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
⊢ IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L →
    L.IsLeftKanExtension α

Tactic:
rintro ⟨_, _⟩

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ L.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : ((i ≫ h) ≫ e) ≫ i = i
⊢ a = default

Tactic:
cancel_mono_id i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
⊢ a = default
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A : StructuredArrow S T
P : { P // ∃ q, q ≫ T.map P.arrow = A.hom }
⊢ ↑((fun P ↦ ⟨projectSubobject P, ⋯⟩) ((fun P ↦ liftSubobject ↑P ⋯) P)) = ↑P

Tactic:
by simp only [liftSubobject, homMk_right, projectSubobject_mk,
      Subobject.mk_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
⊢ ∃ x, x ≫ f = g

Tactic:
exact hf A hA g

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
⊢ ∃ x, f ≫ x = g

Tactic:
exact hf A hA g

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPullbacks C
inst✝¹ : Mono f
H : C ⥤ D
inst✝ : H.PreservesMonomorphisms
⊢ ∀ (X : K), Mono ((whiskerRight f H).app X)

Tactic:
intros

Goal state after:
K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPullbacks C
inst✝¹ : Mono f
H : C ⥤ D
inst✝ : H.PreservesMonomorphisms
X✝ : K
⊢ Mono ((whiskerRight f H).app X✝)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
⊢ ∀ (X : K), Epi ((whiskerRight f H).app X)

Tactic:
intros

Goal state after:
K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
X✝ : K
⊢ Epi ((whiskerRight f H).app X✝)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : AddCommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget AddCommGrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
intros

Goal state after:
X'✝ X✝ : Type u
Y✝ : AddCommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGrpCat).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
⊢ ∀ {Z : AddCommGrpCat} (g h : Z ⟶ free.obj X), g ≫ free.map f = h ≫ free.map f → g = h

Tactic:
intros

Goal state after:
case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
Z✝ : AddCommGrpCat
g✝ h✝ : Z✝ ⟶ free.obj X
a✝ : g✝ ≫ free.map f = h✝ ≫ free.map f
⊢ g✝ = h✝
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
⊢ Function.Bijective (fromSigma F c)

Tactic:
by
  rwa [← isColimit_iff_bijective_fromSigma]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : GrpCat} (f : X' ⟶ X) (g : X ⟶ (forget GrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
intros

Goal state after:
X'✝ X✝ : Type u
Y✝ : GrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GrpCat).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : GrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GrpCat).obj Y✝
⊢ ∀ (a : X'✝),
    (Hom.hom ((ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝)))
        (FreeGroup.of a) =
      (Hom.hom
          (free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝))
        (FreeGroup.of a)

Tactic:
intros

Goal state after:
X'✝ X✝ : Type u
Y✝ : GrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GrpCat).obj Y✝
a✝ : X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (FreeGroup.of a✝) =
    (Hom.hom
        (free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝))
      (FreeGroup.of a✝)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X : Type u
h : IsInitial X
⊢ IsEmpty X

Tactic:
exact Function.isEmpty (IsInitial.to h PEmpty)

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ (X : GrpCat),
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (𝟙 X)))) =
      𝟙 (CommGrpCat.of (Abelianization ↑X))

Tactic:
intros

Goal state after:
X✝ : GrpCat
⊢ CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (𝟙 X✝)))) =
    𝟙 (CommGrpCat.of (Abelianization ↑X✝))
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X Y Z : GrpCat} (f : X ⟶ Y) (g : Y ⟶ Z),
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (f ≫ g)))) =
      CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f))) ≫
        CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g)))

Tactic:
intros

Goal state after:
X✝ Y✝ Z✝ : GrpCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (f✝ ≫ g✝)))) =
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f✝))) ≫
      CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g✝)))