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

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)),
    lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h) = s.snd

pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯

Tactic:
·

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)),
    lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h) = s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯

Tactic:
·

Goal state after:
case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: 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

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:
·

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
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:
·

Goal state after:
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.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.diagonal f → P.diagonal (e.hom ≫ f)

pp: case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.diagonal f → P.diagonal (f ≫ e.hom)

Tactic:
·

Goal state after:
case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.diagonal f → P.diagonal (e.hom ≫ f)
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'
⊢ ∀ {X Y : C} (x : X ≅ Y), P.colimitsOfShape J X → P.colimitsOfShape J Y

Tactic:
rintro _ _ e ⟨h⟩; exact ⟨h.ofIso e⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ (P.strictColimitsOfShape J).isoClosure ≤ P.colimitsOfShape J

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape J ≤ (P.strictColimitsOfShape J).isoClosure

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ (P.strictColimitsOfShape J).isoClosure ≤ P.colimitsOfShape J
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape J ≤ (P.strictColimitsOfShape J).isoClosure

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape J ≤ (P.strictColimitsOfShape J).isoClosure
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.diagonal f → P.diagonal (f ≫ e.hom)

Tactic:
·

Goal state after:
case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.diagonal f → P.diagonal (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : P.HasOfPostcompProperty Q
X Y : C
f : X ⟶ Y
hf : Q f
⊢ P.diagonal f

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ P g

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : P.HasOfPostcompProperty Q
X Y : C
f : X ⟶ Y
hf : Q f
⊢ P.diagonal f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ P g

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ P g
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_2.hf
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P gr

pp: case refine_2.hg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (pullback.snd (g ≫ f) f)

Tactic:
·

Goal state after:
case refine_2.hf
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P gr
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_2.hg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (pullback.snd (g ≫ f) f)

Tactic:
·

Goal state after:
case refine_2.hg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (pullback.snd (g ≫ f) f)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)

pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)

Tactic:
·

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.colimitsOfShape J X
h : P.ColimitOfShape J X
⊢ P.op.LimitOfShape Jᵒᵖ (Opposite.op X)

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.limitsOfShape Jᵒᵖ).unop X
h : P.op.LimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.ColimitOfShape J X

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.colimitsOfShape J X
h : P.ColimitOfShape J X
⊢ P.op.LimitOfShape Jᵒᵖ (Opposite.op X)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.limitsOfShape Jᵒᵖ).unop X
h : P.op.LimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.ColimitOfShape J X

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.limitsOfShape Jᵒᵖ).unop X
h : P.op.LimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.ColimitOfShape J X
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.limitsOfShape J X
h : P.LimitOfShape J X
⊢ P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.limitsOfShape J X
h : P.LimitOfShape J X
⊢ P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)

Tactic:
·

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
·

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ
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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ = lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
·

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ = lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ
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
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
·

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ (β_ X Y).inv ≫ fst X Y = snd Y X

Tactic:
by
  simp [fst_def, snd_def, ← BraidedCategory.braiding_inv_naturality_left_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: 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

pp: 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

Tactic:
·

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
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: 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

Tactic:
·

Goal state after:
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: case h_snd
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
x✝¹ x✝ : C
⊢ (e₁ x✝¹ x✝).hom ≫ snd x✝ x✝¹ = (e₂ x✝¹ x✝).hom ≫ snd x✝ x✝¹

Tactic:
·

Goal state after:
case h_snd
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
x✝¹ x✝ : C
⊢ (e₁ x✝¹ x✝).hom ≫ snd x✝ x✝¹ = (e₂ x✝¹ x✝).hom ≫ snd x✝ x✝¹
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommSemiring R
inst✝¹³ : NonUnitalNonAssocSemiring A
inst✝¹² : Module R A
inst✝¹¹ : SMulCommClass R A A
inst✝¹⁰ : IsScalarTower R A A
inst✝⁹ : AddCommMonoid C
inst✝⁸ : Module R C
inst✝⁷ : CoalgebraStruct R C
D : Type u_7
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R B
inst✝⁴ : CoalgebraStruct R B
inst✝³ : NonUnitalNonAssocSemiring D
inst✝² : Module R D
inst✝¹ : SMulCommClass R D D
inst✝ : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv
      (mul' R (A ⊗[R] D) ∘ₗ
        ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv)) ∘ₗ
          ↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) ∘ₗ AlgebraTensorModule.map δ δ) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)

Tactic:
mul'_tensor,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommSemiring R
inst✝¹³ : NonUnitalNonAssocSemiring A
inst✝¹² : Module R A
inst✝¹¹ : SMulCommClass R A A
inst✝¹⁰ : IsScalarTower R A A
inst✝⁹ : AddCommMonoid C
inst✝⁸ : Module R C
inst✝⁷ : CoalgebraStruct R C
D : Type u_7
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R B
inst✝⁴ : CoalgebraStruct R B
inst✝³ : NonUnitalNonAssocSemiring D
inst✝² : Module R D
inst✝¹ : SMulCommClass R D D
inst✝ : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv
      (((mul' R A ⊗ₘ mul' R D) ∘ₗ ↑(tensorTensorTensorComm R A D A D)) ∘ₗ
        ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv)) ∘ₗ
          ↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) ∘ₗ AlgebraTensorModule.map δ δ) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case refine_1
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 : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.fst ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))) =
    (Iso.refl ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).pt).hom ≫
      BinaryFan.fst
        (Cone.extend (BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd (F.obj A) (F.obj B))) (prodComparison F A B))

pp: case refine_2
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 : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.snd ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))) =
    (Iso.refl ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).pt).hom ≫
      BinaryFan.snd
        (Cone.extend (BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd (F.obj A) (F.obj B))) (prodComparison F A B))

Tactic:
·

Goal state after:
case refine_1
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 : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.fst ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))) =
    (Iso.refl ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).pt).hom ≫
      BinaryFan.fst
        (Cone.extend (BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd (F.obj A) (F.obj B))) (prodComparison F A B))