awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
⊢ IsTranscendenceBasis R x ↔ AlgebraicIndependent R x ∧ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
⟨fun h ↦ ⟨h.1, h.1.isTranscendenceBasis_iff_isAlgebraic.mp h⟩,
    fun ⟨ind, alg⟩ ↦ ind.isTranscendenceBasis_iff_isAlgebraic.mpr alg⟩

Premises used: Iff.mpr, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, IsTranscendenceBasis, And.left, And.intro, Iff.intro, Iff.mp, _private.0.isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.match_1
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
⊢ IsTranscendenceBasis.{u, u_1, w} R (A := A) ((⇑(algebraMap S A) : (a : S) → A) ∘ x)

Tactic:
hx.1.map (f := f) (FaithfulSMul.algebraMap_injective S A).injOn
    |>.isTranscendenceBasis_iff_isAlgebraic.mpr ?_

Premises used: Iff.mpr, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, Function.Injective.injOn, AlgebraicIndependent.map, And.left, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
refine : Algebra.IsAlgebraic (↥(adjoin R (range ((⇑f : (a : S) → A) ∘ x)))) A
⊢ IsTranscendenceBasis.{u, u_1, w} R (A := A) ((⇑(algebraMap S A) : (a : S) → A) ∘ x)

Tactic:
refine hx.1.map (f := f) (FaithfulSMul.algebraMap_injective S A).injOn
    |>.isTranscendenceBasis_iff_isAlgebraic.mpr ?_

Premises used: Iff.mpr, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, Function.Injective.injOn, AlgebraicIndependent.map, And.left, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
rw : Algebra.IsAlgebraic (↥(Subalgebra.map f (adjoin R (range x)))) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range ((⇑f : (a : S) → A) ∘ x)))) A

Tactic:
rw [Set.range_comp, ← AlgHom.map_adjoin]

Premises used: Set.range_comp, AlgHom.map_adjoin
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
set :
  let Rx : Subalgebra R S := adjoin R (range x);
  Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f (adjoin R (range x)))) A

Tactic:
set Rx := adjoin R (range x)

Premises used: Algebra.adjoin, Set.range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : AlgEquiv.{u_1, v, w} R ↥Rx ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this : Algebra.{v, w} ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
⊢ IsScalarTower.{v, w, w} (↥Rx) (↥(Subalgebra.map f Rx)) A

Tactic:
haveI : IsScalarTower Rx (Rx.map f) A := .of_algebraMap_eq fun x ↦ rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : AlgEquiv.{u_1, v, w} R ↥Rx ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this_1 : Algebra.{v, w} ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower.{v, w, w} (↥Rx) (↥(Subalgebra.map f Rx)) A
⊢ Algebra.IsAlgebraic (↥Rx) S

Tactic:
have : Algebra.IsAlgebraic Rx S := hx.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : AlgEquiv.{u_1, v, w} R ↥Rx ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this_1 : Algebra.{v, w} ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
this_2 : IsScalarTower.{v, w, w} (↥Rx) (↥(Subalgebra.map f Rx)) A
this : Algebra.IsAlgebraic (↥Rx) S
⊢ Algebra.IsAlgebraic.{v, w} (↥Rx) A

Tactic:
have : Algebra.IsAlgebraic Rx A := .trans _ S _
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : AlgEquiv.{u_1, v, w} R ↥Rx ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this_1 : Algebra.{v, w} ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
this_2 : IsScalarTower.{v, w, w} (↥Rx) (↥(Subalgebra.map f Rx)) A
this_3 : Algebra.IsAlgebraic (↥Rx) S
this : Algebra.IsAlgebraic.{v, w} (↥Rx) A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A

Tactic:
.extendScalars e.injective

Premises used: Algebra.IsAlgebraic.extendScalars, AlgEquiv.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors S
inst_9 : Algebra.IsAlgebraic S A
inst_10 : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : AlgEquiv.{u_1, v, w} R ↥Rx ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this_1 : Algebra.{v, w} ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
this_2 : IsScalarTower.{v, w, w} (↥Rx) (↥(Subalgebra.map f Rx)) A
this_3 : Algebra.IsAlgebraic (↥Rx) S
this : Algebra.IsAlgebraic.{v, w} (↥Rx) A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A

Tactic:
exact .extendScalars e.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
⊢ Algebra.IsAlgebraic S A ↔ ∀ (i : ι), IsAlgebraic S (v i)

Tactic:
⟨fun _ i ↦ Algebra.IsAlgebraic.isAlgebraic (v i), fun H ↦ ?_⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, Iff.intro
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
refine : ∀ (H : ∀ (i : ι), IsAlgebraic S (v i)), Algebra.IsAlgebraic S A
⊢ Algebra.IsAlgebraic S A ↔ ∀ (i : ι), IsAlgebraic S (v i)

Tactic:
refine ⟨fun _ i ↦ Algebra.IsAlgebraic.isAlgebraic (v i), fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
⊢ Algebra.IsAlgebraic.{v, w} S ↥Sv

Tactic:
simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]

Premises used: Algebra.isAlgebraic_adjoin_iff, Subalgebra.isAlgebraic_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
⊢ Algebra.IsAlgebraic.{v, w} S ↥Sv

Tactic:
have : Algebra.IsAlgebraic S Sv := by
    simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic.{v, w} S ↥Sv
rw : Rv ≤ AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R (range v)
⊢ Rv ≤ Subalgebra.restrictScalars R Sv

Tactic:
rw [Subalgebra.restrictScalars_adjoin]

Premises used: Algebra.Subalgebra.restrictScalars_adjoin
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic.{v, w} S ↥Sv
⊢ Rv ≤ AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R (range v)

Tactic:
le_sup_right

Premises used: Set.Mem, setOf, le_sup_right
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic.{v, w} S ↥Sv
⊢ Rv ≤ AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R (range v)

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic.{v, w} S ↥Sv
⊢ Rv ≤ Subalgebra.restrictScalars R Sv

Tactic:
have le : Rv ≤ Sv.restrictScalars R := by
    rw [Subalgebra.restrictScalars_adjoin]; exact le_sup_right
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this_1 : Algebra.IsAlgebraic.{v, w} S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
⊢ IsScalarTower (↥Rv) (↥Sv) A

Tactic:
have : IsScalarTower Rv Sv A := .of_algebraMap_eq fun x ↦ rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this_1 : Algebra.IsAlgebraic.{v, w} S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this_2 : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this_3 : IsScalarTower (↥Rv) (↥Sv) A
this : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range v))) A

Tactic:
have := hv.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this_1 : Algebra.IsAlgebraic.{v, w} S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this_2 : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this_3 : IsScalarTower (↥Rv) (↥Sv) A
this_4 : Nontrivial R
this : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
⊢ Algebra.IsAlgebraic (↥Sv) A

Tactic:
have : Algebra.IsAlgebraic Sv A := .extendScalars (Subalgebra.inclusion_injective le)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this_1 : Algebra.IsAlgebraic.{v, w} S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this_2 : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this_3 : IsScalarTower (↥Rv) (↥Sv) A
this_4 : Nontrivial R
this_5 : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
this : Algebra.IsAlgebraic (↥Sv) A
⊢ Algebra.IsAlgebraic S A

Tactic:
.trans _ Sv _

Premises used: Membership.mem, Algebra.IsAlgebraic.trans, Subtype
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
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 : IsDomain S
inst_8 : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this_1 : Algebra.IsAlgebraic.{v, w} S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this_2 : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this_3 : IsScalarTower (↥Rv) (↥Sv) A
this_4 : Nontrivial R
this_5 : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
this : Algebra.IsAlgebraic (↥Sv) A
⊢ Algebra.IsAlgebraic S A

Tactic:
exact .trans _ Sv _
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ IsTranscendenceBasis (ι := ι) R (A := MvPolynomial ι R) X

Tactic:
isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.2 ⟨algebraicIndependent_X .., ?_⟩

Premises used: Iff.mpr, And.intro, MvPolynomial.algebraicIndependent_X, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
refine : Algebra.IsAlgebraic (↥(adjoin R (range X))) (MvPolynomial ι R)
⊢ IsTranscendenceBasis (ι := ι) R (A := MvPolynomial ι R) X

Tactic:
refine isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.2 ⟨algebraicIndependent_X .., ?_⟩

Premises used: Iff.mpr, And.intro, MvPolynomial.algebraicIndependent_X, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
rw : Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)
⊢ Algebra.IsAlgebraic (↥(adjoin R (range X))) (MvPolynomial ι R)

Tactic:
rw [adjoin_range_X]

Premises used: MvPolynomial.adjoin_range_X
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
A : Type (max u_1 u) := MvPolynomial ι R
⊢ Algebra.IsIntegral (↥⊤) A

Tactic:
have := Algebra.isIntegral_of_surjective (R := (⊤ : Subalgebra R A)) (B := A) (⟨⟨·, ⟨⟩⟩, rfl⟩)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
A : Type (max u_1 u) := MvPolynomial ι R
this : Algebra.IsIntegral (↥⊤) A
⊢ Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
h : Nontrivial R
⊢ IsTranscendenceBasis (ι := ι) R (A := MvPolynomial ι R) X

Tactic:
.mvPolynomial ι R

Premises used: IsTranscendenceBasis.mvPolynomial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
h : Nontrivial R
⊢ IsTranscendenceBasis (ι := ι) R (A := MvPolynomial ι R) X

Tactic:
exact .mvPolynomial ι R
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h : Nontrivial R
have : ∀ (this : Unique ι), IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X
⊢ IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X

Tactic:
have := (nonempty_unique ι).some
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h : Nontrivial R
this : Unique ι
⊢ IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X

Tactic:
(isTranscendenceBasis_equiv (Equiv.equivPUnit.{_, 1} _).symm).mp <|
    (MvPolynomial.uniqueAlgEquiv R PUnit).symm.isTranscendenceBasis_iff.mp ?_

Premises used: AlgEquiv.isTranscendenceBasis_iff, AlgEquiv.symm, isTranscendenceBasis_equiv, MvPolynomial.uniqueAlgEquiv, PUnit, Iff.mp, Equiv.symm, Equiv.equivPUnit
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h : Nontrivial R
this : Unique ι
refine :
  IsTranscendenceBasis (ι := PUnit.{1}) R (A := MvPolynomial PUnit.{1} R)
    (Function.comp (β := Polynomial R)
      (⇑(AlgEquiv.symm (uniqueAlgEquiv R PUnit.{1})) : (a : Polynomial R) → MvPolynomial PUnit.{1} R)
      ((fun (x : ι) ↦ Polynomial.X) ∘ (⇑(Equiv.equivPUnit ι).symm : (a : PUnit.{1}) → ι)))
⊢ IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X

Tactic:
refine (isTranscendenceBasis_equiv (Equiv.equivPUnit.{_, 1} _).symm).mp <|
    (MvPolynomial.uniqueAlgEquiv R PUnit).symm.isTranscendenceBasis_iff.mp ?_

Premises used: AlgEquiv.isTranscendenceBasis_iff, AlgEquiv.symm, isTranscendenceBasis_equiv, MvPolynomial.uniqueAlgEquiv, PUnit, Iff.mp, Equiv.symm, Equiv.equivPUnit
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h : Nontrivial R
this : Unique ι
⊢ IsTranscendenceBasis (ι := PUnit.{1}) R (A := MvPolynomial PUnit.{1} R) X

Tactic:
IsTranscendenceBasis.mvPolynomial PUnit R

Premises used: PUnit, IsTranscendenceBasis.mvPolynomial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h_1 : Nontrivial R
this : Unique ι
h :
  Eq (α := PUnit.{1} → MvPolynomial PUnit.{1} R)
    (Function.comp (β := Polynomial R)
      (⇑(AlgEquiv.symm (uniqueAlgEquiv R PUnit.{1})) : (a : Polynomial R) → MvPolynomial PUnit.{1} R)
      ((fun (x : ι) ↦ Polynomial.X) ∘ (⇑(Equiv.equivPUnit ι).symm : (a : PUnit.{1}) → ι)))
    X
⊢ IsTranscendenceBasis (ι := PUnit.{1}) R (A := MvPolynomial PUnit.{1} R)
    (Function.comp (β := Polynomial R)
      (⇑(AlgEquiv.symm (uniqueAlgEquiv R PUnit.{1})) : (a : Polynomial R) → MvPolynomial PUnit.{1} R)
      ((fun (x : ι) ↦ Polynomial.X) ∘ (⇑(Equiv.equivPUnit ι).symm : (a : PUnit.{1}) → ι)))

Tactic:
convert! IsTranscendenceBasis.mvPolynomial PUnit R

Premises used: PUnit, IsTranscendenceBasis.mvPolynomial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h_1 : Nontrivial R
this : Unique ι
h :
  ∀ (x : PUnit.{1}) (m : PUnit.{1} →₀ ℕ),
    Eq (α := R)
      (coeff m
        (Function.comp (β := Polynomial R)
          (⇑(AlgEquiv.symm (uniqueAlgEquiv R PUnit.{1})) : (a : Polynomial R) → MvPolynomial PUnit.{1} R)
          ((fun (x : ι) ↦ Polynomial.X) ∘ (⇑(Equiv.equivPUnit ι).symm : (a : PUnit.{1}) → ι)) x))
      (coeff m (X x))
⊢ Eq (α := PUnit.{1} → MvPolynomial PUnit.{1} R)
    (Function.comp (β := Polynomial R)
      (⇑(AlgEquiv.symm (uniqueAlgEquiv R PUnit.{1})) : (a : Polynomial R) → MvPolynomial PUnit.{1} R)
      ((fun (x : ι) ↦ Polynomial.X) ∘ (⇑(Equiv.equivPUnit ι).symm : (a : PUnit.{1}) → ι)))
    X

Tactic:
ext