mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.inv = (prodComparisonIso F X Y).inv

Tactic:
;

Goal state after:
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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.inv = (prodComparisonIso F X Y).inv
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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm = prodComparisonIso F X Y

Tactic:
;

Goal state after:
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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm = prodComparisonIso F X Y
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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.hom = (prodComparisonIso F X Y).hom

Tactic:
;

Goal state after:
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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.hom = (prodComparisonIso F X Y).hom
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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z : C
inst✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv =
    ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z : C
inst✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv =
    ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
x✝ : A
⊢ (counit ∘ₗ antipode R) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
x✝ : A
⊢ (counit ∘ₗ antipode R) x✝ = counit x✝
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
g h : A ⟶ B
⊢ lift g (lift (g ≫ ι) h ≫ μ) ≫ μ = h

Tactic:
;

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
g h : A ⟶ B
⊢ lift g (lift (g ≫ ι) h ≫ μ) ≫ μ = h
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g : A ⟶ B
⊢ f = lift (g ≫ ι) (lift g f ≫ μ) ≫ μ

Tactic:
;

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g : A ⟶ B
⊢ f = lift (g ≫ ι) (lift g f ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
g h : A ⟶ B
⊢ lift (lift g (h ≫ ι) ≫ μ) h ≫ μ = g

Tactic:
;

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
g h : A ⟶ B
⊢ lift (lift g (h ≫ ι) ≫ μ) h ≫ μ = g
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f h : A ⟶ B
⊢ f = lift (lift f h ≫ μ) (h ≫ ι) ≫ μ

Tactic:
;

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f h : A ⟶ B
⊢ f = lift (lift f h ≫ μ) (h ≫ ι) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ CategoryTheory.inv ι = ι

Tactic:
by
  rw [eq_comm, ← CategoryTheory.inv_comp_eq_id, IsIso.inv_inv, inv_comp_inv]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ (mulRight η).hom = (Iso.refl A).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ (mulRight η).hom = (Iso.refl A).hom
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv (antipode R) * toConv id).ofConv c = (ofConv 1) c

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv (antipode R) * toConv id).ofConv c = (ofConv 1) c
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv (antipode R)).ofConv ((ℛ R c).left i) * (toConv id).ofConv ((ℛ R c).right i) =
    (ofConv 1) c

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv (antipode R)).ofConv ((ℛ R c).left i) * (toConv id).ofConv ((ℛ R c).right i) =
    (ofConv 1) c
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv id * toConv (antipode R)).ofConv c = (ofConv 1) c

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv id * toConv (antipode R)).ofConv c = (ofConv 1) c
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv id).ofConv ((ℛ R c).left i) * (toConv (antipode R)).ofConv ((ℛ R c).right i) =
    (ofConv 1) c

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv id).ofConv ((ℛ R c).left i) * (toConv (antipode R)).ofConv ((ℛ R c).right i) =
    (ofConv 1) c
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
x✝¹ x✝ : C
⊢ ((AlgebraTensorModule.curry (mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (δ ∘ₗ mul' R C)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
x✝¹ x✝ : C
⊢ ((AlgebraTensorModule.curry (mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (δ ∘ₗ mul' R C)) x✝¹) x✝
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ (δ ∘ₗ Algebra.linearMap R C) 1 = (Algebra.linearMap R (C ⊗[R] C)) 1

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ (δ ∘ₗ Algebra.linearMap R C) 1 = (Algebra.linearMap R (C ⊗[R] C)) 1
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ 1 = 1 ⊗ₜ[R] 1

Tactic:
;

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ 1 = 1 ⊗ₜ[R] 1
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₂ : GrpObj X
toMonObj✝ : MonObj X
inv✝ : X ⟶ X
left_inv✝ : lift inv✝ (𝟙 X) ≫ μ = toUnit X ≫ η
right_inv✝ : lift (𝟙 X) inv✝ ≫ μ = toUnit X ≫ η
e : { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toMonObj = h₂.toMonObj
this : ι = ι
⊢ { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ } = h₂

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₂ : GrpObj X
toMonObj✝ : MonObj X
inv✝ : X ⟶ X
left_inv✝ : lift inv✝ (𝟙 X) ≫ μ = toUnit X ≫ η
right_inv✝ : lift (𝟙 X) inv✝ ≫ μ = toUnit X ≫ η
e : { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toMonObj = h₂.toMonObj
this : ι = ι
⊢ { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ } = h₂
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f⁻¹ * f =
    toConv
      ((lmul' R).comp
        ((Algebra.TensorProduct.map (f.ofConv.comp (antipodeAlgHom R A)) (f.ofConv.comp (AlgHom.id R A))).comp
          (comulAlgHom R A)))

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f⁻¹ * f =
    toConv
      ((lmul' R).comp
        ((Algebra.TensorProduct.map (f.ofConv.comp (antipodeAlgHom R A)) (f.ofConv.comp (AlgHom.id R A))).comp
          (comulAlgHom R A)))
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom.hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom.hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ x✝¹ x✝ : Grp C
⊢ ((α_ x✝¹ (𝟙_ (Grp C)) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom).hom.hom = ((ρ_ x✝¹).hom ▷ x✝).hom.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ x✝¹ x✝ : Grp C
⊢ ((α_ x✝¹ (𝟙_ (Grp C)) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom).hom.hom = ((ρ_ x✝¹).hom ▷ x✝).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H H₁ H₂ G : Grp C
f : G ⟶ 𝟙_ (Grp C)
⊢ f.hom.hom = (homMk' (toUnit G.toMon)).hom.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H H₁ H₂ G : Grp C
f : G ⟶ 𝟙_ (Grp C)
⊢ f.hom.hom = (homMk' (toUnit G.toMon)).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (fst G.toMon H.toMon)).hom.hom =
    (G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom).hom.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (fst G.toMon H.toMon)).hom.hom =
    (G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (snd G.toMon H.toMon)).hom.hom =
    ((IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from G ▷ H ≫ (λ_ H).hom).hom.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (snd G.toMon H.toMon)).hom.hom =
    ((IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from G ▷ H ≫ (λ_ H).hom).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X Y : C
inst✝ : Closed A
g : A ⊗ Y ⟶ X
⊢ A ◁ curry g ≫ (ihom.ev A).app X = g

Tactic:
by
  simp [curry_eq]

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

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
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : Grp C
e : F.mapGrp.obj H ≅ G
⊢ F.essImage G.X

Tactic:
;

Goal state after:
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
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : Grp C
e : F.mapGrp.obj H ≅ G
⊢ F.essImage G.X
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.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l

Tactic:
by rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2)
    (m ::
      match l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))

Tactic:
;

Goal state after:
l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2)
    (m ::
      match l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))
Module: Mathlib.Data.W.Cardinal

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

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
⊢ (sum fun i ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun a ↦ κ ^ #(β a)) ≤ κ

Tactic:
;

Goal state after:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun a ↦ κ ^ #(β a)) ≤ κ
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) x * WType.elim (↥(closure s)) (operate s) y ∈
    Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
;

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) x * WType.elim (↥(closure s)) (operate s) y ∈
    Set.range (WType.elim (↥(closure s)) (operate s))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) x + WType.elim (↥(closure s)) (operate s) y ∈
    Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
;

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) x + WType.elim (↥(closure s)) (operate s) y ∈
    Set.range (WType.elim (↥(closure s)) (operate s))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ -WType.elim (↥(closure s)) (operate s) x ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
;

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ (WType.elim (↥(closure s)) (operate s) x)⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
;

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ (WType.elim (↥(closure s)) (operate s) x)⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«0»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨0, ⋯⟩))

Tactic:
;

Goal state after:
case convert_3.inl.«0»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨0, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«1»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨1, ⋯⟩))

Tactic:
;

Goal state after:
case convert_3.inl.«1»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨1, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«2»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨2, ⋯⟩))

Tactic:
;

Goal state after:
case convert_3.inl.«2»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨2, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«3»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨3, ⋯⟩))

Tactic:
;

Goal state after:
case convert_3.inl.«3»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨3, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«4»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨4, ⋯⟩))

Tactic:
;

Goal state after:
case convert_3.inl.«4»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨4, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨5, ⋯⟩))

Tactic:
;

Goal state after:
case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨5, ⋯⟩))