mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).inv =
    (ρ_ ((F.comp G.toPrelaxFunctor).map f)).inv ≫
      (F.comp G.toPrelaxFunctor).map f ◁ (G.mapId (F.obj b✝) ≫ G.map₂ (F.mapId b✝)) ≫
        G.mapComp (F.map f) (F.map (𝟙 b✝)) ≫ G.map₂ (F.mapComp f (𝟙 b✝))

Tactic:
dsimp
    simp only [map₂_rightUnitor, PrelaxFunctor.map₂_comp, assoc, mapComp_naturality_right_assoc,
      Bicategory.whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = (asIso (F.mapComp f✝ h)).hom ≫ F.map₂ η ▷ F.map h ≫ (asIso (F.mapComp g✝ h)).inv

Tactic:
dsimp
    rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_left]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_1
X Y : Type u
⊢ (binaryProductFunctor.obj X).obj Y ≅ (prod.functor.obj X).obj Y

Tactic:
exact ((limit.isLimit _).conePointUniqueUpToIso (binaryProductLimit X Y)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : F.Elements
h₁ : x.fst = y.fst
h₂ : (ConcreteCategory.hom (F.map (eqToHom h₁))) x.snd = y.snd
⊢ x = y

Tactic:
cases x

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
y : F.Elements
fst✝ : C
snd✝ : F.obj fst✝
h₁ : ⟨fst✝, snd✝⟩.fst = y.fst
h₂ : (ConcreteCategory.hom (F.map (eqToHom h₁))) ⟨fst✝, snd✝⟩.snd = y.snd
⊢ ⟨fst✝, snd✝⟩ = y
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
1

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
⊢ ∀ (X : Grothendieck (G ⋙ typeToCat)),
    (grothendieckTypeToCatFunctor G).map
          ((NatIso.ofComponents
                  (fun X ↦
                    casesOn X fun base fiber ↦
                      Discrete.casesOn fiber fun as ↦
                        Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
                  ⋯).hom.app
            X) ≫
        (NatIso.ofComponents
                (fun X ↦
                  Sigma.casesOn (motive := fun t ↦
                    X = t →
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ (𝟭 G.Elements).obj X))
                    X
                    (fun fst snd h ↦
                      ⋯ ▸ Iso.refl ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst, snd⟩))
                    ⋯)
                ⋯).hom.app
          ((grothendieckTypeToCatFunctor G).obj X) =
      𝟙 ((grothendieckTypeToCatFunctor G).obj X)

Tactic:
by
    rintro ⟨_, ⟨⟩⟩
    simp
    rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WidePullbackShape J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        x) =
    x

Tactic:
cases x

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        none) =
    none

case some
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
val✝ : J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        (some val✝)) =
    some val✝
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WithTerminal (Discrete J)
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        x) =
    x

Tactic:
cases x

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
a✝ : Discrete J
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        (of a✝)) =
    of a✝

case star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        star) =
    star
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ IsColimit c → IsLimit c.op

Tactic:
intro h

Goal state after:
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
h : IsColimit c
⊢ IsLimit c.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ IsLimit c.op → IsColimit c

Tactic:
intro h

Goal state after:
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
h : IsLimit c.op
⊢ IsColimit c
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ IsColimit c → IsLimit c.unop

Tactic:
intro h

Goal state after:
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
h : IsColimit c
⊢ IsLimit c.unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ IsLimit c.unop → IsColimit c

Tactic:
intro h

Goal state after:
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
h : IsLimit c.unop
⊢ IsColimit c
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c : Comma (Functor.const C) (𝟭 (C ⥤ D))
x y : C
f : x ⟶ y
⊢ c.hom.app x ≫ c.right.map f = c.hom.app y

Tactic:
by simpa using (c.hom.naturality f).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithTerminal C)ᵒᵖ
x : WithTerminal C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (down f).op
      | op star, op (of a), x, x_1 =>
        WithInitial.starInitial.to
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithInitial.of (op x)
        | star => WithInitial.star)

Tactic:
cases x

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithTerminal C)ᵒᵖ
a✝ : C
⊢ (match 𝟙 (op (of a✝)) with
    | op f =>
      match op (of a✝), op (of a✝), f, 𝟙 (op (of a✝)) with
      | op (of x), op (of y), f, x_1 => (down f).op
      | op star, op (of a), x, x_1 =>
        WithInitial.starInitial.to
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)) =
    𝟙
      (match op (of a✝) with
      | op x =>
        match x with
        | of x => WithInitial.of (op x)
        | star => WithInitial.star)

case star
C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithTerminal C)ᵒᵖ
⊢ (match 𝟙 (op star) with
    | op f =>
      match op star, op star, f, 𝟙 (op star) with
      | op (of x), op (of y), f, x_1 => (down f).op
      | op star, op (of a), x, x_1 =>
        WithInitial.starInitial.to
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)) =
    𝟙
      (match op star with
      | op x =>
        match x with
        | of x => WithInitial.of (op x)
        | star => WithInitial.star)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : HasLimitsOfShape D E
inst✝ : HasLimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ lim.map f ≫ (limitIso F Y✝).symm.hom = (limitIso F X✝).symm.hom ≫ ((whiskeringLeft C D E).obj F ⋙ lim).map f

Tactic:
by
    simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map,
      Iso.symm_hom, limitIso_inv]
    ext
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithInitial Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match x with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

Tactic:
cases x

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match WithInitial.of a✝, WithInitial.of a✝, 𝟙 (WithInitial.of a✝) with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match WithInitial.of a✝ with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match WithInitial.star, WithInitial.star, 𝟙 WithInitial.star with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match WithInitial.star with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
x : WithInitial C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

Tactic:
cases x

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
a✝ : C
⊢ (match 𝟙 (op (of a✝)) with
    | op f =>
      match op (of a✝), op (of a✝), f, 𝟙 (op (of a✝)) with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    𝟙
      (match op (of a✝) with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

case star
C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
⊢ (match 𝟙 (op star) with
    | op f =>
      match op star, op star, f, 𝟙 (op star) with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    𝟙
      (match op star with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithTerminal Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match x with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
cases x

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match WithTerminal.of a✝, WithTerminal.of a✝, 𝟙 (WithTerminal.of a✝) with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match WithTerminal.of a✝ with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match WithTerminal.star, WithTerminal.star, 𝟙 WithTerminal.star with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match WithTerminal.star with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange → P.pullbacks ≤ P

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
⊢ P.pullbacks ≤ P
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pullbacks ≤ P → P.IsStableUnderBaseChange

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
⊢ P.IsStableUnderBaseChange
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderCobaseChange → P.pushouts ≤ P

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
⊢ P.pushouts ≤ P
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pushouts ≤ P → P.IsStableUnderCobaseChange

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
⊢ P.IsStableUnderCobaseChange
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P ≤ Q → P.pushouts ≤ Q

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
h : P ≤ Q
⊢ P.pushouts ≤ Q
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
⊢ m ≫ c₂.fst =
    ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      c₂.fst

Tactic:
(BinaryFan.IsLimit.lift' t₂ _ _).2.1

Goal state after:
case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
⊢ m ≫ c₂.fst = s.π.app { as := 0 }
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hf
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P (Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))

pp: case hg
C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P (Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))

Tactic:
exacts [underPushoutMap _ _ h₂, underPushoutMap _ _ h₁]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : IsIso f
j : J
⊢ c₁.ι.app j ≫ φ ≫ h₂.desc { pt := c₁.pt, ι := inv f ≫ c₁.ι } = c₁.ι.app j ≫ 𝟙 c₁.pt

Tactic:
by simp [reassoc_of% (hφ j)]

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ P ≤ Q → coproducts.{w, v, u} P ≤ Q

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
h : P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q