mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ Small.{v, max v w} ↑(G ⋙ forget C).sections

Tactic:
← Types.hasLimit_iff_small_sections

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ HasLimit (G ⋙ forget C)
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget GrpCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget GrpCat).map f)) (a⁻¹ j) = a⁻¹ j'

Tactic:
by
      simp only [Functor.comp_map, Pi.inv_apply]
      dsimp [Functor.sections] at ah ⊢
      rw [(F.map f).hom.map_inv (a j), ah f]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ GrpCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
this✝¹ : (forget₂ GrpCat MonCat).ReflectsIsomorphisms := reflectsIsomorphisms_forget₂ GrpCat MonCat
c' : Cone (F ⋙ forget₂ GrpCat MonCat)
t : IsLimit c'
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
⊢ (forget₂ GrpCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget GrpCat)).pt,
        π := { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ GrpCat MonCat) j), naturality := ⋯ } } ≅
    c'

Tactic:
apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit.{v, u} _) t

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y = Z
⊢ X ◁ eqToHom f = eqToHom ⋯

Tactic:
by
  cases f
  simp only [whiskerLeft_id, eqToHom_refl]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
    e.inverse.map (X ◁ f) =
      (e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y₁)).inv ≫
        e.inverse.obj X ◁ e.inverse.map f ≫ (e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y₂)).hom

Tactic:
simp +zetaDelta +instances

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D),
    e.inverse.map (f ▷ Y) =
      (e.unitIso.app (e.inverse.obj X₁ ⊗ e.inverse.obj Y)).inv ≫
        e.inverse.map f ▷ e.inverse.obj Y ≫ (e.unitIso.app (e.inverse.obj X₂ ⊗ e.inverse.obj Y)).hom

Tactic:
simp +zetaDelta +instances

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    e.inverse.map (f ⊗ₘ g) =
      (e.unitIso.app (e.inverse.obj X₁ ⊗ e.inverse.obj X₂)).inv ≫
        (e.inverse.map f ⊗ₘ e.inverse.map g) ≫ (e.unitIso.app (e.inverse.obj Y₁ ⊗ e.inverse.obj Y₂)).hom

Tactic:
simp +zetaDelta +instances

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X Y Z : D),
    e.inverse.map (α_ X Y Z).hom =
      (((e.unitIso.app (e.inverse.obj (X ⊗ Y) ⊗ e.inverse.obj Z)).symm ≪≫
            ((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y)).symm ⊗ᵢ Iso.refl (e.inverse.obj Z))) ≪≫
          α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ e.unitIso.app (e.inverse.obj Y ⊗ e.inverse.obj Z)) ≪≫
              e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj (Y ⊗ Z))).hom

Tactic:
simp +zetaDelta +instances

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D),
    e.inverse.map (λ_ X).hom =
      (((e.unitIso.app (e.inverse.obj (𝟙_ D) ⊗ e.inverse.obj X)).symm ≪≫
            ((e.unitIso.app (𝟙_ C)).symm ⊗ᵢ Iso.refl (e.inverse.obj X))) ≪≫
          λ_ (e.inverse.obj X)).hom

Tactic:
simp +zetaDelta +instances

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D),
    e.inverse.map (ρ_ X).hom =
      (((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj (𝟙_ D))).symm ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ (e.unitIso.app (𝟙_ C)).symm)) ≪≫
          ρ_ (e.inverse.obj X)).hom

Tactic:
simp +zetaDelta +instances

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
⊢ ∀ (w : ↑W) (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom
          (whiskerRight (associator W X Y).hom Z ≫
            (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro w

Goal state after:
R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
w : ↑W
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom
          (whiskerRight (associator W X Y).hom Z ≫
            (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
x✝ : HasLimitsOfShape J C
this : HasLimitsOfShape Jᵒᵖᵒᵖ C
⊢ HasColimitsOfShape Jᵒᵖ Cᵒᵖ

Tactic:
exact hasColimitsOfShape_op_of_hasLimitsOfShape

Goal state after:
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
⊢ adj.IsMonoidal

Tactic:
let := adj.leftAdjointOplaxMonoidal
  refine ⟨?_, fun X Y ↦ ?_⟩
  · simp [homEquiv_counit, leftAdjointOplaxMonoidal_η]
  · simp [homEquiv_counit, ← μ_natural, leftAdjointOplaxMonoidal_δ]

Goal state after:
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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ IsIso (LaxMonoidal.ε e.inverse)

Tactic:
simp only [this, Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]

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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ IsIso (e.toAdjunction.unit.app (𝟙_ C) ≫ e.inverse.map (OplaxMonoidal.η e.functor))
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 G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (β_ (G.obj X) (G.obj Y)).hom ≫ (i.inv.app Y ⊗ₘ i.inv.app X) ≫ μ F Y X ≫ i.hom.app (Y ⊗ X)

Tactic:
← braiding_naturality_assoc,

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 G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X ≫ i.hom.app (Y ⊗ X)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((Quot.ι F j) x) = (Hom.hom (s.ι.app j)) x

Tactic:
simp only [Quot.ι_desc, Functor.const_obj_obj]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
X : Type u₇
Y : Type u₈
Z : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
inst✝⁵ : Category.{v₄, u₄} D
inst✝⁴ : Category.{v₅, u₅} E
inst✝³ : Category.{v₆, u₆} F
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
G₁ : A ⥤ D
H₁ : B ⥤ E
K₁ : C ⥤ F
G₂ : D ⥤ X
H₂ : E ⥤ Y
K₂ : F ⥤ Z
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : B ⥤ C
R₂ : C ⥤ B
L₃ : D ⥤ E
R₃ : E ⥤ D
L₄ : E ⥤ F
R₄ : F ⥤ E
L₅ : X ⥤ Y
R₅ : Y ⥤ X
L₆ : Y ⥤ Z
R₆ : Z ⥤ Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
vcomp :
  (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    (mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (α ≫ᵥ β) ≫ᵥ (mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (γ ≫ᵥ δ)
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ

Tactic:
simp only [mateEquiv_hcomp] at vcomp

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
X : Type u₇
Y : Type u₈
Z : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
inst✝⁵ : Category.{v₄, u₄} D
inst✝⁴ : Category.{v₅, u₅} E
inst✝³ : Category.{v₆, u₆} F
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
G₁ : A ⥤ D
H₁ : B ⥤ E
K₁ : C ⥤ F
G₂ : D ⥤ X
H₂ : E ⥤ Y
K₂ : F ⥤ Z
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : B ⥤ C
R₂ : C ⥤ B
L₃ : D ⥤ E
R₃ : E ⥤ D
L₄ : E ⥤ F
R₄ : F ⥤ E
L₅ : X ⥤ Y
R₅ : Y ⥤ X
L₆ : Y ⥤ Z
R₆ : Z ⥤ Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
vcomp :
  (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
h : Mono x✝
⊢ Mono ((restrictScalars f).map x✝)

Tactic:
by rwa [mono_iff_injective] at h ⊢

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

Goal state before:
pp: case e'_2.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
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₁ • counit x₁ • x₂ ⊗ₜ[R] y₂ = counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂

Tactic:
smul_tmul'

Goal state after:
case e'_2.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
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂ = counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.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
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₂ • counit x₂ • x₁ ⊗ₜ[R] y₁ = counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁

Tactic:
smul_tmul'

Goal state after:
case e'_2.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
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁ = counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (a \ b) ≤ c ↔ f a \ f b ≤ c

Tactic:
simp only [← le_map_inv_iff, sdiff_le_iff]
        rw [← OrderIsoClass.map_le_map_iff f]
        simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (a \ b) ≤ c ↔ f a \ f b ≤ c

Tactic:
simp only [← le_map_inv_iff, sdiff_le_iff]
        rw [← OrderIsoClass.map_le_map_iff f]
        simp

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✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
symmDiff,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a \ b ⊔ b \ a) = f a \ f b ⊔ f b \ f a
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
N' : Type u_7
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'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
h : P →ₗ[R] M ⊗[R] N
⊢ β ∘ₗ f ⊗ₘ g ∘ₗ h = g ⊗ₘ f ∘ₗ β ∘ₗ h

Tactic:
by
  simp only [← LinearMap.comp_assoc, symm_comp_map]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Tactic:
trans z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ) ↔
    z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ sInf {m | IsCoatom m}
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Tactic:
sInf_eq_iInf'

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ ⨅ a, ↑a
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)
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
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ (algebraMap R S) e = 1

Tactic:
rw [← (algebraMap R S).map_one, H, mul_one, he]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Function.Bijective ⇑f
⊢ f.ker ≤ jacobson R M

Tactic:
simp_rw [LinearMap.ker_eq_bot.mpr hf.1, bot_le]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ Module.jacobson R R = sInf {I | I.IsMaximal}

Tactic:
Module.jacobson,

Goal state after:
R : Type u_1
inst✝ : Ring R
⊢ sInf {m | IsCoatom m} = sInf {I | I.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

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

Tactic:
Module.jacobson,

Goal state after:
R : Type u
inst✝ : Ring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsMaximal} = sInf {m | IsCoatom m}
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

pp: case inr
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✝ : Nonempty ι
⊢ ∃ w, LinearIndependent R w

Tactic:
· exact ⟨isEmptyElim, linearIndependent_empty_type⟩

Goal state after:
case inr
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✝ : Nonempty ι
⊢ ∃ w, LinearIndependent R w
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 : Mon C
f : trivial C ⟶ A
⊢ f = { hom := η, isMonHom_hom := ⋯ }

Tactic:
ext
    rw [← Category.id_comp f.hom]
    dsimp only [trivial_X]
    rw [← trivial_mon_one, IsMonHom.one_hom]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ ∀ (j : Discrete WalkingPair),
    c.π.app j =
      (Iso.refl c.pt).hom ≫
        (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app j

Tactic:
by
            rintro ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ ∀ (j : Discrete WalkingPair),
    c.ι.app j ≫ (Iso.refl c.pt).hom =
      (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app j

Tactic:
by
            rintro ⟨⟨⟩⟩ <;> simp

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'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s))

Tactic:
mul_comm _ s,

Goal state after:
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
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)) = mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂))
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : G
⊢ toUnits x ∈ H.units ↔ x ∈ H

Tactic:
simp_rw [mem_units_iff_val_mem, val_toUnits_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
f : M →ₗ[R] M'
e : M' →ₗ[R] M''
he : Function.Bijective ⇑e
⊢ IsLocalizedModule S (e ∘ₗ f) ↔ IsLocalizedModule S f

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ .of_linearEquiv _ _ (.ofBijective _ he)⟩
  have : (LinearEquiv.ofBijective _ he).symm.toLinearMap ∘ₗ e ∘ₗ f = f := by ext; simp
  rw [← this]
  exact .of_linearEquiv _ _ _

Goal state after: