mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.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✝⁸ : 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
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) ((LinearMap.rTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.lid R B) ((LinearMap.rTensor B counit) (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✝⁸ : 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
⊢ ((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B)) 1)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) (1 ⊗ₜ[S] x) ⊗ₜ[R] (TensorProduct.lid R B) (1 ⊗ₜ[R] y))

Tactic:
· dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      apply (TensorProduct.lid S _).injective
      dsimp
      rw [tmul_smul, smul_assoc, one_smul, smul_tmul']

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✝⁸ : 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
⊢ ((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B)) 1)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) (1 ⊗ₜ[S] x) ⊗ₜ[R] (TensorProduct.lid R B) (1 ⊗ₜ[R] y))
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (BialgCat R) (AlgCat R)).map (x✝³ ◁ x✝) =
    (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

Tactic:
ext; 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
⊢ (forget₂ (BialgCat R) (AlgCat R)).map (x✝¹ ▷ x✝) =
    (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

Tactic:
ext; 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₂✝
⊢ (forget₂ (BialgCat R) (AlgCat R)).map (x✝¹ ⊗ₘ x✝) =
    (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

Tactic:
ext; 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
⊢ ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom)).comp
          Algebra.TensorProduct.includeLeft).comp
      Algebra.TensorProduct.includeLeft =
    ((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

Tactic:
ext; 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
⊢ (AlgHom.restrictScalars R
          ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom)).comp
            Algebra.TensorProduct.includeLeft)).comp
      Algebra.TensorProduct.includeRight =
    (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

Tactic:
ext; 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
⊢ (AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom))).comp
      Algebra.TensorProduct.includeRight =
    (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

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : BialgCat R
⊢ (AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (λ_ x✝).hom))).comp
      Algebra.TensorProduct.includeRight =
    (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

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : BialgCat R
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (ρ_ x✝).hom)).comp Algebra.TensorProduct.includeLeft =
    (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

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹ = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ α ∘ₗ ρ⁻¹ = LinearMap.id ⊗ₘ ρ⁻¹

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ α ∘ₗ λ⁻¹ ⊗ₘ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ α ∘ₗ ρ⁻¹ ⊗ₘ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹)

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ λ⁻¹ ∘ₗ f = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ρ⁻¹ ∘ₗ f = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ β ∘ₗ f ⊗ₘ g = g ⊗ₘ f ∘ₗ β

Tactic:
ext; rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (Δ ≫ Δ ▷ A.X).op = (α_ A.X A.X A.X).inv.op ≫ (Δ ≫ A.X ◁ Δ).op

Tactic:
comul_assoc_flip,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (Δ ≫ A.X ◁ Δ ≫ (α_ A.X A.X A.X).inv).op = (α_ A.X A.X A.X).inv.op ≫ (Δ ≫ A.X ◁ Δ).op
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R N)))).X)).compr₂ₛₗ
      ((TensorProduct.mk R
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N)))).X)
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R P)))).X)).compr₂ₛₗ
        (α_ (of R M) (of R N) (of R P)).hom.toCoalgHom'.toLinearMap) =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R N)))).X)).compr₂ₛₗ
      ((TensorProduct.mk R
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N)))).X)
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R P)))).X)).compr₂ₛₗ
        ↑(TensorProduct.assoc R M N P))

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
      (λ_ (of R M)).hom.toCoalgHom'.toLinearMap =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
      ↑(TensorProduct.lid R M)

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
      (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
      ↑(TensorProduct.rid R M)

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
obtain ⟨⟨a, ⟨-, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers x) z
  use n, a
  simpa using h

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
obtain ⟨n, hn⟩ := exists_of_eq r hab
    use n
    rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (PullbackCone.mk h k ⋯)
⊢ IsLimit (BinaryFan.mk h k)

Tactic:
by
  apply isBinaryProductOfIsTerminalIsPullback _ _ H₁
  exact H₂

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), 1 * a = a

Tactic:
rintro ⟨a, s⟩
      with_unfolding_all exact mk_eq.mpr ⟨1, by simp only [one_mul, mul_one, one_smul]⟩

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ -1 = f (-1)

Tactic:
f.map_neg,

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ -1 = -f 1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x✝ : FreeCommRing α
hx : x✝.IsSupported s
x y : FreeCommRing α
q : ℤ
hq : (lift fun a ↦ if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : (lift fun a ↦ if a ∈ s then 0 else X) y = ↑r
⊢ ↑q + (lift fun a ↦ if a ∈ s then 0 else X) y = ↑(q + r)

Tactic:
hr

Goal state after:
case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x✝ : FreeCommRing α
hx : x✝.IsSupported s
x y : FreeCommRing α
q : ℤ
hq : (lift fun a ↦ if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : (lift fun a ↦ if a ∈ s then 0 else X) y = ↑r
⊢ ↑q + ↑r = ↑(q + r)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case add
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x + ↑y

Tactic:
exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : r • x = 0
⊢ x = 0

Tactic:
rw [smul_eq_iff_of_mem (hr := hr)] at hx

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : x = Localization.mk 1 ⟨r, hr⟩ • 0
⊢ x = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
x y : LocalizedModule S M
⊢ (x + y).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    x.liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + y.liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
by
    refine x.induction_on₂ ?_ y
    intro m₁ m₂ t₁ t₂
    simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left s]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
⊢ IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X)

Tactic:
refine ⟨fun _ ↦ ⟨section_ (T.ε.app X), ?_, by simp⟩, fun _ ↦ inferInstance⟩
  rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]

Goal state after: