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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ f ⊗ₘ ∑ j ∈ s, g j = ∑ j ∈ s, f ⊗ₘ g j

Tactic:
simp only [tensorHom_def, whiskerLeft_sum, Preadditive.comp_sum]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝ =
    (∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝

Tactic:
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.uniqueUpToIso ((tensorLeft X).obj ∘ f) (isBilimitOfPreserves (tensorLeft X) (biproduct.isBilimit f))).hom ≫
      biproduct.π (fun j ↦ X ⊗ f j) j✝ =
    (∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ (leftDistributor X f).inv =
    biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ ∑ j, biproduct.π (fun j ↦ X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ biproduct.desc fun j ↦ X ◁ biproduct.ι f j) =
    biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ ∑ j, biproduct.π (fun j ↦ X ⊗ f j) j ≫ X ◁ biproduct.ι f j
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a : F.Monoidal
⊢ ∀ ⦃a₂ : F.Monoidal⦄, a.toLaxMonoidal = a₂.toLaxMonoidal → a = a₂

Tactic:
b

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
⊢ a.toLaxMonoidal = b.toLaxMonoidal → a = b
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a : F.Monoidal
⊢ ∀ ⦃a₂ : F.Monoidal⦄, a.toOplaxMonoidal = a₂.toOplaxMonoidal → a = a₂

Tactic:
b

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
⊢ a.toOplaxMonoidal = b.toOplaxMonoidal → a = b
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj X✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj X✝) (F.obj x✝)) ≫
      F.map x✝¹ ▷ F.obj x✝ =
    F.map (x✝¹ ▷ x✝) ≫
      (adj.homEquiv (Y✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm, assoc, ← μ_natural_left]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      ((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ G.map (F.map x✝¹) ▷ G.obj (F.obj x✝) ≫ μ G (F.obj Y✝) (F.obj x✝)) =
    (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      (x✝¹ ▷ x✝ ≫ (adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
⊢ (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ G.map (F.map (β_ X Y).hom) =
    (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ μ G (F.obj Y) (F.obj X) ≫ G.map (μ F Y X)

Tactic:
slice_lhs 2 3 =>
      rw [← CategoryTheory.Functor.map_comp, braided, CategoryTheory.Functor.map_comp]

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
⊢ μ G (F.obj X) (F.obj Y) ≫ G.map (β_ (F.obj X) (F.obj Y)).hom ≫ G.map (μ F Y X) =
    (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ μ G (F.obj Y) (F.obj X) ≫ G.map (μ F Y X)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ (((((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ V₁ V₂).inv)) ≫
          (𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂)) ≫
        (𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom)) ≫
      (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        (𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫
          (𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

Tactic:
slice_lhs 2 3 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ (α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
      ((((𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂)) ≫
          (𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom)) ≫
        (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        (𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫
          (𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ g = (lift R) f

Tactic:
rw [← (lift R).symm_apply_eq]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ (lift R).symm g = f
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0

Tactic:
op_smul_op_smul,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ r •> x.snd + -(r •> x.snd <• (r * x.fst)) = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ -(x.snd <• r) + x.snd <• r = 0

Tactic:
neg_add_cancel

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
⊢ Function.LeftInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
⊢ Function.RightInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.fst •> b.snd <• (b.fst⁻¹ * a.fst⁻¹) +
        (b.fst⁻¹ * a.fst⁻¹) •> a.snd <• b.fst <• (b.fst⁻¹ * a.fst⁻¹)) =
    -(b.fst⁻¹ •> a.fst⁻¹ •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹ <• a.fst⁻¹)

Tactic:
op_smul_op_smul,

Goal state after:
case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.fst •> b.snd <• (b.fst⁻¹ * a.fst⁻¹) +
        (b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) =
    -(b.fst⁻¹ •> a.fst⁻¹ •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ↑(TensorProduct.assoc R B B B) ∘ₗ LinearMap.rTensor B comul ∘ₗ comul = LinearMap.lTensor B comul ∘ₗ comul

Tactic:
by
    simp only [← ((f : A ≃ₗ[R] B).comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul,
      ← LinearMap.comp_assoc]
    congr 1
    ext x
    simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp,
      LinearEquiv.coe_coe, Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul,
      LinearMap.coe_coe, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
      symm_apply_apply, LinearMap.lTensor_comp_map, TensorProduct.sum_tmul,
      TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using (sum_map_tmul_tmul_eq f f f x).symm

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = ⇑f
⊢ ∀ (x y : A), ((↑f).copy f' h).toFun (x * y) = ((↑f).copy f' h).toFun x * ((↑f).copy f' h).toFun y

Tactic:
by intros; simp_all

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

Goal state before:
pp: 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
⊢ ↑(TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ LinearMap.rTensor (A ⊗[R] B) comul ∘ₗ comul =
    LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul

Tactic:
ext x y
  let 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 _ _ _ _ _ _ _ _ ≪≫ₗ
      AlgebraTensorModule.congr (.refl _ _)
        (AlgebraTensorModule.tensorTensorTensorComm _ _ _ _ _ _ _ _)
  let F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S]
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
    TensorProduct.mapOfCompatibleSMul .. ∘ₗ
        TensorProduct.map .id (TensorProduct.mapOfCompatibleSMul ..) ∘ₗ F.toLinearMap
  convert! congr(F ($(Coalgebra.coassoc_apply x) ⊗ₜ[R] $(Coalgebra.coassoc_apply y))) using 1
  · 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
  · 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.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ f aᶜ = (f a)ᶜ

Tactic:
rw [← himp_bot, ← himp_bot, map_himp, map_bot]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_symm_eq]
  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
P : Type u_5
M' : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

Tactic:
by
  simp_rw [← LinearMap.comp_assoc, ← assoc_symm_comp_map_rid_symm]

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✝ B✝ : Comon C
f : A✝ ⟶ B✝
e : IsIso ((forget C).map f)
⊢ f ≫ { hom := inv f.hom, isComonHom_hom := ⋯ } = 𝟙 A✝ ∧ { hom := inv f.hom, isComonHom_hom := ⋯ } ≫ f = 𝟙 B✝

Tactic:
by cat_disch

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
M N : Comon C
f : M.X ≅ N.X
f_counit : f.hom ≫ ε = ε
f_comul : f.hom ≫ Δ = Δ ≫ (f.hom ⊗ₘ f.hom)
this : IsComonHom f.hom
⊢ { hom := f.hom, isComonHom_hom := this } ≫ { hom := f.inv, isComonHom_hom := ⋯ } = 𝟙 M

Tactic:
by cat_disch

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
M N : Comon C
f : M.X ≅ N.X
f_counit : f.hom ≫ ε = ε
f_comul : f.hom ≫ Δ = Δ ≫ (f.hom ⊗ₘ f.hom)
this : IsComonHom f.hom
⊢ { hom := f.inv, isComonHom_hom := ⋯ } ≫ { hom := f.hom, isComonHom_hom := this } = 𝟙 N

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: x✝¹ : Type u
x✝ : CommRingCat
⊢ Function.RightInverse (fun f ↦ ofHom (homEquiv.symm ⇑(ConcreteCategory.hom f))) fun f ↦ ↾homEquiv (Hom.hom f)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsMaximal} = Ring.jacobson R

Tactic:
Ring.jacobson,

Goal state after:
R : Type u
inst✝ : Ring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsMaximal} = Module.jacobson R R
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (f 1 - f a)

Tactic:
← f.map_sub

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (f (1 - a))
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ (↑a * ↑b) ^
        (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
          N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
      ((↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ * (r a * ↑b ^ N)) =
    (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r b * ↑a ^ N)

Tactic:
hN',

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ (↑a * ↑b) ^
        (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
          N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
      ((↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)) =
    (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r b * ↑a ^ N)
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
⊢ Ideal.map f (maximalIdeal R) ≤ maximalIdeal S

Tactic:
rw [Ideal.map_le_iff_le_comap, IsLocalRing.maximalIdeal_comap]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a : S
⊢ ∀ (b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b

Tactic:
b

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : S
⊢ IsUnit (a + b) → IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
cases nonempty_fintype ι
  obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f
  exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : LinearIndependent R v
h✝ : IsEmpty ι
⊢ ∃ w, LinearIndependent R w

Tactic:
exact ⟨isEmptyElim, linearIndependent_empty_type⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A✝ B✝ : Mon C
f : A✝ ⟶ B✝
e : IsIso ((forget C).map f)
⊢ f ≫ Hom.mk' (inv f.hom) ⋯ ⋯ = 𝟙 A✝ ∧ Hom.mk' (inv f.hom) ⋯ ⋯ ≫ f = 𝟙 B✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : Mono g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P), m ≫ fst = s.fst → m ≫ snd = s.snd → m = s.fst ≫ inv fst

Tactic:
by cat_disch

Goal state after: