awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
rw : range x = range (Subtype.val (p := fun (x : A) ↦ x ∈ s) ∘ Set.inclusion (s := range x) (t := s) hxs)
⊢ range x = Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)
have rw₁ : range x = range (ι := (↑(range x) : Type w)) (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
Tactic: rw [← range_comp, val_comp_inclusion, Subtype.range_val]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
rw : range x = range (Subtype.val (p := fun (x : A) ↦ x ∈ s) ∘ Set.inclusion (s := range x) (t := s) hxs)
rw₁ : range x = range (ι := (↑(range x) : Type w)) (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
⊢ range x = Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)
have rw₂ : range x = range x
Tactic: rw [← range_comp, val_comp_inclusion, Subtype.range_val]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False
have rw : ∀
  (alg :
    Algebra.IsAlgebraic
      (↥(adjoin R (Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)))) A)
  (hxs' : ¬range x = s) (this : ¬s ⊆ range x) (a : A) (has : a ∈ s) (hax : a ∉ range x), False
Tactic: rw [show range x = Subtype.val '' range (Set.inclusion hxs) by
    rw [← range_comp, val_comp_inclusion, Subtype.range_val]] at alg
Cleared hypotheses: alg, hxs', this, a, has, hax
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg :
  Algebra.IsAlgebraic
    (↥(adjoin R (Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False
have refine : Subtype.mk (p := fun (x : A) ↦ x ∈ s) a has ∉ range (Set.inclusion (s := range x) (t := s) hxs)
Tactic: refine ind_s.transcendental_adjoin (s := range (inclusion hxs)) (i := ⟨a, has⟩) ?_ (alg.1 _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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)
have refine : Algebra.IsAlgebraic (↥(adjoin R (range ((⇑f : (a : S) → A) ∘ x)))) A
Tactic: refine hx.1.map (f := f) (FaithfulSMul.algebraMap_injective S A).injOn
    |>.isTranscendenceBasis_iff_isAlgebraic.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ Algebra.IsAlgebraic (↥(adjoin R (range ((⇑f : (a : S) → A) ∘ x)))) A
have rw : Algebra.IsAlgebraic (↥(Subalgebra.map f (adjoin R (range x)))) A
Tactic: rw [Set.range_comp, ← AlgHom.map_adjoin]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A
have this₁ : IsScalarTower.{v, w, w} (↥Rx) (↥(Subalgebra.map f Rx)) A
Tactic: haveI : IsScalarTower Rx (Rx.map f) A := .of_algebraMap_eq fun x ↦ rfl
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 (↥(Subalgebra.map f Rx)) A
have this₁ : Algebra.IsAlgebraic (↥Rx) S
Tactic: have : Algebra.IsAlgebraic Rx S := hx.isAlgebraic
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 (↥(Subalgebra.map f Rx)) A
have this₁ : Algebra.IsAlgebraic.{v, w} (↥Rx) A
Tactic: have : Algebra.IsAlgebraic Rx A := .trans _ S _
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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)
have refine : ∀ (H : ∀ (i : ι), IsAlgebraic S (v i)), Algebra.IsAlgebraic S A
Tactic: refine ⟨fun _ i ↦ Algebra.IsAlgebraic.isAlgebraic (v i), fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 S A
have this : Algebra.IsAlgebraic.{v, w} S ↥Sv
Tactic: have : Algebra.IsAlgebraic S Sv := by
    simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
have rw : Rv ≤ AlgHom.range (IsScalarTower.toAlgHom R S A) ⊔ adjoin R (range v)
Tactic: rw [Subalgebra.restrictScalars_adjoin]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ Algebra.IsAlgebraic S A
have le : Rv ≤ Subalgebra.restrictScalars R Sv
Tactic: have le : Rv ≤ Sv.restrictScalars R := by
    rw [Subalgebra.restrictScalars_adjoin]; exact le_sup_right
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ Algebra.IsAlgebraic S A
have this₁ : IsScalarTower (↥Rv) (↥Sv) A
Tactic: have : IsScalarTower Rv Sv A := .of_algebraMap_eq fun x ↦ rfl
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 S A
have this₁ : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
Tactic: have := hv.isAlgebraic
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 S A
have this₁ : Algebra.IsAlgebraic (↥Sv) A
Tactic: have : Algebra.IsAlgebraic Sv A := .extendScalars (Subalgebra.inclusion_injective le)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ IsTranscendenceBasis (ι := ι) R (A := MvPolynomial ι R) X
have refine : Algebra.IsAlgebraic (↥(adjoin R (range X))) (MvPolynomial ι R)
Tactic: refine isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.2 ⟨algebraicIndependent_X .., ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range X))) (MvPolynomial ι R)
have rw : Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)
Tactic: rw [adjoin_range_X]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
A : Type (max u_1 u) := MvPolynomial ι R
⊢ Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)
have this : Algebra.IsIntegral (↥⊤) A
Tactic: have := Algebra.isIntegral_of_surjective (R := (⊤ : Subalgebra R A)) (B := A) (⟨⟨·, ⟨⟩⟩, rfl⟩)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
⊢ IsTranscendenceBasis (ι := ι) R (A := MvPolynomial ι R) X
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
⊢ IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h : Nontrivial R
⊢ IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X
have have : ∀ (this : Unique ι), IsTranscendenceBasis R (A := Polynomial R) fun (x : ι) ↦ Polynomial.X
Tactic: have := (nonempty_unique ι).some
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
have 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}) → ι)))
Tactic: refine (isTranscendenceBasis_equiv (Equiv.equivPUnit.{_, 1} _).symm).mp <|
    (MvPolynomial.uniqueAlgEquiv R PUnit).symm.isTranscendenceBasis_iff.mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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)
    (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}) → ι)))
have 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
Tactic: convert! IsTranscendenceBasis.mvPolynomial PUnit R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
inst : CommRing R
inst_1 : Nonempty ι
inst_2 : Subsingleton ι
h : Nontrivial R
this : Unique ι
⊢ 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
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
have inl : Subsingleton R → IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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))
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
have inr : Nontrivial R → IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
have inl : ∀ (hx : Nonempty ι) (hy : IsTranscendenceBasis S y), Subsingleton R → Nonempty (ι' ⊕ ι)
Tactic: rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢
Cleared hypotheses: hx, hy, h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ IsTranscendenceBasis R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))
have inr : Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))) A
Tactic: rw [(hx.1.sumElim_comp hy.1).isTranscendenceBasis_iff_isAlgebraic]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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)
⊢ Eq (α := Subalgebra R A) (adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))
    (Subalgebra.restrictScalars R Rxy)
have 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))
Tactic: rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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))
⊢ Eq (α := Subalgebra R A) (adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))
    (Subalgebra.restrictScalars R Rxy)
have 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))
Tactic: rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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))
⊢ Eq (α := Subalgebra R A) (adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))
    (Subalgebra.restrictScalars R Rxy)
have 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))
Tactic: rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]