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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
a : A
ha : Transcendental R a
inst✝ : Algebra.IsAlgebraic R S
⊢ Transcendental S a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommRing R
R' : Type u_4
S : Type u
inst✝¹⁴ : CommRing R'
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : IsFractionRing R R'
inst✝⁹ : FaithfulSMul R S
inst✝⁸ : Algebra.IsAlgebraic R S
inst✝⁷ : NoZeroDivisors S
S' : Type v
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R S'
inst✝⁴ : Algebra S S'
inst✝³ : Module R' S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsFractionRing S S'
⊢ Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
h : 1 ⊗ₜ[R] m = 0
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
this : f = 0
⊢ m = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommRing R
R' : Type u_4
S : Type u
inst✝¹⁴ : CommRing R'
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : IsFractionRing R R'
inst✝⁹ : FaithfulSMul R S
inst✝⁸ : Algebra.IsAlgebraic R S
inst✝⁷ : NoZeroDivisors S
S' : Type u
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R S'
inst✝⁴ : Algebra S S'
inst✝³ : Module R' S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsFractionRing S S'
⊢ Module.rank R' S' = Module.rank R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
⊢ finrank R S * finrank S T = finrank R T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
⊢ Function.Injective ⇑(algebraMap R S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
σ : Type u
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
⊢ Algebra.IsAlgebraic R[X] S[X]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
⊢ Module.rank (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 ↔ m = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
σ : Type u
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
z : A
z' : S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : Module.Finite R S
⊢ FiniteDimensional (FractionRing R) (FractionRing S)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ ↑z' * y = ↑⟨(algebraMap R S) z, hz0'⟩ * y'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
⊢ LinearMap.lTensor M LinearMap.id = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
x : R
⊢ (residue R) x = 0 ↔ x ∈ maximalIdeal R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
x : R
⊢ (residue R) x ≠ 0 ↔ IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsLocalRing R
inst✝⁴ : CommRing S
inst✝³ : IsLocalRing S
inst✝² : CommRing T
inst✝¹ : IsLocalRing T
f : R →+* S
inst✝ : IsLocalHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ((Ideal.Quotient.mk (maximalIdeal S)).comp f) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
inst✝³ : CommRing S
inst✝² : IsLocalRing S
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
f : R ≃+* S
x : ResidueField R
⊢ (map ↑f.symm) ((map ↑f) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
inst✝³ : CommRing S
inst✝² : IsLocalRing S
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
f : R ≃+* S
x : ResidueField S
⊢ (map ↑f) ((map ↑f.symm) x) = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : IsLocalRing R
inst✝¹² : CommRing S
inst✝¹¹ : IsLocalRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsLocalRing T
inst✝⁸ : Algebra R S
inst✝⁷ : IsLocalHom (algebraMap R S)
R₀ : Type u_4
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : IsLocalRing R₀
inst✝¹ : IsLocalHom (algebraMap R₀ R)
inst✝ : IsLocalHom (algebraMap R₀ S)
⊢ IsScalarTower (ResidueField R₀) (ResidueField R) (ResidueField S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsLocalRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsLocalRing S
inst✝⁴ : CommRing T
inst✝³ : IsLocalRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
e : S →ₐ[R] T
inst✝ : IsLocalHom e
x : R
⊢ (↑↑(map ↑e)).toFun ((algebraMap R (ResidueField S)) x) = (algebraMap R (ResidueField T)) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
⊢ Subsingleton N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
⊢ LinearMap.rTensor M LinearMap.id = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
⊢ ∀ z ∉ M, M < M + A ∙ z

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
eq : f = 0
⊢ lTensor M 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk (y, ⟨t, h⟩).1 (y, ⟨t, h⟩).2

Tactic:
simp only

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk y ⟨t, h⟩
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
⊢ ↑(Ideal.span {(algebraMap S L) a}) ⊆ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
⊢ FaithfullyFlat R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
by

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

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
⊢ Algebra.IsAlgebraic K L

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
⊢ FaithfullyFlat S (S ⊗[R] M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type u_1
N : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfullyFlat R S
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
I : Ideal R
⊢ Ideal.map (algebraMap R S) I • ⊤ ≠ ⊤ ↔ I • ⊤ ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit (f s)
hr' : f s * x = f r
⊢ 1 ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit (f s)
hr' : f s * x = f r
⊢ 1 * f s * x = 1 * f r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ 1 ∉ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ f 1 ∉ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ 1 * f 1 * s = 1 * f r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
⊢ (g.comp f).SurjectiveOnStalks

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
⊢ g.SurjectiveOnStalks

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ 1 • 1 ∉ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ 1 ⊗ₜ[R] (1 • 1) * 0 = 0 ⊗ₜ[R] 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
⊢ LinearMap.lTensor S (LinearMap.lTensor M f) =
    ↑(TensorProduct.assoc R S M P) ∘ₗ LinearMap.lTensor (S ⊗[R] M) f ∘ₗ ↑(TensorProduct.assoc R S M N).symm

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
h_nzI : I ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
⊢ Flat R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
⊢ baseChange A p ≤ baseChange A q ↔ p ≤ q

Tactic:
by

Goal state after: