mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ Z✝ : ModuleCat R
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑(CoextendScalars.obj' f X✝)
⊢ (Hom.hom (CoextendScalars.map' f (x✝² ≫ x✝¹))) x✝ =
    (Hom.hom (CoextendScalars.map' f x✝² ≫ CoextendScalars.map' f x✝¹)) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : ↑Y
r : R
s : S
⊢ (ConcreteCategory.hom g) ((r • s) • y) = (Hom.hom g) ((RingHom.id R) r • s • y)

Tactic:
simp [ModuleCat.restrictScalars.smul_def (M := ModuleCat.of S S), mul_smul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y : ModuleCat S
y : ↑Y
r : R
s : S
⊢ (r • s) • y = (RingHom.id R) r • s • y

Tactic:
simp [ModuleCat.restrictScalars.smul_def (M := ModuleCat.of S S), mul_smul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : ↑X
x : S
⊢ (ConcreteCategory.hom g) (x ⊗ₜ[R] s) = (Hom.hom g) (x ⊗ₜ[R] s)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x : ↑X
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f) g)) x =
    (ConcreteCategory.hom g) ((Hom.hom ((ExtendRestrictScalarsAdj.unit f).app X)) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app ((extendScalars f₁₂).obj M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))).inv =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))).inv

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        ((extendRestrictScalarsAdj f₁₂).unit.app M ≫
          (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
            (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))))
      m =
    1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
x₁ x₂ : A
y₁ y₂ : B
x₁₁ x₁₂ : A
y₁₁ y₁₂ : B
⊢ (TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B))
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[R] (y₁₁ ⊗ₜ[R] y₁₂)) ⊗ₜ[S]
        (x₂ ⊗ₜ[R] y₂)) =
    F
      ((TensorProduct.assoc S A A A) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[S] x₂) ⊗ₜ[R]
        (TensorProduct.assoc R B B B) (y₁₁ ⊗ₜ[R] y₁₂ ⊗ₜ[R] y₂))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = 1 ⊗ₜ[R₁] m

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_3.tmul.tmul.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
x₁ x₂ : A
y₁ y₂ : B
x₂₁ x₂₂ : A
y₂₁ y₂₂ : B
⊢ x₁ ⊗ₜ[R] y₁ ⊗ₜ[S] (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₂₁ ⊗ₜ[S] x₂₂ ⊗ₜ[R] (y₂₁ ⊗ₜ[R] y₂₂)) =
    F (x₁ ⊗ₜ[S] (x₂₁ ⊗ₜ[S] x₂₂) ⊗ₜ[R] (y₁ ⊗ₜ[R] (y₂₁ ⊗ₜ[R] y₂₂)))

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.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✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul)) x) y =
    F ((LinearMap.lTensor A comul) (comul x) ⊗ₜ[R] (LinearMap.lTensor B comul) (comul y))

Tactic:
· dsimp
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    dsimp
    hopf_tensor_induction comul (R := S) x₂ with x₂₁ x₂₂
    hopf_tensor_induction comul (R := R) y₂ with y₂₁ y₂₂
    rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : BialgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (x✝⁴ ⊗ x✝³))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝³)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ◁ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).hom))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : BialgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : BialgCat R
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ x✝¹))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).map x✝² ▷ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₂✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ X₂✝))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (BialgCat R) (AlgCat R)).map x✝² ⊗ₘ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹) ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj Y₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj Y₂✝)).hom))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝³.carrier
⊢ (((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom)).comp
            Algebra.TensorProduct.includeLeft).comp
        Algebra.TensorProduct.includeLeft)
      x✝ =
    (((AlgCat.Hom.hom
                (((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                      ((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                        Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                    α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                      (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom).comp
            Algebra.TensorProduct.includeLeft).comp
        Algebra.TensorProduct.includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝².carrier
⊢ ((AlgHom.restrictScalars R
            ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom)).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgCat.Hom.hom
                  (((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                        ((Iso.refl
                              ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                                (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                          Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                      α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                        (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                            Iso.refl
                              ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                                (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                      Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                  α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                      Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (λ_ x✝¹).hom))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (AlgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (ρ_ x✝¹).hom)).comp Algebra.TensorProduct.includeLeft) x✝ =
    ((AlgCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ⊗
                        (forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)))).symm ≪≫
                  (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (AlgCat R))).symm)) ≪≫
                ρ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom).comp
        Algebra.TensorProduct.includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
    (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x =
    ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X✝ Y✝ Z✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ⇑(ConcreteCategory.hom (x✝¹ ≫ x✝)) = ⇑(ConcreteCategory.hom x✝) ∘ ⇑(ConcreteCategory.hom x✝¹)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case none
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case some
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
val✝ : X'✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false * 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true * 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case some
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case some
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

Tactic:
rfl

Goal state after: