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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) ⊥ ≤ P

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (algebraMap R S) I ≤ P
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : y ∈ nonZeroDivisors R
h : IsAlgebraic R (y • z)
p : R[X]
hp : p ≠ 0
eval0 : (aeval (y • z)) p = 0
⊢ (aeval z) (p.comp (C y * X)) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : y ∈ nonZeroDivisors R
h : IsAlgebraic R (y • z)
p : R[X]
hp : p ≠ 0
eval0 : (aeval (y • z)) p = 0
⊢ (aeval ((algebraMap R A) y * z)) p = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ n ≠ 0

Tactic:
simpa using

Goal state after:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ ¬n = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_1
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ p ≠ 0

Tactic:
simpa using

Goal state after:
case refine_1
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ r ≠ 0 ∧ p✝ ≠ 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this✝ : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi₁ : i ∈ q.support
hi₂ : i ≠ q.natDegree
this : N + i < q.natDegree + N
⊢ (if i ≤ q.natDegree + N then (q.coeff i).coeff ((revAt N) (q.natDegree + N - i)) else 0) = 0

Tactic:
simpa using

Goal state after:
case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this✝ : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi₁ : i ∈ q.support
hi₂ : i ≠ q.natDegree
this : N + i < q.natDegree + N
⊢ (q.coeff i).coeff (q.natDegree + N - i) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s ↦ zeroLocus s) fun t ↦ ↑(vanishingIdeal t)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s ↦ zeroLocus s) fun t ↦ ↑(vanishingIdeal t)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
⊢ IsAlgebraic R a

Tactic:
have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
  let p := (r • p).toSubring (integralClosure R S).toSubring fun s hs ↦ by
    obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
    exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)
  have : IsAlgebraic (integralClosure R S) a := by
    refine ⟨p, ?_, ?_⟩
    · simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp
    rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]
  exact restrictScalars_of_isIntegral _ this

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

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
x y : C
h : (algebraMap C L) x = (algebraMap C L) y
⊢ ↑1 * x = ↑1 * y

Tactic:
simpa using

Goal state after:
A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
x y : C
h : (algebraMap C L) x = (algebraMap C L) y
⊢ x = y
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f * g} ↔ x ∈ zeroLocus {f} ∪ zeroLocus {g}

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R
x : PrimeSpectrum R
⊢ f * g ∈ x.asIdeal ↔ f ∈ x.asIdeal ∨ g ∈ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f ^ n} ↔ x ∈ zeroLocus {f}

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
x : PrimeSpectrum R
⊢ f ^ n ∈ x.asIdeal ↔ f ∈ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : m ≤ I.asIdeal
⊢ I ∈ {{ asIdeal := m, isPrime := ⋯ }}

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : m ≤ I.asIdeal
⊢ I = { asIdeal := m, isPrime := ⋯ }
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
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
⊢ y = 0

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
⊢ y = 0
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
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
x : N ⊗[R] M
⊢ (LinearMap.rTensor M 0) x = 0 ↔ x ∈ Set.range ⇑(LinearMap.rTensor M 0)

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
x : N ⊗[R] M
⊢ 0 = x
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
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
x : N
⊢ f x = 0 x

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
x : N
⊢ f x = 0
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.lTensor M f = 0
n : N
m : M
⊢ (TensorProduct.comm R N' M) (((AlgebraTensorModule.curry (LinearMap.rTensor M f)) n) m) =
    (TensorProduct.comm R N' M) (((AlgebraTensorModule.curry 0) n) m)

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.lTensor M f = 0
n : N
m : M
⊢ m ⊗ₜ[R] f n = 0
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ (TensorProduct.comm R M N') (((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n) =
    (TensorProduct.comm R M N') (((AlgebraTensorModule.curry 0) m) n)

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ f n ⊗ₜ[R] m = 0
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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
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'
aux : lTensor M f = 0
m : M
n : N
⊢ (AlgebraTensorModule.cancelBaseChange R S S M N')
      (((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f))) m))
          1)
        n) =
    (AlgebraTensorModule.cancelBaseChange R S S M N')
      (((AlgebraTensorModule.curry ((AlgebraTensorModule.curry 0) m)) 1) n)

Tactic:
simpa using

Goal state after:
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'
aux : lTensor M f = 0
m : M
n : N
⊢ m ⊗ₜ[R] f n = 0
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:
simpa using

Goal state after:
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
⊢ ¬Subsingleton (N ⧸ Ideal.map (algebraMap R S) I • ⊤) ↔ ¬Subsingleton (M ⧸ I • ⊤)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h.refine_1
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
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (A ∙ x) * M + (A ∙ x) * (A ∙ y) ≤ M

Tactic:
apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_right)

Goal state after:
case h.refine_1
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
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (A ∙ x) * (A ∙ y) ≤ M
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)
this :
  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
⊢ Function.Injective ⇑(LinearMap.lTensor S (LinearMap.lTensor M f))

Tactic:
simpa using

Goal state after:
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)
this :
  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
⊢ Function.Injective ⇑(LinearMap.lTensor (S ⊗[R] M) f)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
x : R i
⊢ x ∈ p.asIdeal ↔ x ∈ q.asIdeal

Tactic:
simpa using

Goal state after:
case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
x : R i
⊢ x ∈ p.asIdeal ↔ x ∈ q.asIdeal
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
I : Ideal R
inst✝² : I.IsPrime
k : Type u_5
inst✝¹ : Field k
p : Ideal k
inst✝ : p.IsPrime
⊢ p.IsMaximal

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
I : Ideal R
inst✝² : I.IsPrime
k : Type u_5
inst✝¹ : Field k
p : Ideal k
inst✝ : p.IsPrime
⊢ ⊥.IsMaximal
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
x✝¹ x✝ : Ideal A
h : map (algebraMap A B) x✝¹ = map (algebraMap A B) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
x✝¹ x✝ : Ideal A
h : map (algebraMap A B) x✝¹ = map (algebraMap A B) x✝
⊢ x✝¹ = x✝
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
x : Π₀ (i : ι), R i
hx : DFinsupp.coeFnAddMonoidHom x = 1
i : ι
hi : i ∉ x.support
⊢ False

Tactic:
simpa using

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
x : Π₀ (i : ι), R i
hx : DFinsupp.coeFnAddMonoidHom x = 1
i : ι
hi : i ∉ x.support
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
⊢ ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal

Tactic:
simpa using

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
⊢ 1 ∉ p.asIdeal