mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ CommSq g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
constructor

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ autoParam (g ≫ diagonal f = lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) CommSq.w._autoParam
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ autoParam (g ≫ diagonal f = lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) CommSq.w._autoParam

Tactic:
ext

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ fst f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ fst f f

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (g ≫ diagonal f) ≫ snd f f = (lift (𝟙 Y) g ⋯ ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≫ snd f f
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
refine ⟨.ofObj Y, inferInstance, (monotone_retractClosure h₂).trans ?_⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
⊢ Q.isoClosure.retractClosure ≤ (ofObj Y).isoClosure
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
⊢ W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.IsStableUnderColimitsOfShape J → W.colimitsOfShape J ≤ W

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.colimitsOfShape J ≤ W → W.IsStableUnderColimitsOfShape J
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
⊢ W.IsStableUnderColimitsOfShape J

Tactic:
constructor

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
⊢ ∀ (X₁ X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x : Discrete PUnit.{w + 1}
⊢ x = ⊥_ Discrete PUnit.{w + 1}

Tactic:
ext

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

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

Tactic:
constructor

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

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
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv = pullback.diagonal f.op

Tactic:
ext

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ ((codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv) ≫ pullback.fst f.op f.op =
    pullback.diagonal f.op ≫ pullback.fst f.op f.op

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ ((codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv) ≫ pullback.snd f.op f.op =
    pullback.diagonal f.op ≫ pullback.snd f.op f.op
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape J
⊢ P.op.IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
← isClosedUnderColimitsOfShape_iff_op

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape J
⊢ P.IsClosedUnderColimitsOfShape J
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M : Mon C
f : M ⟶ 𝟙_ (Mon C)
⊢ f = { hom := toUnit M.X, isMonHom_hom := ⋯ }

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M : Mon C
f : M ⟶ 𝟙_ (Mon C)
⊢ f.hom = { hom := toUnit M.X, isMonHom_hom := ⋯ }.hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := fst M.X N.X, isMonHom_hom := ⋯ } =
    M ◁ (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N ≫ (ρ_ M).hom

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := fst M.X N.X, isMonHom_hom := ⋯ }.hom =
    (M ◁ (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N ≫ (ρ_ M).hom).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := snd M.X N.X, isMonHom_hom := ⋯ } =
    (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M ▷ N ≫ (λ_ N).hom

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := snd M.X N.X, isMonHom_hom := ⋯ }.hom =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M ▷ N ≫ (λ_ N).hom).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst X Y = lift (f ≫ g) (f ≫ h) ≫ fst X Y

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd X Y = lift (f ≫ g) (f ≫ h) ≫ snd X Y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) = 𝟙 (X ⊗ Y)

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ fst X Y = 𝟙 (X ⊗ Y) ≫ fst X Y

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ snd X Y = 𝟙 (X ⊗ Y) ≫ snd X Y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ (h ⊗ₘ k) = lift (f ≫ h) (g ≫ k)

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ fst Y Z = lift (f ≫ h) (g ≫ k) ≫ fst Y Z

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ snd Y Z = lift (f ≫ h) (g ≫ k) ≫ snd Y Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') = g ⊗ₘ g'

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ fst X Z = (g ⊗ₘ g') ≫ fst X Z

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ snd X Z = (g ⊗ₘ g') ≫ snd X Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom = lift f₁ (lift f₂ f₃)

Tactic:
ext

Goal state after:
case e_a.e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ (lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ fst M (M ⊗ M) = lift f₁ (lift f₂ f₃) ≫ fst M (M ⊗ M)

case h_snd.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ fst M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ fst M M

case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ snd M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ snd M M
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ μ = μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z) = fst W X ⊗ₘ fst Y Z

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ fst W Y = (fst W X ⊗ₘ fst Y Z) ≫ fst W Y

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ snd W Y = (fst W X ⊗ₘ fst Y Z) ≫ snd W Y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z) = snd W X ⊗ₘ snd Y Z

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ fst X Z = (snd W X ⊗ₘ snd Y Z) ≫ fst X Z

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ snd X Z = (snd W X ⊗ₘ snd Y Z) ≫ snd X Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z) = fst W Y ⊗ₘ fst X Z

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z)) ≫ fst W X = (fst W Y ⊗ₘ fst X Z) ≫ fst W X

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z)) ≫ snd W X = (fst W Y ⊗ₘ fst X Z) ≫ snd W X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z) = snd W Y ⊗ₘ snd X Z

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z)) ≫ fst Y Z = (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z

case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z)) ≫ snd Y Z = (snd W Y ⊗ₘ snd X Z) ≫ snd Y Z
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
      ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) =
    (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)

Tactic:
ext

Goal state after:
case e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      fst N.X N.X =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ fst N.X N.X

case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      snd N.X N.X =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ snd N.X N.X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
⊢ yonedaMon.essImage F ↔ (F ⋙ forget MonCat).IsRepresentable

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
⊢ yonedaMon.essImage F → (F ⋙ forget MonCat).IsRepresentable

case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
⊢ (F ⋙ forget MonCat).IsRepresentable → yonedaMon.essImage F
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ F.obj A ◁ F.map g

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ fst (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ fst (F.obj A) (F.obj B')

case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ snd (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ snd (F.obj A) (F.obj B')
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ F.map (f ▷ B) ≫ prodComparison F A' B = prodComparison F A B ≫ F.map f ▷ F.obj B

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ fst (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ fst (F.obj A') (F.obj B)

case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ snd (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ snd (F.obj A') (F.obj B)
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ (ofHom (counitAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op = (λ_ (op (of R A))).hom

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom ((ofHom (counitAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom (λ_ (op (of R A))).hom.unop) x✝
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ op (of R A) ◁ (ofHom (counitAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op = (ρ_ (op (of R A))).hom

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom (op (of R A) ◁ (ofHom (counitAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom (ρ_ (op (of R A))).hom.unop) x✝
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ (ofHom (comulAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op =
    (α_ (op (of R A)) (op (of R A)) (op (of R A))).hom ≫
      op (of R A) ◁ (ofHom (comulAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom ((ofHom (comulAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom
        ((α_ (op (of R A)) (op (of R A)) (op (of R A))).hom ≫
            op (of R A) ◁ (ofHom (comulAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op).unop)
      x✝
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
⊢ (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))).hom ≫ μ = μ

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
x✝ : ↑(unop (op (CommAlgCat.of R A)))
⊢ (CommAlgCat.Hom.hom ((β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))).hom ≫ μ).unop) x✝ =
    (CommAlgCat.Hom.hom μ.unop) x✝