mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
hx : x ≠ 0
⊢ ∏ᶠ (p : R), p ^ count p (normalizedFactors x) ~ᵤ x

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
S : Under R
⊢ { app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app
        ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) ≫
      (Under.forget R ⋙ forget₂ CommRingCat CommMonCat).map
        ({
              app := fun S ↦
                Under.homMk
                  (ofHom
                    (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                      (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                  ⋯,
              naturality := ⋯ }.app
          S) =
    𝟙 ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
⊢ a ∣ b ↔ ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
H : ∀ (p : R), Prime p → emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
p : R
hp : Prime p
this : ↑n * emultiplicity p a ≤ ↑n * emultiplicity p b
⊢ ↑n ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
⊢ Function.HasFiniteMulSupport fun s ↦ f s ^ multiplicity (g s) r

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.counit = CoalgebraStruct.counit

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.counit = CoalgebraStruct.counit

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x * invSelf x = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ s * (algebraMap R S) (x ^ (sec x s).2) = (algebraMap R S) (sec x s).1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
n : ℕ
⊢ (fun x_1 ↦ x ^ x_1) 1 = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (fun x_1 ↦ x ^ x_1) 1 = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ Associated ((algebraMap R S) (sec x s).1) s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
y : R
⊢ (∃ m ∈ Submonoid.powers x, y ∣ m) ↔ ∃ n, y ∣ x ^ n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
⊢ ∀ (y : ↥(Submonoid.powers r)), IsUnit ((algebraMap R S) ↑y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
x y : R
h : (algebraMap R S) x = (algebraMap R S) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r r' : R
h : Associated r r'
inst✝ : Away r S
⊢ Away r' S

Tactic:
by

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

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
P : Type u_3
inst✝⁶ : CommSemiring P
x : R
inst✝⁵ : Away x S
g : R →+* P
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A P
inst✝ : IsScalarTower A R S
f : R →ₐ[A] P
hf : IsUnit (f x)
r : A
⊢ (↑↑(lift x hf)).toFun ((algebraMap A S) r) = (algebraMap A P) r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0
x : R
hx : f x = 0
⊢ f r ^ 0 * f x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
a : R
n : ℕ
ha : f r ^ n * f a = 0
⊢ f (r ^ n * a) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
a : R
n : ℕ
ha : f r ^ n * f a = 0
m : ℕ
hm : r ^ m * (r ^ n * a) = 0
⊢ r ^ (m + n) * a = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Function.Injective ⇑(map S Q f r) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
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 ^ (0 + n) * b) = f r ^ (0 + (n + m)) * a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
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
⊢ Function.Surjective ⇑(map S Q f r) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a

Tactic:
by

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

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
P : Type u_3
inst✝¹⁶ : CommSemiring P
x : R
inst✝¹⁵ : Away x S
g : R →+* P
Q : Type u_4
inst✝¹⁴ : CommSemiring Q
inst✝¹³ : Algebra P Q
A : Type u_5
inst✝¹² : CommSemiring A
inst✝¹¹ : Algebra R A
B : Type u_6
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R B
Aₚ : Type u_7
inst✝⁸ : CommSemiring Aₚ
inst✝⁷ : Algebra A Aₚ
inst✝⁶ : Algebra R Aₚ
inst✝⁵ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁴ : CommSemiring Bₚ
inst✝³ : Algebra B Bₚ
inst✝² : Algebra R Bₚ
inst✝¹ : IsScalarTower R B Bₚ
f : A →+* B
a : A
inst✝ : Away (f a) Bₚ
⊢ IsLocalization (Submonoid.map f (Submonoid.powers a)) Bₚ

Tactic:
by

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

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
P : Type u_3
inst✝¹⁶ : CommSemiring P
x✝ : R
inst✝¹⁵ : Away x✝ S
g : R →+* P
Q : Type u_4
inst✝¹⁴ : CommSemiring Q
inst✝¹³ : Algebra P Q
A : Type u_5
inst✝¹² : CommSemiring A
inst✝¹¹ : Algebra R A
B : Type u_6
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R B
Aₚ : Type u_7
inst✝⁸ : CommSemiring Aₚ
inst✝⁷ : Algebra A Aₚ
inst✝⁶ : Algebra R Aₚ
inst✝⁵ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁴ : CommSemiring Bₚ
inst✝³ : Algebra B Bₚ
inst✝² : Algebra R Bₚ
inst✝¹ : IsScalarTower R B Bₚ
x : R
inst✝ : Away ((algebraMap R A) x) Aₚ
⊢ IsLocalization (Algebra.algebraMapSubmonoid A (Submonoid.powers x)) Aₚ

Tactic:
by

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

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
P : Type u_3
inst✝¹⁷ : CommSemiring P
x : R
inst✝¹⁶ : Away x S
g : R →+* P
Q : Type u_4
inst✝¹⁵ : CommSemiring Q
inst✝¹⁴ : Algebra P Q
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ (↑↑(map Aₚ Bₚ f.toRingHom a)).toFun ((algebraMap R Aₚ) r) = (algebraMap R Bₚ) r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ x - 0 ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
⊢ s ⊆ ↑(span s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
⊢ span s ≤ span t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
h : (fun a b ↦ a - b ∈ s) ≤ ⇑I.ringCon
x : R
hx : x ∈ s
⊢ x ∈ ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ span s ≤ I ↔ s ⊆ ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x✝ : R
hx✝ : x✝ ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x : R
hx : x ∈ s
⊢ x - 0 ∈ span s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x✝ : R
hx✝ : x✝ ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x : R
hx : x ∈ s
⊢ p (x - 0) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x : R
hx : x ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x✝ : x - 0 ∈ span s
⊢ p (x - 0) x✝ → p x hx

Tactic:
by

Goal state after:
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
⊢ Monotone fun I ↦ { ringCon := I.ringCon.comap f }

Tactic:
by

Goal state after:
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
I : TwoSidedIdeal S
x : R
⊢ x ∈ (comap f) I ↔ f x ∈ I

Tactic:
by

Goal state after:
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
⊢ (comap e.symm).comp (comap e) = OrderHom.id

Tactic:
by

Goal state after:
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
⊢ (comap e).comp (comap e.symm) = OrderHom.id

Tactic:
by

Goal state after:
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
⊢ (comap f) ((comap g) I) = (comap (g.comp f)) I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
⊢ x * y ∈ closure s

Tactic:
by

Goal state after: