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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := ⋯
i : J
hi : i ∈ l
⊢ ∀ ⦃x y : J⦄, Zag x y → Zigzag y j₂ → Zigzag x j₂

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
i : J
hi : i ∈ l
j : J
⊢ ∀ ⦃y : J⦄, Zag j y → Zigzag y j₂ → Zigzag j j₂
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
F : typeToCat.obj X ⟶ C
x✝¹ x✝ : ↑(of (Discrete ((fun X ↦ X) X)))
as✝ : X
f : { as := as✝ } ⟶ { as := { as := as✝ }.as }
⊢ ((fun f ↦ (Discrete.functor ⇑(ConcreteCategory.hom f)).toCatHom)
            ((fun F ↦ ↾fun x ↦ F.toFunctor.obj { as := x }) F)).toFunctor.map
      f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ (∃ a_1 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_1) →
    ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩

Tactic:
simp

Goal state after:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ ∀ (x : ¬f.toFun a = Y.point) (x_1 : ¬g.toFun (f.toFun a) = Z.point),
    ⟨g.toFun (f.toFun a), ⋯⟩ = ⟨c, hc⟩ → c = g.toFun (f.toFun a)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ (∃ x, f a = b) ↔ f a = b

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X : PartialFun
x : X
⊢ ↑(ConcreteCategory.hom
          (partialFunToPointed.map
              ((NatIso.ofComponents
                      (fun X ↦
                        PartialFun.Iso.mk
                          { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯,
                            right_inv := ⋯ })
                      ⋯).hom.app
                X) ≫
            (NatIso.ofComponents (fun X ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯).hom.app
              (partialFunToPointed.obj X)))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)

Tactic:
simp

Goal state after:
case some
X : PartialFun
x : X
⊢ ↑(ConcreteCategory.hom
          ({ toFun := Option.elim' none fun a ↦ some ⟨some a, ⋯⟩, map_point := ⋯ } ≫
            (Pointed.Iso.mk (Equiv.optionSubtypeNe (partialFunToPointed.obj X).point) ⋯).hom))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
⊢ f.fix a = f.fix a'

Tactic:
ext b

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝¹ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
pf✝ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a pf✝
⊢ C a

Tactic:
induction ‹Acc (Sum.inr · ∈ f ·) a› with | intro a ha IH => _

Goal state after:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a✝ : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
a : α
ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y ↦ Sum.inr x ∈ f y) y
IH :
  (y : α) →
    (a : Sum.inr y ∈ f a) →
      b ∈
          WellFounded.fixF
            (fun a IH ↦
              Part.assert (f a).Dom fun hf ↦
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            y ⋯ →
        C y
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
⊢ C a
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) (Sum.inl b)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hbase a fa

Tactic:
simp

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun y ↦ (f a).get ⋯ = y → C a) (Sum.inr a')
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction h' fun a' h ih ↦
        Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → (fun x ↦ C x) a') ((f a').get ⋯)
          (fun b' e ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun a'' e ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
x✝ : α
⊢ x✝ ∈ (↑f).preimage s ↔ x✝ ∈ f ⁻¹' s

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ (x, y) ∈ (graphFunctor.map (asIso (↾f)).hom).rel ↔ (x, y) ∈ r.rel

Tactic:
exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ (PFun.id β).comp f x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ f.comp (PFun.id α) x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ (f.comp g).Dom ↔ x✝ ∈ g.preimage f.Dom

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y a, a ∈ g x✝ ∧ y ∈ f a) ↔ ∃ y, (∃ y_1, y_1 ∈ f y) ∧ y ∈ g x✝
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝¹ : α
x✝ : γ
⊢ x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ (↑g).comp (↑f) x✝¹

Tactic:
by simp only [coe_val, comp_apply, Function.comp, Part.bind_some]

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j j' : J
f : j ⟶ j'
⊢ (hom ((homDiagram X X).map f)) (𝟙 ((hom (limit.π (F ⋙ objects) j)) X)) = 𝟙 ((hom (limit.π (F ⋙ objects) j')) X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans (L.colimitIsoColimitGrothendieck (L ⋙ G))
              (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).symm)
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun x ↦ Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x)) ⋯)))
          (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
            (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)))
        (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))))
      (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)))
    ((𝟭 T).colimitIsoColimitGrothendieck G).symm
x✝ : Grothendieck (R ⋙ functor L)
⊢ colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).hom ≫
        (L.colimitIsoColimitGrothendieck (L ⋙ G)).inv ≫ colimit.pre G L =
    colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (HasColimit.isoOfNatIso (NatIso.ofComponents (fun x ↦ Iso.refl (G.obj (L.obj (left x.fiber)))) ⋯)).hom ≫
        (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
              (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)).hom ≫
          (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))).hom ≫
            (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)).hom ≫
              ((𝟭 T).colimitIsoColimitGrothendieck G).inv

Tactic:
simp

Goal state after:
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:
intro j

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.refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ (hom (limit.π (F ⋙ objects) j))
      ((hom
          (limit.lift (F ⋙ objects)
            { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
        X✝) =
    (s.π.app j).toFunctor.obj X✝

Tactic:
simp

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

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

Tactic:
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:
intro j

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' : 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 h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
⊢ eqToHom ⋯ ≫ (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
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
⊢ ∀ (j : J),
    (hom (limit.π (F ⋙ objects) j)) ((limitConeLift F s).toFunctor.obj X) =
      (hom (limit.π (F ⋙ objects) j)) (m.toFunctor.obj X)

Tactic:
intro j

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
j : J
⊢ (hom (limit.π (F ⋙ objects) j)) ((limitConeLift F s).toFunctor.obj X) =
    (hom (limit.π (F ⋙ objects) j)) (m.toFunctor.obj X)
Module: Mathlib.CategoryTheory.Localization.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
inst✝⁷ : Category.{v_5, u_5} E
inst✝⁶ : Category.{v_6, u_6} E'
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv).app
            (L₁.obj X₁)).app
        (L₂.obj X₂) =
      ((𝟙 F₁').app (L₁.obj X₁)).app (L₂.obj X₂)

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
inst✝⁷ : Category.{v_5, u_5} E
inst✝⁶ : Category.{v_6, u_6} E'
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom).app
            (L₁.obj X₁)).app
        (L₂.obj X₂) =
      ((𝟙 F₂').app (L₁.obj X₁)).app (L₂.obj X₂)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case e_self.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case e'_3
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₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case e'_4
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₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hf
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)).f = (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂).f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)).F = (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂).F

Tactic:
simp

Goal state after:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
      prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) ≫ π₁ =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
        prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) ≫
      π₁

Tactic:
simp

Goal state after:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F = prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.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₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F) ≫ π₂ =
    π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
        prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) ≫
      π₂

Tactic:
simp

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F = prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case hF.h₁.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) = prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F)

Tactic:
simp

Goal state after: