awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e :
  HMul.hMul (α := S ⧸ q) (β := S ⧸ q)
      (((aeval ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) x) : AlgHom.{u_1, u_1, u_2} R R[X] (S ⧸ q)) :
            (a : R[X]) → S ⧸ q)
          p :
        S ⧸ q)
      ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u : S ⧸ q) =
    0
⊢ HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q

Tactic:
rw [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at e

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem, map_mul, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
⊢ q.IsPrime

Tactic:
have := hq.1.1
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this : q.IsPrime
⊢ Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)

Tactic:
have : Ring.KrullDimLE 0 (Localization.AtPrime q) := .of_isLocalization _ hq _
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
rw :
  Membership.mem (α := Localization.AtPrime q) (γ := Ideal (Localization.AtPrime q))
    (Ideal.map (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q)) q)
    ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q)
        (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u) :
      Localization.AtPrime q)
⊢ Eq (α := Localization.AtPrime q)
    ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q)
        (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u) :
      Localization.AtPrime q)
    (0 : Localization.AtPrime q)

Tactic:
rw [← Ideal.mem_bot, ← IsLocalRing.maximalIdeal_eq_bot,
      ← Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Ideal.mem_bot, IsLocalRing.maximalIdeal_eq_bot, Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
⊢ Membership.mem (α := Localization.AtPrime q) (γ := Ideal (Localization.AtPrime q))
    (Ideal.map (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q)) q)
    ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q)
        (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u) :
      Localization.AtPrime q)

Tactic:
Ideal.mem_map_of_mem _ e

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
⊢ Membership.mem (α := Localization.AtPrime q) (γ := Ideal (Localization.AtPrime q))
    (Ideal.map (F := S →+* Localization.AtPrime q) (algebraMap S (Localization.AtPrime q)) q)
    ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q)
        (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u) :
      Localization.AtPrime q)

Tactic:
exact Ideal.mem_map_of_mem _ e

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
obtain :
  ∀ (m : S) (hmq : m ∈ q.primeCompl)
    (hm :
      (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
          HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
        0),
    HMul.hMul (α := (S ⧸ q)[X]) (β := (S ⧸ q)[X]) (map (algebraMap R (S ⧸ q)) p)
        ((C : (a : S ⧸ q) → (S ⧸ q)[X]) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u) : (S ⧸ q)[X]) =
      0
⊢ HMul.hMul (α := (S ⧸ q)[X]) (β := (S ⧸ q)[X]) (map (algebraMap R (S ⧸ q)) p)
      ((C : (a : S ⧸ q) → (S ⧸ q)[X]) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u) : (S ⧸ q)[X]) =
    0

Tactic:
obtain ⟨⟨m, hmq⟩, hm⟩ := (IsLocalization.map_eq_zero_iff q.primeCompl (Localization.AtPrime q)
    (aeval x p * u)).mp (by rw [← Ideal.mem_bot, ← IsLocalRing.maximalIdeal_eq_bot,
      ← Localization.AtPrime.map_eq_maximalIdeal]; exact Ideal.mem_map_of_mem _ e)

Premises used: HMul.hMul, Localization.AtPrime, IsLocalization.map_eq_zero_iff, Iff.mp, Ideal.primeCompl, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
a :
  ∀ (i : ℕ),
    (HMul.hMul (α := (S ⧸ q)[X]) (β := (S ⧸ q)[X]) (map (algebraMap R (S ⧸ q)) p)
            ((C : (a : S ⧸ q) → (S ⧸ q)[X]) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u) : (S ⧸ q)[X])).coeff
        i =
      coeff 0 i
⊢ HMul.hMul (α := (S ⧸ q)[X]) (β := (S ⧸ q)[X]) (map (algebraMap R (S ⧸ q)) p)
      ((C : (a : S ⧸ q) → (S ⧸ q)[X]) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u) : (S ⧸ q)[X]) =
    0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
i : ℕ
a : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u ∈ q
⊢ (HMul.hMul (α := (S ⧸ q)[X]) (β := (S ⧸ q)[X]) (map (algebraMap R (S ⧸ q)) p)
          ((C : (a : S ⧸ q) → (S ⧸ q)[X]) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u) : (S ⧸ q)[X])).coeff
      i =
    coeff 0 i

Tactic:
simp only [coeff_mul_C, coeff_map, coeff_zero, ← Ideal.Quotient.mk_algebraMap, ← map_mul,
    Ideal.Quotient.eq_zero_iff_mem]

Premises used: Polynomial.coeff_map, Polynomial.coeff_mul_C, Ideal.Quotient.eq_zero_iff_mem, map_mul, Polynomial.coeff_zero, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
i : ℕ
⊢ HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) (u * m) = 0

Tactic:
linear_combination hm
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
i : ℕ
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u * m = 0

Tactic:
simpa [← mul_assoc] using congr(($(hx (u * m) p (by linear_combination hm))).coeff i)

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
i : ℕ
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u * m = 0

Tactic:
have : algebraMap R S (p.coeff i) * u * m = 0 := by
    simpa [← mul_assoc] using congr(($(hx (u * m) p (by linear_combination hm))).coeff i)
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this_3 : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
i : ℕ
this : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u * m = 0
⊢ m * HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u = 0

Tactic:
linear_combination this
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
u : S
p : R[X]
e : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
this_1 : q.IsPrime
this_2 : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
this_3 : Field (Localization.AtPrime q) := IsField.toField ⋯
m : S
hmq : m ∈ q.primeCompl
hm :
  (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) m hmq) : S) *
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u =
    0
i : ℕ
this : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u * m = 0
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u ∈ q

Tactic:
exact (Ideal.IsPrime.mem_or_mem_of_mul_eq_zero ‹_› (by linear_combination this)).resolve_left hmq

Premises used: Or.resolve_left, Ideal.IsPrime.mem_or_mem_of_mul_eq_zero
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom (K := FractionRing (MvPolynomial ι F)) ⋯
hC :
  ∀ (x_1 : F),
    Eq.{u_3 + 1} (α := E)
      ((RingHom.comp (β := MvPolynomial ι F)
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
                (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))))
              C :
            (a : F) → E)
          x_1 :
        E)
      ((RingHom.comp (↑(aeval x) : MvPolynomial ι F →+* E) C : (a : F) → E) x_1 : E)
hX :
  ∀ (i_1 : ι),
    Eq.{u_3 + 1} (α := E)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
              (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) :
            (a : MvPolynomial ι F) → E)
          (X i_1) :
        E)
      (((↑(aeval x) : MvPolynomial ι F →+* E) : (a : MvPolynomial ι F) → E) (X i_1) : E)
⊢ Eq (α := MvPolynomial ι F →+* E)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
      (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))))
    (↑(aeval x) : MvPolynomial ι F →+* E)

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom (K := FractionRing (MvPolynomial ι F)) ⋯
x_1 : F
⊢ Eq.{u_3 + 1} (α := E)
    ((RingHom.comp (β := MvPolynomial ι F)
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
              (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))))
            C :
          (a : F) → E)
        x_1 :
      E)
    ((RingHom.comp (↑(aeval x) : MvPolynomial ι F →+* E) C : (a : F) → E) x_1 : E)

Tactic:
simp [i]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom (K := FractionRing (MvPolynomial ι F)) ⋯
i_1 : ι
⊢ Eq.{u_3 + 1} (α := E)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
            (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) :
          (a : MvPolynomial ι F) → E)
        (X i_1) :
      E)
    (((↑(aeval x) : MvPolynomial ι F →+* E) : (a : MvPolynomial ι F) → E) (X i_1) : E)

Tactic:
simp [i]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
a : FractionRing (MvPolynomial ι F)
⊢ Eq.{u_3 + 1} (α := E)
    ((↑((hx.aevalEquivField : (a : FractionRing (MvPolynomial ι F)) → ↥(IntermediateField.adjoin F (range x))) a) : E) :
      E)
    ((IsFractionRing.lift ⋯ : (a : FractionRing (MvPolynomial ι F)) → E) a : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
a : MvPolynomial ι F
⊢ Eq.{u_3 + 1} (α := E)
    ((↑((hx.aevalEquivField : (a : FractionRing (MvPolynomial ι F)) → ↥(IntermediateField.adjoin F (range x)))
            ((algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)) :
                (a : MvPolynomial ι F) → FractionRing (MvPolynomial ι F))
              a)) :
        E) :
      E)
    ((aeval x : (a : MvPolynomial ι F) → E) a : E)

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
p : ↥(IntermediateField.adjoin F (range x))
⊢ (IsFractionRing.lift ⋯ : (a : FractionRing (MvPolynomial ι F)) → E)
      ((hx.reprField : (a : ↥(IntermediateField.adjoin F (range x))) → FractionRing (MvPolynomial ι F)) p :
        FractionRing (MvPolynomial ι F)) =
    (↑p : E)

Tactic:
Subtype.ext_iff.1 (AlgEquiv.apply_symm_apply hx.aevalEquivField p)

Premises used: AlgebraicIndependent.aevalEquivField, AlgEquiv.apply_symm_apply, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : AlgebraicIndependent F x
⊢ Eq (α := ↥(IntermediateField.adjoin F (range x)) →ₐ[F] E)
    (AlgHom.comp (IsFractionRing.liftAlgHom (K := FractionRing (MvPolynomial ι F)) ⋯) hx.reprField)
    (IntermediateField.val (IntermediateField.adjoin F (range x)))

Tactic:
AlgHom.ext <| hx.lift_reprField

Premises used: AlgebraicIndependent.lift_reprField, AlgHom.ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
⊢ AlgebraicIndependent S x

Tactic:
algebraicIndependent_of_finite_type'
    (Algebra.IsAlgebraic.injective_tower_top S hx.algebraMap_injective) fun t fin ind i hi ↦ ?_

Premises used: algebraicIndependent_of_finite_type', AlgebraicIndependent.algebraMap_injective, Algebra.IsAlgebraic.injective_tower_top
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
refine :
  ∀ (t : Set ι) (fin : t.Finite)
    (ind : AlgebraicIndependent.{u_1, u_5, u_4} S (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) (i : ι) (hi : i ∉ t),
    Transcendental (↥(adjoin S (x '' t))) (x i)
⊢ AlgebraicIndependent S x

Tactic:
refine algebraicIndependent_of_finite_type'
    (Algebra.IsAlgebraic.injective_tower_top S hx.algebraMap_injective) fun t fin ind i hi ↦ ?_

Premises used: algebraicIndependent_of_finite_type', AlgebraicIndependent.algebraMap_injective, Algebra.IsAlgebraic.injective_tower_top
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent.{u_1, u_5, u_4} S (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
⊢ x '' t ⊆ (↑(Subalgebra.restrictScalars R St) : Set A)

Tactic:
subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent.{u_1, u_5, u_4} S (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
⊢ x '' t ⊆ (↑(Subalgebra.restrictScalars R St) : Set A)

Tactic:
exact subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent.{u_1, u_5, u_4} S (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x_1 : Algebra ↥Rt ↥St := RingHom.toAlgebra (AlgHom.toRingHom.{u_2, u_4, u_4} (R := R) (Subalgebra.inclusion ⋯))
⊢ IsScalarTower (↥Rt) (↥St) A

Tactic:
have : IsScalarTower Rt St A := .of_algebraMap_eq fun ⟨y, _⟩ ↦ show y = y from rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent.{u_1, u_5, u_4} S (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x_1 : Algebra ↥Rt ↥St := RingHom.toAlgebra (AlgHom.toRingHom.{u_2, u_4, u_4} (R := R) (Subalgebra.inclusion ⋯))
this : IsScalarTower (↥Rt) (↥St) A
⊢ NoZeroDivisors.{u_4} ↥St

Tactic:
have : NoZeroDivisors St := (Set.image_eq_range _ _ ▸ ind.aevalEquiv)
    |>.symm.injective.noZeroDivisors _ (map_zero _) (map_mul _)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent.{u_1, u_5, u_4} S (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x_1 : Algebra ↥Rt ↥St := RingHom.toAlgebra (AlgHom.toRingHom.{u_2, u_4, u_4} (R := R) (Subalgebra.inclusion ⋯))
this_1 : IsScalarTower (↥Rt) (↥St) A
this : NoZeroDivisors.{u_4} ↥St
⊢ NoZeroDivisors.{u_4} ↥Rt

Tactic:
have : NoZeroDivisors Rt := (Subalgebra.inclusion_injective _).noZeroDivisors
    (algebraMap Rt St) (map_zero _) (map_mul _)