mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : uncurry.obj F₁ = uncurry.obj F₂
⊢ F₁ = F₂

Tactic:
← curry_obj_uncurry_obj F₁,

Goal state after:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : uncurry.obj F₁ = uncurry.obj F₂
⊢ curry.obj (uncurry.obj F₁) = F₂
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
X : C
t : (const J).obj X ⟶ F
⊢ t.app ∈ (F ⋙ coyoneda.obj (op X)).sections

Tactic:
simp [Functor.sections, ← t.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
s : P.obj (op X)
Y : C
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (op Y))) (shrinkYonedaObjObjEquiv.symm f) =
    (ConcreteCategory.hom (P.map f.op)) s

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaEquiv.surjective s
  simp [map_shrinkYonedaEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
⊢ uliftCoyoneda.{w', v, u}.map g ≫
      (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
      shrinkCoyoneda.{max w' v, v, u}.map g

Tactic:
ext
      exact (shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm _ _).symm

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ⟨(ConcreteCategory.hom (kernel.ι f)) 0, ⋯⟩ = 0

Tactic:
refine Subtype.ext ?_

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ↑⟨(ConcreteCategory.hom (kernel.ι f)) 0, ⋯⟩ = ↑0
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
g g' : ↑(limit.cone (parallelPair f 0)).1
⊢ ⟨(ConcreteCategory.hom (kernel.ι f)) (g + g'), ⋯⟩ =
    ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩ + ⟨(ConcreteCategory.hom (kernel.ι f)) g', ⋯⟩

Tactic:
refine Subtype.ext ?_

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
g g' : ↑(limit.cone (parallelPair f 0)).1
⊢ ↑⟨(ConcreteCategory.hom (kernel.ι f)) (g + g'), ⋯⟩ =
    ↑(⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩ + ⟨(ConcreteCategory.hom (kernel.ι f)) g', ⋯⟩)
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x : ↑G
mem : x ∈ (Hom.hom f).ker
⊢ (ConcreteCategory.hom
        (kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ ≫
          ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }))
      ⟨x, mem⟩ =
    (ConcreteCategory.hom (𝟙 (of ↥(Hom.hom f).ker))) ⟨x, mem⟩

Tactic:
refine Subtype.ext ?_

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x : ↑G
mem : x ∈ (Hom.hom f).ker
⊢ ↑((ConcreteCategory.hom
          (kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ ≫
            ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }))
        ⟨x, mem⟩) =
    ↑((ConcreteCategory.hom (𝟙 (of ↥(Hom.hom f).ker))) ⟨x, mem⟩)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : V ⟶ W
⊢ (f ⊗ₘ h) ≫ g ▷ W = f ≫ g ⊗ₘ h

Tactic:
simp [tensorHom_def, whisker_exchange]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst✝¹ : IsIso f
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (f ⊗ₘ g) = inv f ⊗ₘ inv g

Tactic:
simp [tensorHom_def, whisker_exchange]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ₘ g ⊗ₘ h = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X' Y' Z').hom

Tactic:
by
  rw [associator_naturality, inv_hom_id_assoc]

Goal state after:
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
F : Jᵒᵖ ⥤ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeRightOp c).ι.app j ≫ m = s.ι.app j
j : J
⊢ (m.op ≫ c.π.app j).unop = ((hc.lift (coneRightOpOfCocone s)).unop.op ≫ c.π.app j).unop

Tactic:
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using! w (op j)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)

Tactic:
apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit ((Cocone.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W' f✝

Tactic:
induction hf with
    | of _ hf => exact h _ hf
    | id x => exact W'.id_mem _
    | comp_of _ _ _ hg hf => exact W'.comp_mem _ _ hf (h _ hg)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      (β_ (F.obj X✝) (F.obj Y✝ ⊗ F.obj Z✝)).hom ≫
        (α_ (F.obj Y✝) (F.obj Z✝) (F.obj X✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝) =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝)

Tactic:
hexagon_forward_assoc

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝) =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom =
    AddEquiv.ulift.symm.toAddMonoidHom.comp (desc F c)

Tactic:
refine Quot.addMonoidHom_ext _ (fun j a ↦ ?_)

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ ((desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom) ((ι F j) a) =
    (AddEquiv.ulift.symm.toAddMonoidHom.comp (desc F c)) ((ι F j) a)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ (c.comapQuotientEquivRangeS f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x

Tactic:
simp [RingEquiv.symm_apply_eq]

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

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ x.fst •> xs.prod.snd + x.snd <• xs.prod.fst =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
fst_list_prod,

Goal state after:
case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ x.fst •> xs.prod.snd + x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    (List.map
        (fun x_1 ↦
          (List.take x_1.2 (List.map fst (x :: xs))).prod •> x_1.1.snd <•
            (List.drop x_1.2.succ (List.map fst (x :: xs))).prod)
        (x :: xs).zipIdx).sum

Tactic:
| cons x xs ih =>

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

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
rw [comp_assoc, snd_comp_inl, comp_zero, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, snd_comp_inl, TensorProduct.map_zero_left, zero_comp]

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
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ _root_.TensorProduct.map (AlgebraTensorModule.map f.toLinearMap g.toLinearMap)
        (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) ∘ₗ
      comul =
    comul ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap

Tactic:
by
    ext x y
    dsimp
    simp only [← CoalgHomClass.map_comp_comul_apply]
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    simp

Goal state after:
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: X : Preord
⊢ PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization =
    𝟙 { carrier := Antisymmetrization ↑X fun x1 x2 ↦ x1 ≤ x2, str := instPartialOrderAntisymmetrization }

Tactic:
ext x
    induction x using Quotient.inductionOn'
    exact Quotient.map'_mk'' _ (fun a b ↦ id) _

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

Goal state before:
pp: R : CommRingCat
S : Under R
⊢ (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).obj S).hom ≫
      ofHom
        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯) =
    ((𝟭 (Under R)).obj S).hom

Tactic:
by ext; simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a b : α
ha : ¬IsUnit a
hb : b ≠ 0
⊢ FiniteMultiplicity a b

Tactic:
obtain ⟨n, c, ndvd, rfl⟩ := WfDvdMonoid.max_power_factor' hb ha

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ FiniteMultiplicity a (a ^ n * c)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single 1 r✝)

Tactic:
simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w]

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

Goal state before:
pp: case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
m✝ : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single m✝ 1)

Tactic:
simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ count p (normalizedFactors x) = n

Tactic:
apply Nat.cast_injective (R := ℕ∞)

Goal state after:
case neg
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ ↑(count p (normalizedFactors x)) = ↑n
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₂
| comap f (jacobson R₂ M₂)

Tactic:
jacobson,

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₂
| comap f (sInf {m | IsCoatom m})
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 ≤ jacobson R M
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Tactic:
jacobson,

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 ≤ sInf {m | IsCoatom m}
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)
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 ≤ ⨅ a, ↑a
| map f (jacobson R M)

Tactic:
jacobson,

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
| map f (sInf {m | IsCoatom m})
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ jacobson R ((i : ι) → M i) ≤ ⨅ i, comap (LinearMap.proj i) (jacobson R (M i))

Tactic:
jacobson,

Goal state after:
R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ sInf {m | IsCoatom m} ≤ ⨅ i, comap (LinearMap.proj i) (sInf {m | IsCoatom m})
Module: Mathlib.RingTheory.Jacobson.Radical

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

Tactic:
jacobson,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

Tactic:
jacobson,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(Module.jacobson (R ⧸ I) (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ⊥.jacobson = Ring.jacobson R

Tactic:
jacobson,

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ I.jacobson
⊢ x ∈ J.jacobson

Tactic:
jacobson,

Goal state after:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ sInf {J | I ≤ J ∧ J.IsMaximal}
⊢ x ∈ sInf {J_1 | J ≤ J_1 ∧ J_1.IsMaximal}
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case mp
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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach → x✝ ∈ commonDenomOfFinset M s • ↑s

pp: case mpr
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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s → x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach

Tactic:
· rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
    rw [map_integerMultiple]
    exact Set.mem_image_of_mem _ x.prop

Goal state after:
case mpr
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
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s → x✝ ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (λ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| η ⊗ₘ η ⊗ₘ η

Tactic:
← leftUnitor_tensor_inv

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (λ_ (𝟙_ C ⊗ 𝟙_ C)).inv

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| η ⊗ₘ η ⊗ₘ η
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ span R (Set.range ⇑(ofIsLocalizedModule Rₛ S f b)) = f.range

Tactic:
calc span R (Set.range (b.ofIsLocalizedModule Rₛ S f))
    _ = span R (f '' (Set.range b)) := by congr; ext; simp
    _ = map f (span R (Set.range b)) := by rw [Submodule.map_span]
    _ = LinearMap.range f := by rw [b.span_eq, Submodule.map_top]

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap

Tactic:
rw [← isLocalizedModule_iff_isBaseChange (S := S)]

Goal state after: