mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Mon Cᵒᵖ
⊢ (ρ_ A.X).hom.unop = (ρ_ (unop A.X)).inv

Tactic:
;

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 : Mon Cᵒᵖ
⊢ (ρ_ A.X).hom.unop = (ρ_ (unop A.X)).inv
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
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (f.unop.hom.unop ≫ ε).op = ε.op

Tactic:
;

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
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (f.unop.hom.unop ≫ ε).op = ε.op
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
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (f.unop.hom.unop ≫ Δ).op = (Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop)).op

Tactic:
;

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
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (f.unop.hom.unop ≫ Δ).op = (Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop)).op
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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ F.map ε ≫ η F = F.map ε ≫ η F

Tactic:
;

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ F.map ε ≫ η F = F.map ε ≫ η F
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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
A : Comon C
⊢ { hom := F.map (𝟙 A).hom, isComonHom_hom := ⋯ }.hom = (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }).hom

Tactic:
;

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
A : Comon C
⊢ { hom := F.map (𝟙 A).hom, isComonHom_hom := ⋯ }.hom = (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }).hom
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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X✝ Y✝ Z✝ : Comon C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ }.hom =
    ({ hom := F.map f.hom, isComonHom_hom := ⋯ } ≫ { hom := F.map g.hom, isComonHom_hom := ⋯ }).hom

Tactic:
;

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X✝ Y✝ Z✝ : Comon C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ }.hom =
    ({ hom := F.map f.hom, isComonHom_hom := ⋯ } ≫ { hom := F.map g.hom, isComonHom_hom := ⋯ }).hom
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: n : Type v
inst✝ : Unique n
X✝ Y✝ : CommRingCat
f : X✝ ⟶ Y✝
x✝ : ↑((coyoneda.obj (op n)).obj X✝)
⊢ (Hom.hom ((coyoneda.obj (op n)).map f ≫ (RingEquiv.piUnique fun i ↦ ↑Y✝).toCommRingCatIso.hom)) x✝ =
    (Hom.hom ((RingEquiv.piUnique fun i ↦ ↑X✝).toCommRingCatIso.hom ≫ (𝟭 CommRingCat).map f)) x✝

Tactic:
;

Goal state after:
n : Type v
inst✝ : Unique n
X✝ Y✝ : CommRingCat
f : X✝ ⟶ Y✝
x✝ : ↑((coyoneda.obj (op n)).obj X✝)
⊢ (Hom.hom ((coyoneda.obj (op n)).map f ≫ (RingEquiv.piUnique fun i ↦ ↑Y✝).toCommRingCatIso.hom)) x✝ =
    (Hom.hom ((RingEquiv.piUnique fun i ↦ ↑X✝).toCommRingCatIso.hom ≫ (𝟭 CommRingCat).map f)) x✝
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯))

Tactic:
;

Goal state after:
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯))
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S : Under R
x✝ : ↑R
⊢ (Hom.hom
        ((((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)) ⋯)))
      x✝ =
    (Hom.hom ((𝟭 (Under R)).obj S).hom) x✝

Tactic:
;

Goal state after:
R : CommRingCat
S : Under R
x✝ : ↑R
⊢ (Hom.hom
        ((((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)) ⋯)))
      x✝ =
    (Hom.hom ((𝟭 (Under R)).obj S).hom) x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ¬x ∣ a

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ¬x ∣ a
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom CoalgebraStruct.comul ≫ X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫
        ModuleCat.ofHom CoalgebraStruct.comul ▷ X.toModuleCat ≫ (α_ X.toModuleCat X.toModuleCat X.toModuleCat).hom)

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom CoalgebraStruct.comul ≫ X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫
        ModuleCat.ofHom CoalgebraStruct.comul ▷ X.toModuleCat ≫ (α_ X.toModuleCat X.toModuleCat X.toModuleCat).hom)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

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

Tactic:
;

Goal state after:
R : CommRingCat
S : Under R
⊢ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑S.right) ≫
      CommMonCat.ofHom ↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id ↑S.right) ⋯) =
    𝟙 ((forget₂ CommRingCat CommMonCat).obj S.right)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S : Under R
x✝ : ↑((forget₂ CommRingCat CommMonCat).obj S.right)
⊢ (CommMonCat.Hom.hom
        (CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑S.right) ≫
          CommMonCat.ofHom ↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id ↑S.right) ⋯)))
      x✝ =
    (CommMonCat.Hom.hom (𝟙 ((forget₂ CommRingCat CommMonCat).obj S.right))) x✝

Tactic:
;

Goal state after:
R : CommRingCat
S : Under R
x✝ : ↑((forget₂ CommRingCat CommMonCat).obj S.right)
⊢ (CommMonCat.Hom.hom
        (CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑S.right) ≫
          CommMonCat.ofHom ↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id ↑S.right) ⋯)))
      x✝ =
    (CommMonCat.Hom.hom (𝟙 ((forget₂ CommRingCat CommMonCat).obj S.right))) x✝
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
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((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)
        1)
      x✝ =
    (((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))
        1)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((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)
        1)
      x✝ =
    (((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))
        1)
      x✝
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
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((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)
        x✝)
      1 =
    (((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))
        x✝)
      1

Tactic:
;

Goal state after:
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((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)
        x✝)
      1 =
    (((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))
        x✝)
      1
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
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : P), ∃ b m, f b = f r ^ m * a
a : P
n : ℕ
b : R
m : ℕ
e : f b = f r ^ m * a
⊢ f r ^ n * (f r ^ m * a) = f r ^ n * f r ^ m * a

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : P), ∃ b m, f b = f r ^ m * a
a : P
n : ℕ
b : R
m : ℕ
e : f b = f r ^ m * a
⊢ f r ^ n * (f r ^ m * a) = f r ^ n * f r ^ m * a
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
x✝¹ : TwoSidedIdeal S
x✝ : S
⊢ x✝ ∈ ((comap e.symm).comp (comap e)) x✝¹ ↔ x✝ ∈ OrderHom.id x✝¹

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
x✝¹ : TwoSidedIdeal S
x✝ : S
⊢ x✝ ∈ ((comap e.symm).comp (comap e)) x✝¹ ↔ x✝ ∈ OrderHom.id x✝¹
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
x✝¹ : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ ((comap e).comp (comap e.symm)) x✝¹ ↔ x✝ ∈ OrderHom.id x✝¹

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
x✝¹ : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ ((comap e).comp (comap e.symm)) x✝¹ ↔ x✝ ∈ OrderHom.id x✝¹
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
x✝ : R
⊢ x✝ ∈ (comap f) ((comap g) I) ↔ x✝ ∈ (comap (g.comp f)) I

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
x✝ : R
⊢ x✝ ∈ (comap f) ((comap g) I) ↔ x✝ ∈ (comap (g.comp f)) I
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
inst✝ : Away e S
x : R
n : ℕ
⊢ e * x = e ^ 1 * x

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
⊢ e * x = e ^ 1 * x
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
m : Ideal R
inst✝ : m.IsMaximal
⊢ jacobson R ≤ m

Tactic:
rw [Ring.jacobson_eq_sInf_isMaximal]
  exact sInf_le ‹_›

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ (TwoSidedIdeal.asIdeal I).toTwoSided ↔ x✝ ∈ I

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ (TwoSidedIdeal.asIdeal I).toTwoSided ↔ x✝ ∈ I
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' := ⋯ }
⊢ 0 ∈ Module.jacobson R (R ⧸ I)

Tactic:
;

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' := ⋯ }
⊢ 0 ∈ Module.jacobson R (R ⧸ I)
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
le : I ≤ jacobson R
⊢ (Ideal.Quotient.mk I).toSemilinearMap.ker ≤ Module.jacobson R R

Tactic:
← I.ker_mkQ

Goal state after:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
le : (Submodule.mkQ I).ker ≤ jacobson R
⊢ (Ideal.Quotient.mk I).toSemilinearMap.ker ≤ Module.jacobson R R
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ Ring.jacobson R • N

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ Ring.jacobson R • N
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
ι : Type u_3
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ¬IsUnit (f i)
⊢ ¬IsUnit (∑ i ∈ s, f i)

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
ι : Type u_3
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ¬IsUnit (f i)
⊢ ¬IsUnit (∑ i ∈ s, f i)
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit 1

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit 1
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ f a ^ n * ((f a * f b) ^ m * s) = f a ^ n * f a ^ m * f b ^ m * s

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ f a ^ n * ((f a * f b) ^ m * s) = f a ^ n * f a ^ m * f b ^ m * s
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
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
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
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
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set 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
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
⊢ (algebraMap R (Away ↑a)) r = f a

Tactic:
have ⟨r', eq, _⟩ := this ({a.1} ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦
      h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) (Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{a.1} ∪ t, by simp⟩

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set 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
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq✝ : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
r' : R
eq : (fun r ↦ ∀ (a_1 : ↑({↑a} ∪ ↑t)), (algebraMap R (Away ↑a_1)) r = f ⟨↑a_1, ⋯⟩) r'
right✝ : ∀ (y : R), (fun r ↦ ∀ (a_1 : ↑({↑a} ∪ ↑t)), (algebraMap R (Away ↑a_1)) r = f ⟨↑a_1, ⋯⟩) y → y = r'
⊢ (algebraMap R (Away ↑a)) r = f a