mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    (toFunAlgHom R A) (invFun R A p) = p →
      (toFunAlgHom R A) (invFun R A q) = q → (toFunAlgHom R A) (invFun R A (p + q)) = p + q

pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    (toFunAlgHom R A) (invFun R A p) = p →
      (toFunAlgHom R A) (invFun R A q) = q → (toFunAlgHom R A) (invFun R A (p + q)) = p + q
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case hx
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ ?x ∈ Ideal.map (algebraMap R S) I

pp: case h
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ?x

pp: case x
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ S

Tactic:
·

Goal state after:
case hx
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ ?x ∈ Ideal.map (algebraMap R S) I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case h
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ((algebraMap R S) y)

Tactic:
·

Goal state after:
case h
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
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ((algebraMap R S) y)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R
e : g (mk' S (x - y) 1) = 0
r : R
hr : r ∈ M
hr' : r * (x - y) ∈ RingHom.ker f
⊢ ↑⟨f r, ⋯⟩ * f x = ↑⟨f r, ⋯⟩ * f y

Tactic:
by simpa [sub_eq_zero, mul_sub] using hr'

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

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
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) →
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

pp: case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) →
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Tactic:
·

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
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ z' * ↑t ∈ localizationLocalizationSubmodule M N

pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ x * (algebraMap R T) ↑(z * ↑t', ⟨z' * ↑t, ?refine_1⟩).2 = (algebraMap R T) (z * ↑t', ⟨z' * ↑t, ?refine_1⟩).1

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ z' * ↑t ∈ localizationLocalizationSubmodule M N
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ x * (algebraMap R T) ↑(z * ↑t', ⟨z' * ↑t, ⋯⟩).2 = (algebraMap R T) (z * ↑t', ⟨z' * ↑t, ⋯⟩).1

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ x * (algebraMap R T) ↑(z * ↑t', ⟨z' * ↑t, ⋯⟩).2 = (algebraMap R T) (z * ↑t', ⟨z' * ↑t, ⋯⟩).1
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑c * z' ∈ localizationLocalizationSubmodule M N

pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑⟨↑c * z', ?refine_1⟩ * x = ↑⟨↑c * z', ?refine_1⟩ * y

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑c * z' ∈ localizationLocalizationSubmodule M N
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S

pp: case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ ∀ (x : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ ∀ (x : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ ∀ (x : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ Function.Injective ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ Function.Injective ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ Function.Surjective ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ Function.Surjective ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
·

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr.map_units
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (y : ↥(Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S))),
    IsUnit ((algebraMap (↥(adjoin R ↑σ)) S) ↑y)

pp: case surj
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (z : S), ∃ x, z * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

pp: case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
·

Goal state after:
case mpr.map_units
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (y : ↥(Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S))),
    IsUnit ((algebraMap (↥(adjoin R ↑σ)) S) ↑y)