awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
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))

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
inl : Subsingleton R → IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
inr : Nontrivial R → IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Subsingleton R
inl : ∀ (hx : Nonempty ι) (hy : IsTranscendenceBasis S y), Subsingleton R → Nonempty (ι' ⊕ ι)
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))

Tactic:
rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢

Premises used: isTranscendenceBasis_iff_of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : Nonempty ι
hy : IsTranscendenceBasis S y
h : Subsingleton R
⊢ Nonempty (ι' ⊕ ι)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
inr : Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))) A
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))

Tactic:
rw [(hx.1.sumElim_comp hy.1).isTranscendenceBasis_iff_isAlgebraic]

Premises used: AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, AlgebraicIndependent.sumElim_comp, And.left
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
rw :
  Eq (α := Subalgebra R A) (adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))
    (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' range x ∪ range y))
rw₁ :
  Eq (α := Subalgebra R A) (adjoin R (range y ∪ range ((⇑(algebraMap S A) : (a : S) → A) ∘ x)))
    (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' range x ∪ range y))
rw₂ :
  Eq (α := Subalgebra R A) (adjoin R (range ((⇑(algebraMap S A) : (a : S) → A) ∘ x) ∪ range y))
    (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' range x ∪ range y))
rw₃ rw₄ :
  Eq (α := Subalgebra R A) (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' range x ∪ range y))
    (adjoin R ((⇑(algebraMap S A) : (a : S) → A) '' range x ∪ range y))
⊢ Eq (α := Subalgebra R A) (adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))
    (Subalgebra.restrictScalars R Rxy)

Tactic:
rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]

Premises used: Set.range_comp, Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin, Set.Sum.elim_range, Set.union_comm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
inr : Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))) A

Tactic:
rw [show adjoin R (range <| Sum.elim y (algebraMap S A ∘ x)) = Rxy.restrictScalars R by
    rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
inr : Algebra.IsAlgebraic (↥Rxy) A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) A

Tactic:
change Algebra.IsAlgebraic Rxy A

Premises used: Membership.mem, Subtype, Algebra.IsAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
⊢ Nontrivial S

Tactic:
have := hx.1.algebraMap_injective.nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this : Nontrivial S
⊢ Nontrivial A

Tactic:
have := hy.1.algebraMap_injective.nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this : Nontrivial A
⊢ Algebra.IsAlgebraic (↥(adjoin S (range y))) A

Tactic:
have := hy.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
this : Algebra.IsAlgebraic (↥(adjoin S (range y))) A
⊢ let Sy : Subalgebra S A := adjoin S (range y);
  Algebra.IsAlgebraic (↥Sy) A

Tactic:
set Sy := adjoin S (range y)

Premises used: Algebra.adjoin, Set.range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
refine : range y ⊆ (↑(Subalgebra.restrictScalars (↥Rx) Sy) : Set A)
⊢ Algebra ↥Rxy ↥Sy

Tactic:
refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra

Premises used: RingHom.toAlgebra
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
i : ι'
⊢ y i ∈ (↑(Subalgebra.restrictScalars (↥Rx) Sy) : Set A)

Tactic:
subset_adjoin (s := range y) ⟨i, rfl⟩

Premises used: Set.Mem, Algebra.subset_adjoin, Exists.intro, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
i : ι'
⊢ y i ∈ (↑(Subalgebra.restrictScalars (↥Rx) Sy) : Set A)

Tactic:
exact subset_adjoin (s := range y) ⟨i, rfl⟩

Premises used: Algebra.subset_adjoin, Exists.intro, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
⊢ IsScalarTower (↥Rxy) (↥Sy) A

Tactic:
have : IsScalarTower Rxy Sy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this : IsScalarTower (↥Rxy) (↥Sy) A
⊢ IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy

Tactic:
have : IsScalarTower Rx Rxy Sy := .of_algebraMap_eq fun ⟨a, _⟩ ↦ Subtype.ext rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
⊢ Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy

Tactic:
⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩

Premises used: IsAlgebraic, Membership.mem, Subtype, Algebra.IsAlgebraic.mk, Algebra.adjoin_induction, _private.0.IsTranscendenceBasis.sumElim_comp.match_2
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
refine_1 :
  ∀ (x : ↥Sy) (a : A) (ha : a ∈ Sy) (x : A) (hx : x ∈ range y),
    IsAlgebraic ↥Rxy (A := ↥Sy) (Subtype.mk (p := fun (x : A) ↦ x ∈ Sy) x ⋯)
refine_2 :
  ∀ (x : ↥Sy) (a : A) (ha : a ∈ Sy) (x : S),
    Injective.{v + 1, w + 1} (α := ↥Rx) (β := ↥Rxy) (⇑(algebraMap ↥Rx ↥Rxy) : (a : ↥Rx) → ↥Rxy)
refine_3 :
  ∀ (x : ↥Sy) (a : A) (ha : a ∈ Sy) (x : S),
    IsAlgebraic.{v, w} ↥Rx (A := ↥Sy)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ Sy) ((algebraMap S A : (a : S) → A) x) ⋯ : ↥Sy)
⊢ Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
x_2 : ↥Sy
a : A
ha : a ∈ Sy
i : ι'
⊢ IsAlgebraic ↥Rxy (A := ↥Sy) (Subtype.mk (p := fun (x : A) ↦ x ∈ Sy) (y i) ⋯)

Tactic:
isAlgebraic_algebraMap (⟨y i, subset_adjoin ⟨i, rfl⟩⟩ : Rxy)

Premises used: Set.Mem, Algebra.subset_adjoin, Subtype.mk, Exists.intro, isAlgebraic_algebraMap, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
x_2 : ↥Sy
a : A
ha : a ∈ Sy
i : ι'
⊢ IsAlgebraic ↥Rxy (A := ↥Sy) (Subtype.mk (p := fun (x : A) ↦ x ∈ Sy) (y i) ⋯)

Tactic:
exact isAlgebraic_algebraMap (⟨y i, subset_adjoin ⟨i, rfl⟩⟩ : Rxy)

Premises used: Algebra.subset_adjoin, Subtype.mk, Exists.intro, isAlgebraic_algebraMap, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
x_2 : ↥Sy
a : A
ha : a ∈ Sy
x_3 : S
⊢ Injective.{v + 1, w + 1} (α := ↥Rx) (β := ↥Rxy) (⇑(algebraMap ↥Rx ↥Rxy) : (a : ↥Rx) → ↥Rxy)

Tactic:
fun _ _ ↦ (Subtype.ext <| hy.1.algebraMap_injective <| Subtype.ext_iff.mp ·)

Premises used: AlgebraicIndependent.algebraMap_injective, Subtype.ext_iff, And.left, Iff.mp, Function.Injective, Subtype.ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
x_2 : ↥Sy
a : A
ha : a ∈ Sy
x_3 : S
⊢ Injective.{v + 1, w + 1} (α := ↥Rx) (β := ↥Rxy) (⇑(algebraMap ↥Rx ↥Rxy) : (a : ↥Rx) → ↥Rxy)

Tactic:
exact fun _ _ ↦ (Subtype.ext <| hy.1.algebraMap_injective <| Subtype.ext_iff.mp ·)

Premises used: AlgebraicIndependent.algebraMap_injective, And.left, Subtype.ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
x_2 : ↥Sy
a : A
ha : a ∈ Sy
x_3 : S
⊢ IsAlgebraic.{v, w} ↥Rx (A := ↥Sy)
    (Subtype.mk (p := fun (x : A) ↦ x ∈ Sy) ((algebraMap S A : (a : S) → A) x_3) ⋯ : ↥Sy)

Tactic:
(hx.isAlgebraic.1 _).algHom (IsScalarTower.toAlgHom Rx S Sy)

Premises used: Algebra.IsAlgebraic.isAlgebraic, Subsemiring.mk', Subsemiring.closure, IsAlgebraic.algHom, Set.Mem, IsScalarTower.toAlgHom, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
x_2 : ↥Sy
a : A
ha : a ∈ Sy
x_3 : S
⊢ IsAlgebraic.{v, w} ↥Rx (A := ↥Sy)
    (Subtype.mk (p := fun (x : A) ↦ x ∈ Sy) ((algebraMap S A : (a : S) → A) x_3) ⋯ : ↥Sy)

Tactic:
exact (hx.isAlgebraic.1 _).algHom (IsScalarTower.toAlgHom Rx S Sy)

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.algHom, IsScalarTower.toAlgHom, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : 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 : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra.{v, w} (↥Rx) A := adjoin (↥Rx) (range y)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this_3 : Algebra.IsAlgebraic (↥Sy) A
x_1 : Algebra ↥Rxy ↥Sy := RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this_4 : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
⊢ Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy

Tactic:
have : Algebra.IsAlgebraic Rxy Sy := by
    refine ⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
    · rintro _ ⟨i, rfl⟩; exact isAlgebraic_algebraMap (⟨y i, subset_adjoin ⟨i, rfl⟩⟩ : Rxy)
    · exact fun _ _ ↦ (Subtype.ext <| hy.1.algebraMap_injective <| Subtype.ext_iff.mp ·)
    · exact (hx.isAlgebraic.1 _).algHom (IsScalarTower.toAlgHom Rx S Sy)