mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hp : f.Splits
hq : g.Splits
⊢ (f * g).Splits

pp: case inl.inr
R : Type u_1
inst✝¹ : CommRing R
g : R[X]
inst✝ : IsDomain R
hp : Splits 0
⊢ (0 * g).Splits

pp: case inr.inl
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hq : Splits 0
⊢ (f * 0).Splits

pp: case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (0 * 0).Splits

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hp : f.Splits
hq : g.Splits
⊢ (f * g).Splits

case inl.inr
R : Type u_1
inst✝¹ : CommRing R
g : R[X]
inst✝ : IsDomain R
hp : Splits 0
⊢ (0 * g).Splits

case inr.inl
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hq : Splits 0
⊢ (f * 0).Splits

case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (0 * 0).Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : (algebraMap Rₘ Sₘ) v' * (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑⟨v, ⋯⟩) = 1
⊢ (algebraMap Rₘ Sₘ) v' * (algebraMap S Sₘ) u = 1

Tactic:
localizationAlgebraMap_def,

Goal state after:
case refine_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' :
  (IsLocalization.map Sₘ (algebraMap R S) ⋯) v' *
      (IsLocalization.map Sₘ (algebraMap R S) ⋯) ((algebraMap R Rₘ) ↑⟨v, ⋯⟩) =
    1
⊢ (algebraMap Rₘ Sₘ) v' * (algebraMap S Sₘ) u = 1
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
⊢ f.Splits

Tactic:
by_cases hf0 : f = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : f = 0
⊢ f.Splits

case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
⊢ f.Splits
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ 0 ≠ 0 → eval₂ f r 0 = 0 → ∃ i, coeff 0 i ≠ 0 ∧ coeff 0 i ∈ comap f I

pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
          p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]),
    p ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
        p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
· intro h
    contradiction

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
          p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]),
    p ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
        p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
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
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : Submodule.comap l23.ker.subtype l12.range = ⊤
⊢ l23.ker = l12.range

Tactic:
Submodule.comap_subtype_eq_top

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : l23.ker ≤ l12.range
⊢ l23.ker = l12.range
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case left.inl.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' })
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' })
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }

pp: case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' })
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' })
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
<;>

Goal state after:
case left.inl.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' })
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inl { asIdeal := I', isPrime := hI' }

case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' })
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }

case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' })
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' })
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }
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
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
⊢ z * (algebraMap C L) ↑(mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).2 =
    (algebraMap C L) (mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).1

Tactic:
by
        rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]

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

Goal state before:
pp: case h₁
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asIdeal

pp: case h₂
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asIdeal

Tactic:
<;>

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asIdeal

case h₂
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asIdeal
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a)

pp: case mp.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) b)

Tactic:
<;>

Goal state after:
case mp.refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a)

case mp.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) b)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ I

Tactic:
by
  induction I using IsNoetherian.induction with | hgt M hgt =>
  change Ideal R at M
  by_cases h_prM : M.IsPrime
  · use {⟨M, h_prM⟩}
    rw [Multiset.map_singleton, Multiset.prod_singleton]
  by_cases htop : M = ⊤
  · rw [htop]
    exact ⟨0, le_top⟩
  have lt_add : ∀ z ∉ M, M < M + span R {z} := by
    intro z hz
    refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
    rw [m_eq]
    exact Ideal.mem_sup_right (mem_span_singleton_self z)
  obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop
  obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx)
  obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy)
  use Wx + Wy
  rw [Multiset.map_add, Multiset.prod_add]
  apply le_trans (mul_le_mul' h_Wx h_Wy)
  rw [add_mul]
  apply sup_le (show M * (M + span R {y}) ≤ M from Ideal.mul_le_left)
  rw [mul_add]
  apply sup_le (show span R {x} * M ≤ M from Ideal.mul_le_right)
  rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]

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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
⊢ ∀ x ∈ s, IsAlgebraic (↥Rt) x

Tactic:
intro x hs

Goal state after:
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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
x : S
hs : x ∈ s
⊢ IsAlgebraic (↥Rt) 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'
h : LinearMap.rTensor M f = 0
⊢ LinearMap.lTensor M f = 0

Tactic:
ext m n; exact (TensorProduct.comm R M N').injective <| (by simpa using congr($h (n ⊗ₜ m)))

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case e'_2
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
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (t * (f yx * f ts)) = yc * f yx * (yt * f ts * t)

pp: case e'_3
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
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (f ys * f tx * y) = yc * f ys * y * (yt * f tx)

Tactic:
<;>

Goal state after:
case e'_2
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
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (t * (f yx * f ts)) = yc * f yx * (yt * f ts * t)

case e'_3
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
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (f ys * f tx * y) = yc * f ys * y * (yt * f tx)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h.refine_2.inl
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 ≠ ⊥
hx : (Multiset.map asIdeal Wx).prod = ⊥
⊢ False

pp: case h.refine_2.inr
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 ≠ ⊥
hy : (Multiset.map asIdeal Wy).prod = ⊥
⊢ False

Tactic:
<;>

Goal state after:
case h.refine_2.inl
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 ≠ ⊥
hx : (Multiset.map asIdeal Wx).prod = ⊥
⊢ False

case h.refine_2.inr
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 ≠ ⊥
hy : (Multiset.map asIdeal Wy).prod = ⊥
⊢ False
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case ha
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x✝ : S
⊢ ((Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
            ((↑(Algebra.TensorProduct.comm R T' S)).comp
              ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T)))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

pp: case hb
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
              ((↑(Algebra.TensorProduct.comm R T' S)).comp
                ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x✝ : S
⊢ ((Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
            ((↑(Algebra.TensorProduct.comm R T' S)).comp
              ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T)))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

case hb
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
              ((↑(Algebra.TensorProduct.comm R T' S)).comp
                ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))).comp
        Algebra.TensorProduct.includeRight)
      x✝