mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g) =
    (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((fun x x_1 ↦
          ((fun x x_2 ↦
                  (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                    ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                (F.obj x) x_1).trans
            (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
        Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((fun x x_1 ↦
          ((fun x x_2 ↦
                  (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                    ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                (F.obj x) x_1).trans
            (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
        Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z).symm f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f))

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z).symm f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((fun x x_1 ↦
              ((fun x x_2 ↦
                      (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                        ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                    (F.obj x) x_1).trans
                (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
            Y Z).symm
        f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))).symm f))

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((fun x x_1 ↦
              ((fun x x_2 ↦
                      (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                        ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                    (F.obj x) x_1).trans
                (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
            Y Z).symm
        f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))).symm f))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ (ihom.ev x).app y = (ihom.ev x).app y

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ ((𝟭 C).obj y)).inv ≫ (𝟭 C).obj y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ ((𝟭 C).obj y)).inv ≫ (𝟭 C).obj y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ uncurry (id y ≫ 𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ uncurry (id y ≫ 𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      w ◁ curry (compTranspose w x y) ▷ (ihom y).obj z ≫ compTranspose w y z =
    w ◁ (ihom w).obj x ◁ curry (compTranspose x y z) ≫ compTranspose w x z

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      w ◁ curry (compTranspose w x y) ▷ (ihom y).obj z ≫ compTranspose w y z =
    w ◁ (ihom w).obj x ◁ curry (compTranspose x y z) ≫ compTranspose w x z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        (w ◁
                curry
                  ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫
                    (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ≫
              (ihom.ev w).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    w ◁
        (ihom w).obj x ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
      (α_ w ((ihom w).obj x) ((ihom x).obj z)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).app z

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        (w ◁
                curry
                  ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫
                    (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ≫
              (ihom.ev w).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    w ◁
        (ihom w).obj x ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
      (α_ w ((ihom w).obj x) ((ihom x).obj z)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).app z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    (α_ w ((ihom w).obj x) ((ihom x).obj y ⊗ (ihom y).obj z)).inv ≫
      (ihom.ev w).app x ▷ ((ihom x).obj y ⊗ (ihom y).obj z) ≫
        (α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    (α_ w ((ihom w).obj x) ((ihom x).obj y ⊗ (ihom y).obj z)).inv ≫
      (ihom.ev w).app x ▷ ((ihom x).obj y ⊗ (ihom y).obj z) ≫
        (α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry (ρ_ X).hom = id X

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry (ρ_ X).hom = id X
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ (λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (pre f).app Z

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ (λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (pre f).app Z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z = f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ihom X).map f

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ihom X).map f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (𝟭 C).obj Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (𝟭 C).obj Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ihom.ev X).app Y ≫ f = (ihom.ev X).app Y ≫ f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = curry' (f ≫ g)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
⊢ m :: l = m :: l

Tactic:
]

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
⊢ (sum fun i ↦ #(WType β) ^ lift.{u, v} #(β i)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)

Tactic:
]

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
⊢ 1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
⊢ 1 ≤ ⨆ a, m ^ lift.{u, v} #(β a)
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ ?m.139 ^ 0 ≤ m ^ lift.{u, v} #(β a)

pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := ⋯
a : α
⊢ Cardinal.{max u v}

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ ?m.139 ^ 0 ≤ m ^ lift.{u, v} #(β a)

α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := ⋯
a : α
⊢ Cardinal.{max u v}
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ max #α ℵ₀ = max #α ℵ₀

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ Subtype.val '' ↑(rangeOfWType s)

Tactic:
]

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ Subtype.val '' ↑(rangeOfWType s)
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Set.range (WType.elim (↥(closure s)) (operate s)) = Set.univ

Tactic:
]

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Set.range (WType.elim (↥(closure s)) (operate s)) = Set.univ
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
]

Goal state after:
case e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ ℵ₀ = ℵ₀

pp: case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #↑s ≤ ℵ₀

Tactic:
]

Goal state after:
case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #↑s ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ #↑s = #↑s

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ (ε_ X₁ Y₁ ▷ 𝟙_ C ≫ 𝟙_ C ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) =
    (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ (ε_ X₁ Y₁ ▷ 𝟙_ C ≫ 𝟙_ C ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 ((Y₂ ⊗ Y₁) ⊗ 𝟙_ C) ⊗≫ Y₂ ◁ ⊗𝟙.hom ⊗≫ ⊗𝟙.hom ▷ Y₁ ⊗≫ 𝟙 (𝟙_ C ⊗ Y₂ ⊗ Y₁) = (ρ_ (Y₂ ⊗ Y₁)).hom ≫ (λ_ (Y₂ ⊗ Y₁)).inv

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 ((Y₂ ⊗ Y₁) ⊗ 𝟙_ C) ⊗≫ Y₂ ◁ ⊗𝟙.hom ⊗≫ ⊗𝟙.hom ▷ Y₁ ⊗≫ 𝟙 (𝟙_ C ⊗ Y₂ ⊗ Y₁) = (ρ_ (Y₂ ⊗ Y₁)).hom ≫ (λ_ (Y₂ ⊗ Y₁)).inv
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0

Tactic:
]

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i

Tactic:
]

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i

Tactic:
]

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ (b.toDual m) (b i) = (b.toDual m) (b i)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
m : M
⊢ (b.toDual (b i)) m = (b.toDual (b i)) m

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
m : M
i : ι
⊢ (b.repr m) i = (b.repr m) i

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : b.toDual m = 0
⊢ b.toDual m = 0

Tactic:
]

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : b.toDual m = 0
⊢ b.toDual m = 0
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
⊢ Module.rank K (ℕ → K) < #K

Tactic:
]

Goal state after:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
⊢ Module.rank K (ℕ → K) < #K
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case e'_3.h₁
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ i = j ↔ i = j

Tactic:
]

Goal state after: