mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
⊢ I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime J
⊢ (↑↑(localRingHom I J (↑f) hIJ)).toFun ((localRingHom J I ↑f.symm ⋯) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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
I✝ : Ideal R
hI : I✝.IsPrime
inst✝² : Algebra R P
I : Ideal S
inst✝¹ : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : S →ₐ[R] P
hIJ : I = Ideal.comap f J
r : R
⊢ (↑↑(localRingHom I J f.toRingHom hIJ)).toFun ((algebraMap R (Localization.AtPrime I)) r) =
    (algebraMap R (Localization.AtPrime J)) r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
⊢ ∀ (m : S) (x : S ⧸ Ideal.map (algebraMap R S) I),
    (↑(tensorQuotEquivQuotSMul S I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (algebraMap R S) I)).symm).toFun
        (m • x) =
      (RingHom.id S) m •
        (↑(tensorQuotEquivQuotSMul S I ≪≫ₗ
                    (I • ⊤).quotEquivOfEq (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯ ≪≫ₗ
                  Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (algebraMap R S) I)).symm).toFun
          x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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✝
I : Ideal R
hI : I.IsPrime
P : Ideal S
inst✝ : P.IsPrime
s : Subalgebra R S
⊢ P.primeCompl ⊓ s.toSubmonoid ≤ s.toSubmonoid

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
this :
  ∀ a ∈ s,
    ∀ b ∈ s,
      b ∉ P →
        ∀ c ∈ s,
          ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
⊢ Function.Injective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x : M ⊗[R] (N ⧸ n)
⊢ (↑(TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n))).toFun (m • x) =
    (RingHom.id A) m • (↑(TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n))).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
a : A
m : M
n : N
⊢ (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) ∈ ↑(mapOfCompatibleSMul A R A M N).ker

Tactic:
simp [smul_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
x✝¹ x✝ : N
⊢ S.mkQ (m ⊗ₜ[R] (x✝¹ + x✝)) = S.mkQ (m ⊗ₜ[R] x✝¹) + S.mkQ (m ⊗ₜ[R] x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
t : S
ht : t * x ∈ s
htP : t ∈ ↑P.primeCompl
⊢ t * x * (a * d) = t * x * (c * b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ S.mkQ (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • S.mkQ (m ⊗ₜ[R] n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
x✝¹ x✝ : M
⊢ { toFun := fun n ↦ S.mkQ ((x✝¹ + x✝) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun n ↦ S.mkQ (x✝¹ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun n ↦ S.mkQ (x✝ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
this : ∀ (y z : S), z ∉ P → ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
⊢ Function.Surjective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
x✝¹ : A
x✝ : M
⊢ { toFun := fun n ↦ S.mkQ ((x✝¹ • x✝) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) x✝¹ • { toFun := fun n ↦ S.mkQ (x✝ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ ↑P.primeCompl
has : a ∈ ↑s.toSubmonoid
b : S
hb : b * z ∈ s
hbP : b ∈ ↑P.primeCompl
hbs : b ∈ ↑s.toSubmonoid
⊢ 1 * (z * (a * y * b)) = 1 * (b * z * a * y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
⊢ F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
⊢ Function.Bijective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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✝
I : Ideal R
hI : I.IsPrime
A : Type u_4
B : Type u_5
C : Type u_6
inst✝¹⁴ : CommSemiring A
inst✝¹³ : CommSemiring B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : Algebra A B
inst✝⁹ : IsScalarTower R A B
inst✝⁸ : CommSemiring C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : IsScalarTower A B C
p : Ideal A
inst✝⁴ : p.IsPrime
P : Ideal B
inst✝³ : P.IsPrime
inst✝² : P.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝ : IsLiesOverAlgebra p P
⊢ ∀ (x : R),
    (algebraMap R (Localization.AtPrime P)) x =
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime P)) ((algebraMap R (Localization.AtPrime p)) x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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✝
I : Ideal R
hI : I.IsPrime
A : Type u_4
B : Type u_5
C : Type u_6
inst✝²¹ : CommSemiring A
inst✝²⁰ : CommSemiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : IsScalarTower R A B
inst✝¹⁵ : CommSemiring C
inst✝¹⁴ : Algebra A C
inst✝¹³ : Algebra B C
inst✝¹² : IsScalarTower A B C
p : Ideal A
inst✝¹¹ : p.IsPrime
P : Ideal B
inst✝¹⁰ : P.IsPrime
inst✝⁹ : P.LiesOver p
Q : Ideal C
inst✝⁸ : Q.IsPrime
inst✝⁷ : Q.LiesOver P
inst✝⁶ : Q.LiesOver p
inst✝⁵ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝⁴ : IsLiesOverAlgebra p P
inst✝³ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝² : IsLiesOverAlgebra P Q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime Q)
inst✝ : IsLiesOverAlgebra p Q
⊢ algebraMap (Localization.AtPrime p) (Localization.AtPrime Q) =
    (algebraMap (Localization.AtPrime P) (Localization.AtPrime Q)).comp
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime P))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ Disjoint ↑q.primeCompl ↑p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ p.IsPrime

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ (map (algebraMap R S) p).IsPrime

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ under R (map (algebraMap R S) p) = p

Tactic:
by

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

Goal state before:
pp: R : Type u_5
inst✝³ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
S : Type u_6
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.AtPrime S p
this : p.IsPrime
⊢ { asIdeal := p, isPrime := ⋯ } ∈ Set.Iic { asIdeal := p, isPrime := ⋯ }

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
h : Ideal.map (algebraMap R R') (under R (under R' (Ideal.map (algebraMap S S') P))) = Ideal.map (algebraMap R R') p
⊢ Ideal.map (algebraMap R R') p = under R' (Ideal.map (algebraMap S S') P)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ (Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : (under R ⊤).IsMaximal
⊢ under R ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ (mapOfCompatibleSMul A R A M N).ker = Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
J : Ideal S
inst✝ : (under R J).IsMaximal
⊢ J ≠ ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
J : Ideal S
inst✝ : (under R J).IsMaximal
⊢ J.IsMaximal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
p : Ideal R
inst✝⁴ : p.IsPrime
Rₚ : Type u_4
inst✝³ : CommSemiring Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ Ideal.map (algebraMap R Rₚ) p = maximalIdeal Rₚ

Tactic:
convert! congr_arg (Ideal.map (algebraMap R Rₚ)) (under_maximalIdeal Rₚ p).symm

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
p : Ideal R
inst✝⁴ : p.IsPrime
Rₚ : Type u_4
inst✝³ : CommSemiring Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ maximalIdeal Rₚ = Ideal.map (algebraMap R Rₚ) (under R (maximalIdeal Rₚ))
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
p : Ideal R
inst✝⁴ : p.IsPrime
Rₚ : Type u_4
inst✝³ : CommSemiring Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ Ideal.map (algebraMap R Rₚ) p = maximalIdeal Rₚ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ coeSubmodule S ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ coeSubmodule S ⊤ = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
h : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
by

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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✝
p : Ideal R
inst✝⁸ : p.IsPrime
Rₚ : Type u_4
inst✝⁷ : CommSemiring Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p
inst✝⁴ : IsLocalRing Rₚ
Sₚ : Type u_5
inst✝³ : CommSemiring Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : Algebra Rₚ Sₚ
P : Ideal S
⊢ (Ideal.map (algebraMap R Rₚ) p).IsMaximal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
h : x✝ ∈ p ^ n
⊢ 1 ∈ p.primeCompl

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
h : x✝ ∈ p ^ n
⊢ 1 * x✝ ∈ p ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
⊢ under R (maximalIdeal Rₚ ^ n) = p ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ (coeSubmodule S I).IsPrincipal ↔ Submodule.IsPrincipal I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ x = mk' S 1 1 • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ 0 = mk' S 1 1 • 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.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✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h₁ : EssFiniteType R S
h₂ : EssFiniteType S T
⊢ EssFiniteType R T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ S₀ M, FiniteType R ↥S₀ ∧ IsLocalization M S

Tactic:
by

Goal state after: