awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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
⊢ 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
have this : q.IsPrime
Tactic: have := hq.1.1
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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
⊢ 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
have this₁ : Ring.KrullDimLE.{u_2} 0 (Localization.AtPrime q)
Tactic: have : Ring.KrullDimLE 0 (Localization.AtPrime q) := .of_isLocalization _ hq _
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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 ⋯
⊢ 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)
have 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)
Tactic: rw [← Ideal.mem_bot, ← IsLocalRing.maximalIdeal_eq_bot,
      ← Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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 ⋯
⊢ 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
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ 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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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 ⧸ 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
have a : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff i) : S) u ∈ q
Tactic: simp only [coeff_mul_C, coeff_map, coeff_zero, ← Ideal.Quotient.mk_algebraMap, ← map_mul,
    Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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 ∈ q
have this₁ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Adjoin (goal)
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)) ⋯
⊢ Eq (α := MvPolynomial ι F →+* E)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
      (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))))
    (↑(aeval x) : MvPolynomial ι F →+* E)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Adjoin (goal)
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)
⊢ Eq (α := MvPolynomial ι F →+* E)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑i : FractionRing (MvPolynomial ι F) →+* E)
      (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))))
    (↑(aeval x) : MvPolynomial ι F →+* E)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (goal)
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
have 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)
Tactic: refine algebraicIndependent_of_finite_type'
    (Algebra.IsAlgebraic.injective_tower_top S hx.algebraMap_injective) fun t fin ind i hi ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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 ⋯))
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)
have this : IsScalarTower (↥Rt) (↥St) A
Tactic: have : IsScalarTower Rt St A := .of_algebraMap_eq fun ⟨y, _⟩ ↦ show y = y from rfl
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)
have this₁ : NoZeroDivisors.{u_4} ↥St
Tactic: have : NoZeroDivisors St := (Set.image_eq_range _ _ ▸ ind.aevalEquiv)
    |>.symm.injective.noZeroDivisors _ (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)
have this₁ : NoZeroDivisors.{u_4} ↥Rt
Tactic: have : NoZeroDivisors Rt := (Subalgebra.inclusion_injective _).noZeroDivisors
    (algebraMap Rt St) (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (goal)
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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic (↥Rt) (Subtype.mk (p := fun (x : A) ↦ x ∈ St) y hy)
have rw : IsAlgebraic ↥Rt (A := A)
  ((IsScalarTower.toAlgHom (↥Rt) (↥St) A : (a : ↥St) → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ St) y hy) : A)
Tactic: rw [← isAlgebraic_algHom_iff (IsScalarTower.toAlgHom Rt St A) Subtype.val_injective]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (goal)
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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic ↥Rt (A := A)
    ((IsScalarTower.toAlgHom (↥Rt) (↥St) A : (a : ↥St) → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ St) y hy) : A)
have change : IsAlgebraic (↥Rt) y
Tactic: change IsAlgebraic Rt y
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic (↥Rt) y
have this₁ : Nontrivial R
Tactic: have := Algebra.IsAlgebraic.nontrivial R S
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
this : Nontrivial R
⊢ IsAlgebraic (↥Rt) y
have this₁ : Nontrivial A
Tactic: have := hx.algebraMap_injective.nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)
have this₁ : Algebra.IsAlgebraic.{u_4, u_4} ↥Rt ↥St
Tactic: have : Algebra.IsAlgebraic Rt St := ⟨fun ⟨y, hy⟩ ↦ by
    rw [← isAlgebraic_algHom_iff (IsScalarTower.toAlgHom Rt St A) Subtype.val_injective]
    change IsAlgebraic Rt y
    have := Algebra.IsAlgebraic.nontrivial R S
    have := hx.algebraMap_injective.nontrivial
    exact adjoin_induction (fun _ h ↦ isAlgebraic_algebraMap (⟨_, subset_adjoin h⟩ : Rt))
      (fun z ↦ ((alg.1 z).algHom (IsScalarTower.toAlgHom R S A)).extendScalars fun _ _ eq ↦ by
        exact hx.algebraMap_injective congr($eq.1)) (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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
inst_8 : Algebra.IsIntegral R S
⊢ AlgebraicIndependent S x
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure (hypothesis)
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
inst_8 : Algebra.IsIntegral R S
h : Nontrivial S
⊢ AlgebraicIndependent S x
have this : Nontrivial R
Tactic: have := Module.nontrivial R S
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsEmpty ι
⊢ AlgebraicIndependent R x ↔ Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have rw : Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A) ↔
  Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsEmpty ι
rw :
  Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A) ↔
    Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ AlgebraicIndependent R x ↔ Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
have rw₁ : Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ↔
  Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
Tactic: rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
⊢ Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
have h : ∀ (a : ι),
  Eq.{v + 1} (α := A) ((Finsupp.linearCombination R x ∘ₗ Finsupp.lsingle a : (a : R) → A) 1 : A)
    ((((AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X) ∘ₗ Finsupp.lsingle a : R →ₗ[R] A) : (a : R) → A)
        1 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
⊢ Injective (α := ι →₀ R) (β := A) (⇑(Finsupp.linearCombination R x) : (a : ι →₀ R) → A)
have this : Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
  (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
Tactic: have : Finsupp.linearCombination R x =
      (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) := by
    ext
    simp
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
this :
  Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
⊢ Injective (α := ι →₀ R) (β := A) (⇑(Finsupp.linearCombination R x) : (a : ι →₀ R) → A)
have rw : Injective (α := ι →₀ R) (β := A)
  (⇑(AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A) : (a : ι →₀ R) → A)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
this :
  Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
⊢ Injective (α := ι →₀ R) (β := A)
    (⇑(AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A) : (a : ι →₀ R) → A)
have refine : Injective (α := ι →₀ R) (β := MvPolynomial ι R) (⇑(Finsupp.linearCombination R X) : (a : ι →₀ R) → MvPolynomial ι R)
Tactic: refine (algebraicIndependent_iff_injective_aeval.mp hx).comp ?_