awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
rw :
  IsAlgebraic ↥Rt (A := A)
    ((IsScalarTower.toAlgHom (↥Rt) (↥St) A : (a : ↥St) → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ St) y hy) : A)
⊢ IsAlgebraic (↥Rt) (Subtype.mk (p := fun (x : A) ↦ x ∈ St) y hy)

Tactic:
rw [← isAlgebraic_algHom_iff (IsScalarTower.toAlgHom Rt St A) Subtype.val_injective]

Premises used: isAlgebraic_algHom_iff, Subtype.val_injective, IsScalarTower.toAlgHom, Membership.mem, Subtype
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
change : IsAlgebraic (↥Rt) y
⊢ IsAlgebraic ↥Rt (A := A)
    ((IsScalarTower.toAlgHom (↥Rt) (↥St) A : (a : ↥St) → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ St) y hy) : A)

Tactic:
change IsAlgebraic Rt y

Premises used: IsAlgebraic, Membership.mem, Subtype
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
⊢ Nontrivial R

Tactic:
have := Algebra.IsAlgebraic.nontrivial R S
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
this : Nontrivial R
⊢ Nontrivial A

Tactic:
have := hx.algebraMap_injective.nontrivial
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
this_4 : Nontrivial R
this : Nontrivial A
z : S
x_3 x_4 : R
eq :
  Eq.{u_4 + 1} (α := ↥Rt) ((algebraMap R ↥Rt : (a : R) → ↥Rt) x_3 : ↥Rt) ((algebraMap R ↥Rt : (a : R) → ↥Rt) x_4 : ↥Rt)
⊢ x_3 = x_4

Tactic:
hx.algebraMap_injective congr($eq.1)

Premises used: congrArg, id, AlgebraicIndependent.algebraMap_injective, Subtype.val
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
this_4 : Nontrivial R
this : Nontrivial A
z : S
x_3 x_4 : R
eq :
  Eq.{u_4 + 1} (α := ↥Rt) ((algebraMap R ↥Rt : (a : R) → ↥Rt) x_3 : ↥Rt) ((algebraMap R ↥Rt : (a : R) → ↥Rt) x_4 : ↥Rt)
⊢ x_3 = x_4

Tactic:
exact hx.algebraMap_injective congr($eq.1)

Premises used: congrArg, id, AlgebraicIndependent.algebraMap_injective, Subtype.val
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
x_2 : ↥St
y : A
hy : y ∈ St
this_4 : Nontrivial R
this : Nontrivial A
⊢ IsAlgebraic (↥Rt) y

Tactic:
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
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this : NoZeroDivisors.{u_4} ↥Rt
⊢ 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⟩
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
this : Algebra.IsAlgebraic.{u_4, u_4} ↥Rt ↥St
change : Transcendental (↥St) (x i)
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Tactic:
change Transcendental St (x i)

Premises used: Membership.mem, Subtype, Transcendental
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
this : Algebra.IsAlgebraic.{u_4, u_4} ↥Rt ↥St
⊢ Transcendental (↥St) (x i)

Tactic:
(hx.transcendental_adjoin hi).extendScalars _

Premises used: AlgebraicIndependent.transcendental_adjoin, Transcendental.extendScalars
-- 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_2 : NoZeroDivisors.{u_4} ↥St
this_3 : NoZeroDivisors.{u_4} ↥Rt
this : Algebra.IsAlgebraic.{u_4, u_4} ↥Rt ↥St
⊢ Transcendental (↥St) (x i)

Tactic:
exact (hx.transcendental_adjoin hi).extendScalars _

Premises used: AlgebraicIndependent.transcendental_adjoin, Transcendental.extendScalars
-- 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
inst_8 : Algebra.IsIntegral R S
⊢ Nontrivial S

Tactic:
nontriviality S
-- 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
inst_8 : Algebra.IsIntegral R S
h : Nontrivial S
⊢ Nontrivial R

Tactic:
have := Module.nontrivial R S
-- 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
inst_8 : Algebra.IsIntegral R S
h : Nontrivial S
this : Nontrivial R
⊢ AlgebraicIndependent S x

Tactic:
hx.extendScalars S

Premises used: AlgebraicIndependent.extendScalars
-- 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
inst_8 : Algebra.IsIntegral R S
h : Nontrivial S
this : Nontrivial R
⊢ AlgebraicIndependent S x

Tactic:
exact hx.extendScalars S

Premises used: AlgebraicIndependent.extendScalars
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
inst_3 : IsDomain R
inst_4 : NoZeroDivisors A
⊢ AlgebraicIndependent (↥(Subalgebra.algebraicClosure R A)) x

Tactic:
hx.extendScalars _

Premises used: AlgebraicIndependent.extendScalars
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
inst_3 : NoZeroDivisors A
⊢ AlgebraicIndependent (↥(integralClosure R A)) x

Tactic:
hx.extendScalars_of_isIntegral _

Premises used: AlgebraicIndependent.extendScalars_of_isIntegral
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
F : Type u_5
E : Type u_6
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : ι → E
hx : AlgebraicIndependent F x
⊢ AlgebraicIndependent (↥(algebraicClosure F E)) x

Tactic:
hx.extendScalars _

Premises used: AlgebraicIndependent.extendScalars
-- 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
inst_8 : FaithfulSMul R S
inst_9 : Algebra.IsIntegral R S
⊢ AlgebraicIndependent R x ↔ AlgebraicIndependent S x

Tactic:
⟨(·.extendScalars_of_isIntegral _),
    (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

Premises used: AlgebraicIndependent.extendScalars_of_isIntegral, FaithfulSMul.algebraMap_injective, Iff.intro, AlgebraicIndependent.restrictScalars
-- 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
inst_8 : FaithfulSMul R S
inst_9 : Algebra.IsAlgebraic R S
⊢ AlgebraicIndependent R x ↔ AlgebraicIndependent S x

Tactic:
⟨(·.extendScalars _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

Premises used: FaithfulSMul.algebraMap_injective, Iff.intro, AlgebraicIndependent.restrictScalars, AlgebraicIndependent.extendScalars
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
F : Type u_2
E : Type u_3
S : Type u_5
s : Set E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Ring S
inst_4 : Algebra E S
x : S
⊢ IsAlgebraic.{u_3, u_5} (↥(adjoin F s)) x ↔ IsAlgebraic.{u_3, u_5} (↥(Algebra.adjoin F s)) x

Tactic:
(IsAlgebraic.isAlgebraic_iff ..).symm

Premises used: Algebra.IsAlgebraic.isAlgebraic_iff, Iff.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
F : Type u_2
E : Type u_3
S : Type u_5
s : Set E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Ring S
inst_4 : Algebra E S
⊢ Algebra.IsAlgebraic.{u_3, u_5} (↥(adjoin F s)) S ↔ Algebra.IsAlgebraic.{u_3, u_5} (↥(Algebra.adjoin F s)) S

Tactic:
(IsAlgebraic.isAlgebraic_iff_top ..).symm

Premises used: Algebra.IsAlgebraic.isAlgebraic_iff_top, Iff.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
F : Type u_2
E : Type u_3
R : Type u_4
s : Set E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : CommRing R
inst_4 : Algebra R F
inst_5 : Algebra R E
inst_6 : IsScalarTower R F E
⊢ Algebra.IsAlgebraic.{u_4, u_3} R ↥(adjoin F s) ↔ Algebra.IsAlgebraic.{u_4, u_3} R ↥(Algebra.adjoin F s)

Tactic:
IsAlgebraic.isAlgebraic_iff_bot ..

Premises used: Algebra.IsAlgebraic.isAlgebraic_iff_bot
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
F : Type u_2
E : Type u_3
S : Type u_5
s : Set E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Ring S
inst_4 : Algebra E S
x : S
⊢ Transcendental.{u_3, u_5} (↥(adjoin F s)) x ↔ Transcendental.{u_3, u_5} (↥(Algebra.adjoin F s)) x

Tactic:
(IsAlgebraic.transcendental_iff ..).symm

Premises used: Algebra.IsAlgebraic.transcendental_iff, Iff.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
S : Type u_5
s : Set E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : CommRing S
inst_4 : Algebra E S
x : ι → S
⊢ AlgebraicIndependent.{u_1, u_3, u_5} (↥(adjoin F s)) x ↔
    AlgebraicIndependent.{u_1, u_3, u_5} (↥(Algebra.adjoin F s)) x

Tactic:
(Algebra.IsAlgebraic.algebraicIndependent_iff ..).symm

Premises used: Algebra.IsAlgebraic.algebraicIndependent_iff, Iff.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Goal:
ι : Type u_1
F : Type u_2
E : Type u_3
S : Type u_5
s : Set E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : CommRing S
inst_4 : Algebra E S
x : ι → S
⊢ IsTranscendenceBasis.{u_1, u_3, u_5} (↥(adjoin F s)) x ↔
    IsTranscendenceBasis.{u_1, u_3, u_5} (↥(Algebra.adjoin F s)) x

Tactic:
(Algebra.IsAlgebraic.isTranscendenceBasis_iff ..).symm

Premises used: Algebra.IsAlgebraic.isTranscendenceBasis_iff, Iff.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ AlgebraicIndependent R x ↔
    Eq (α := Ideal (MvPolynomial ι R)) (RingHom.ker (F := MvPolynomial ι R →+* A) (AlgHom.toRingHom (aeval x))) ⊥

Tactic:
RingHom.injective_iff_ker_eq_bot _

Premises used: AlgebraicIndependent, MvPolynomial.aeval, MvPolynomial.eval₂Hom, RingHom.injective_iff_ker_eq_bot, Ideal.comap, RingHom.ker
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)
rw₁ 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)
⊢ AlgebraicIndependent R x ↔ 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]

Premises used: algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
ι' : Type u_1
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
inst_5 : FaithfulSMul R A
⊢ Nonempty.{max 1 (v + 1)} { s : Set A // AlgebraicIndepOn R _root_.id s }

Tactic:
⟨∅, algebraicIndependent_empty_type_iff.mpr <| FaithfulSMul.algebraMap_injective R A⟩

Premises used: Iff.mpr, Nonempty.intro, Subtype.mk, FaithfulSMul.algebraMap_injective, EmptyCollection.emptyCollection, algebraicIndependent_empty_type_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
simpa [Function.comp_def] using
    (Injective.of_comp_iff (algebraicIndependent_iff_injective_aeval.1 hx) MvPolynomial.C).2
      (MvPolynomial.C_injective _ _)

Premises used: Iff.mpr, Function.comp_def, algebraicIndependent_iff_injective_aeval, Iff.mp, MvPolynomial.C_injective, Function.Injective.of_comp_iff, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
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)
⊢ Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
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:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)

Tactic:
have : Finsupp.linearCombination R x =
      (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) := by
    ext
    simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)
rw :
  Injective (α := ι →₀ R) (β := A)
    (⇑(AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A) : (a : ι →₀ R) → A)
⊢ Injective (α := ι →₀ R) (β := A) (⇑(Finsupp.linearCombination R x) : (a : ι →₀ R) → A)

Tactic:
rw [this]