mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2

pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r

Tactic:
·

Goal state after:
case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none

pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
·

Goal state after:
case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
·

Goal state after:
case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none

pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
·

Goal state after:
case none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      none =
    ↑(ConcreteCategory.hom f.hom) none
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (hom (limit.π (F ⋙ objects) Y✝)) X = (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) X)

pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) Y) = (hom (limit.π (F ⋙ objects) Y✝)) Y

Tactic:
·

Goal state after:
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (hom (limit.π (F ⋙ objects) Y✝)) X = (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) X)
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
·

Goal state after:
case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) Y) = (hom (limit.π (F ⋙ objects) Y✝)) Y

Tactic:
·

Goal state after:
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) Y) = (hom (limit.π (F ⋙ objects) Y✝)) Y
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ (j : J) →
    (homDiagram
          ((hom
              (limit.lift (F ⋙ objects)
                { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
            X✝)
          ((hom
              (limit.lift (F ⋙ objects)
                { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
            Y✝)).obj
      j

pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ ∀ (j j' : J) (f : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f))
        (?x j) =
      ?x j'

Tactic:
·

Goal state after:
case x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ (j : J) →
    (homDiagram
          ((hom
              (limit.lift (F ⋙ objects)
                { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
            X✝)
          ((hom
              (limit.lift (F ⋙ objects)
                { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
            Y✝)).obj
      j
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (homDiagram
        ((hom
            (limit.lift (F ⋙ objects)
              { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
          X✝)
        ((hom
            (limit.lift (F ⋙ objects)
              { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
          Y✝)).obj
    j

Tactic:
refine eqToHom ?_ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ?_ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ ∀ (j j' : J) (f_1 : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f_1))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
      eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ ∀ (j j' : J) (f_1 : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f_1))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
      eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X : ↑s.pt), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X

pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X : ↑s.pt), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ fst A A = lift (𝟙 A) (𝟙 A) ≫ fst A A

pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ snd A A = lift (𝟙 A) (𝟙 A) ≫ snd A A

Tactic:
·

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ fst A A = lift (𝟙 A) (𝟙 A) ≫ fst A A
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ snd A A = lift (𝟙 A) (𝟙 A) ≫ snd A A

Tactic:
·

Goal state after:
case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ snd A A = lift (𝟙 A) (𝟙 A) ≫ snd A A
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inl.inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inl_ C C').map f✝¹ = (Sum.inl_ C C').map f✝

pp: case inr.inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝

Tactic:
·

Goal state after:
case inl.inl
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inl_ C C').map f✝¹ = (Sum.inl_ C C').map f✝
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: case inr.inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝

Tactic:
·

Goal state after:
case inr.inr
C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x✝ y✝ : C'
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
·

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_1
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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
          (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
            L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)

pp: case refine_2
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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫
          (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom

Tactic:
·

Goal state after:
case refine_1
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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
          (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
            L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂L X Y Z).hom = X ◁ coprod.inr

Tactic:
by
  rw [leftDistrib_hom, coprod.inr_desc]

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

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inl_ A B).map f✝) ≫
      (match (Sum.inl_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inl_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inl_ A B).map f✝)

pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inr_ A B).map f✝) ≫
      (match (Sum.inr_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inr_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inr_ A B).map f✝)

Tactic:
·

Goal state after:
case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inl_ A B).map f✝) ≫
      (match (Sum.inl_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inl_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inl_ A B).map f✝)
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inr_ A B).map f✝) ≫
      (match (Sum.inr_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inr_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inr_ A B).map f✝)

Tactic:
·

Goal state after:
case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inr_ A B).map f✝) ≫
      (match (Sum.inr_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inr_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inr_ A B).map f✝)