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

Goal state before:
pp: case h_fst
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
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) ≫ fst (F.obj Y) (F.obj X) =
    (((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv) ≫ fst (F.obj Y) (F.obj X)

pp: case h_snd
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
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) ≫ snd (F.obj Y) (F.obj X) =
    (((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv) ≫ snd (F.obj Y) (F.obj X)

Tactic:
<;>

Goal state after:
case h_fst
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
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) ≫ fst (F.obj Y) (F.obj X) =
    (((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv) ≫ fst (F.obj Y) (F.obj X)

case h_snd
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : CartesianMonoidalCategory D
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) ≫ snd (F.obj Y) (F.obj X) =
    (((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv) ≫ snd (F.obj Y) (F.obj X)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G✝ : D ⥤ E
X✝ Y✝ Z : C
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ ((Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      fst (G.obj X) (G.obj Y) =
    ((Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      fst (G.obj X) (G.obj Y)

pp: case h_snd
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G✝ : D ⥤ E
X✝ Y✝ Z : C
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ ((Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      snd (G.obj X) (G.obj Y) =
    ((Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      snd (G.obj X) (G.obj Y)

Tactic:
<;>

Goal state after:
case h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G✝ : D ⥤ E
X✝ Y✝ Z : C
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ ((Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      fst (G.obj X) (G.obj Y) =
    ((Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      fst (G.obj X) (G.obj Y)

case h_snd
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G✝ : D ⥤ E
X✝ Y✝ Z : C
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ ((Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      snd (G.obj X) (G.obj Y) =
    ((Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv) ≫
      snd (G.obj X) (G.obj Y)
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
a : A
⊢ counit ((antipode R) a) = ∑ x ∈ (ℛ R a).index, counit ((antipode R) (counit ((ℛ R a).left x) • (ℛ R a).right x))

Tactic:
← map_sum,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit ((antipode R) a) = counit ((antipode R) (∑ x ∈ (ℛ R a).index, counit ((ℛ R a).left x) • (ℛ R a).right x))
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
f g h : A ⟶ B
⊢ f = lift (g ≫ ι) h ≫ μ → lift g f ≫ μ = h

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift g f ≫ μ = h → f = lift (g ≫ ι) 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
f g h : A ⟶ B
⊢ f = lift (g ≫ ι) h ≫ μ → lift g f ≫ μ = h

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift g f ≫ μ = h → f = lift (g ≫ ι) h ≫ μ
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
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ → lift f h ≫ μ = g

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift f h ≫ μ = g → f = lift g (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
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ → lift f h ≫ μ = g

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift f h ≫ μ = g → f = lift g (h ≫ ι) ≫ μ
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
⊢ toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
      toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) =
    1

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

Tactic:
<;>

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

case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
      toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R)) =
    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
c : C
⊢ (toConv (antipode R) * toConv id).ofConv c = (ofConv 1) c

Tactic:
(ℛ R c).convMul_apply

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:
(ℛ R c).convMul_apply

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.CategoryTheory.Monoidal.Grp

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

pp: case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ = lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ

Tactic:
<;>

Goal state after:
case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f ≫ μ ▷ B = lift (lift f (f ≫ ι)) f ≫ μ ▷ B

case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ = lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

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

pp: case h_snd
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ μ ▷ B) ≫ snd B B = (lift (lift f (f ≫ ι)) f ≫ μ ▷ B) ≫ snd B B

pp: case h₁.h_fst
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ fst B B =
    (lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ fst B B

pp: case h_snd
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ snd B B =
    (lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ snd B B

Tactic:
<;>

Goal state after:
case h₀.h_fst
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ μ ▷ B) ≫ fst B B = (lift (lift f (f ≫ ι)) f ≫ μ ▷ B) ≫ fst B B

case h_snd
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ μ ▷ B) ≫ snd B B = (lift (lift f (f ≫ ι)) f ≫ μ ▷ B) ≫ snd B B

case h₁.h_fst
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ fst B B =
    (lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ fst B B

case h_snd
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ (lift (lift f (ι ≫ f)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ snd B B =
    (lift (lift f (f ≫ ι)) f ≫ (α_ B B B).hom ≫ B ◁ μ) ≫ snd B B
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case ha
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)
x✝ : A
⊢ (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp includeLeft) x✝ =
    ((f.ofConv.comp (lmul' R)).comp includeLeft) x✝

pp: case hb
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)
x✝ : A
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (f.ofConv.comp (lmul' R))).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
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)
x✝ : A
⊢ (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp includeLeft) x✝ =
    ((f.ofConv.comp (lmul' R)).comp includeLeft) x✝

case hb
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)
x✝ : A
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (f.ofConv.comp (lmul' R))).comp includeRight) x✝
Module: Mathlib.CategoryTheory.Monoidal.Grp

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
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ η ≫ e.hom = η

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
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ μ ≫ e.hom = (e.hom ⊗ₘ e.hom) ≫ μ

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
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ η ≫ e.hom = η

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
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ μ ≫ e.hom = (e.hom ⊗ₘ e.hom) ≫ μ
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
f : X ⟶ Y
⊢ X ◁ curry' f ≫ (ihom.ev X).app Y = (ρ_ X).hom ≫ f

Tactic:
dsimp [curry']
  simp only [whiskerLeft_curry_ihom_ev_app]

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

Goal state before:
pp: case zero.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0
⊢ 0 = 0

pp: case zero.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ 0 = m + 1

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0
⊢ 0 = 0

case zero.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ 0 = m + 1
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = Y ◁ η_ X Y ≫ (α_ Y X Y).inv ≫ ε_ X Y ▷ Y

pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢  ⊗𝟙.hom = (ρ_ Y).hom ≫ (λ_ Y).inv

Tactic:
<;>

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = Y ◁ η_ X Y ≫ (α_ Y X Y).inv ≫ ε_ X Y ▷ Y

case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢  ⊗𝟙.hom = (ρ_ Y).hom ≫ (λ_ Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = η_ X Y ▷ X ≫ (α_ X Y X).hom ≫ X ◁ ε_ X Y

pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢  ⊗𝟙.hom = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
<;>

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = η_ X Y ▷ X ≫ (α_ X Y X).hom ≫ X ◁ ε_ X Y

case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢  ⊗𝟙.hom = (λ_ X).hom ≫ (ρ_ X).inv
Module: Mathlib.SetTheory.Cardinal.Subfield

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

Tactic:
rw [← Set.range_eq_univ]

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 convert_3.inl.«0»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨0, ⋯⟩)))

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

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

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

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

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

Tactic:
<;>

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

case convert_3.inl.«1»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨1, ⋯⟩)))

case convert_3.inl.«2»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨2, ⋯⟩)))

case convert_3.inl.«3»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨3, ⋯⟩)))

case convert_3.inl.«4»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨4, ⋯⟩)))

case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨5, ⋯⟩)))
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
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, f ((b.coord x) m • b x) = f m

Tactic:
← map_sum,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ f (∑ x, (b.coord x) m • b x) = f m
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case h₁
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)

pp: case h₂
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{v, u} (Module.rank R ↥f'.ker) ≤ lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
<;>

Goal state after:
case h₁
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)

case h₂
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{v, u} (Module.rank R ↥f'.ker) ≤ lift.{v, u} (Module.rank R ↥f.ker)