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

Goal state before:
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_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))
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.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

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.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom = F.map (fst 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.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom = F.map (fst 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.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom = F.map (fst 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.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ snd (F.obj X) (F.obj Y) = F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom

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.OplaxMonoidal
X Y : C
⊢ F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom = F.map (snd 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.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ snd (F.obj X) (F.obj Y) = F.map (toUnit X ▷ Y) ≫ F.map (λ_ 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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom = F.map (snd 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.OplaxMonoidal
X Y : C
⊢ F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom = F.map (snd X Y)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case η
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✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ η F = η F

pp: case δ
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✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ δ F = δ F

Tactic:
·

Goal state after:
case η
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✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ η F = η F
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case δ
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✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ δ F = δ F

Tactic:
·

Goal state after:
case δ
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✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ δ F = δ F
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry
          (LinearMap.mul' S (B ⊗[R] A) ∘ₗ
            LinearMap.rTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul))
        x)
      y =
    (LinearMap.mul' S B) ((LinearMap.rTensor B (antipode S)) (comul x)) ⊗ₜ[R]
      (LinearMap.mul' R A) ((LinearMap.rTensor A (antipode R)) (comul y))

pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry (Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit)) x) y =
    (algebraMap S B) (counit x) ⊗ₜ[R] (algebraMap R A) (counit y)

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry
          (LinearMap.mul' S (B ⊗[R] A) ∘ₗ
            LinearMap.rTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul))
        x)
      y =
    (LinearMap.mul' S B) ((LinearMap.rTensor B (antipode S)) (comul x)) ⊗ₜ[R]
      (LinearMap.mul' R A) ((LinearMap.rTensor A (antipode R)) (comul y))
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry (Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit)) x) y =
    (algebraMap S B) (counit x) ⊗ₜ[R] (algebraMap R A) (counit y)

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry (Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit)) x) y =
    (algebraMap S B) (counit x) ⊗ₜ[R] (algebraMap R A) (counit y)
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry
          (LinearMap.mul' S (B ⊗[R] A) ∘ₗ
            LinearMap.lTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul))
        x)
      y =
    (LinearMap.mul' S B) ((LinearMap.lTensor B (antipode S)) (comul x)) ⊗ₜ[R]
      (LinearMap.mul' R A) ((LinearMap.lTensor A (antipode R)) (comul y))

pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry (Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit)) x) y =
    (algebraMap S B) (counit x) ⊗ₜ[R] (algebraMap R A) (counit y)

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
x : B
y : A
⊢ ((AlgebraTensorModule.curry
          (LinearMap.mul' S (B ⊗[R] A) ∘ₗ
            LinearMap.lTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul))
        x)
      y =
    (LinearMap.mul' S B) ((LinearMap.lTensor B (antipode S)) (comul x)) ⊗ₜ[R]
      (LinearMap.mul' R A) ((LinearMap.lTensor A (antipode R)) (comul y))
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ fst A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      fst A A

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ snd A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      snd A A

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ snd (A ⊗ A) A =
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ snd (A ⊗ A) A

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ fst A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      fst A A
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case hba
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b

pp: case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b

Tactic:
·

Goal state after:
case hba
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ snd A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      snd A A

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ snd (A ⊗ A) A =
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ snd (A ⊗ A) A

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ snd A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      snd A A
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b

Tactic:
·

Goal state after:
case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ snd (A ⊗ A) A =
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ snd (A ⊗ A) A

Tactic:
·

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ snd (A ⊗ A) A =
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ snd (A ⊗ A) A
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 f.ofConv)).comp
        ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp (comulAlgHom R A)))

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)
⊢ toConv
      (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp
        ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp (comulAlgHom R A))) =
    1

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 f.ofConv)).comp
        ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp (comulAlgHom R A)))
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
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫
      (α_ x (𝟙_ C) ((ihom x).obj y)).inv ≫
        (x ◁ curry (ρ_ x).hom ≫ (ihom.ev x).app x) ▷ (ihom x).obj y ≫ (ihom.ev x).app y =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
← uncurry_eq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫
      (α_ x (𝟙_ C) ((ihom x).obj y)).inv ≫ uncurry (curry (ρ_ x).hom) ▷ (ihom x).obj y ≫ (ihom.ev x).app 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 ((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:
← uncurry_eq,

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 ≫
        uncurry
              (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 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 ◁
            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) ≫
          (ihom.ev x).app z

Tactic:
← uncurry_eq,

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) ≫
        uncurry
          (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))
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: head✝¹ head✝ : ℕ
tail✝ : List ℕ
x✝ : ℕ
⊢ head✝¹ + x✝ < head✝ + (head✝¹ + x✝ + 1)

Tactic:
by lia

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType β
a₂ : α
f₂ : β a₂ → WType β
h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)
⊢ mk a₁ f₁ = mk a₂ f₂

Tactic:
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)

Goal state after:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : (fun b ↦ elim γ fγ (f₁ b)) ≍ fun b ↦ elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂