awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_5 : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
this : Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
.trans _ Sy _

Premises used: Membership.mem, Algebra.IsAlgebraic.trans, 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_5 : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
this : Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
exact .trans _ Sy _
-- 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
hx : IsTranscendenceBasis R x
⊢ IsEmpty ι ↔ Algebra.IsAlgebraic R A

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ hx.1.isEmpty_of_isAlgebraic⟩

Premises used: AlgebraicIndependent.isEmpty_of_isAlgebraic, And.left, Iff.intro
-- 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
hx : IsTranscendenceBasis R x
refine : IsEmpty ι → Algebra.IsAlgebraic R A
⊢ IsEmpty ι ↔ Algebra.IsAlgebraic R A

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ hx.1.isEmpty_of_isAlgebraic⟩
-- 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
hx : IsTranscendenceBasis R x
h : IsEmpty ι
⊢ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
have := hx.isAlgebraic
-- 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
hx : IsTranscendenceBasis R x
h : IsEmpty ι
this : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
⊢ Algebra.IsAlgebraic (↥⊥) A

Tactic:
rw [Set.range_eq_empty x, adjoin_empty] at this

Premises used: Set.range_eq_empty, Algebra.adjoin_empty
-- 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
hx : IsTranscendenceBasis R x
h : IsEmpty ι
this : Algebra.IsAlgebraic (↥⊥) A
⊢ Algebra.IsAlgebraic R A

Tactic:
algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left R A

Premises used: Subalgebra.algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
-- 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
hx : IsTranscendenceBasis R x
h : IsEmpty ι
this : Algebra.IsAlgebraic (↥⊥) A
⊢ Algebra.IsAlgebraic R A

Tactic:
exact algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left R A

Premises used: Subalgebra.algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
-- 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
hx : IsTranscendenceBasis R x
rw : ¬IsEmpty ι ↔ Algebra.Transcendental R A
rw₁ : ¬IsEmpty ι ↔ ¬Algebra.IsAlgebraic R A
rw₂ rw₃ : ¬Algebra.IsAlgebraic R A ↔ ¬Algebra.IsAlgebraic R A
⊢ Nonempty ι ↔ Algebra.Transcendental R A

Tactic:
rw [← not_isEmpty_iff, Algebra.transcendental_iff_not_isAlgebraic, hx.isEmpty_iff_isAlgebraic]

Premises used: Algebra.transcendental_iff_not_isAlgebraic, IsTranscendenceBasis.isEmpty_iff_isAlgebraic, not_isEmpty_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : IsTranscendenceBasis F x
⊢ Algebra.IsAlgebraic (↥(adjoin F (range x))) E

Tactic:
haveI := hx.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (range x))) E
set :
  let S := range x;
  ∀ (this : Algebra.IsAlgebraic (↥(adjoin F S)) E), Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Tactic:
set S := range x

Premises used: Set.range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this_1 : Algebra.IsAlgebraic (↥(adjoin F S)) E
this : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
⊢ IsScalarTower (↥(adjoin F S)) (↥(IntermediateField.adjoin F S)) E

Tactic:
haveI : IsScalarTower (adjoin F S) (IntermediateField.adjoin F S) E :=
    IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this_1 : Algebra.IsAlgebraic (↥(adjoin F S)) E
this_2 : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this : IsScalarTower (↥(adjoin F S)) (↥(IntermediateField.adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Tactic:
Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

Premises used: Algebra.IsAlgebraic.extendScalars, Subalgebra.inclusion_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this_1 : Algebra.IsAlgebraic (↥(adjoin F S)) E
this_2 : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Subalgebra.inclusion ⋯))
this : IsScalarTower (↥(adjoin F S)) (↥(IntermediateField.adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Tactic:
exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

Premises used: Algebra.IsAlgebraic.extendScalars
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ¬Maximal (AlgebraicIndepOn R _root_.id) I
B_base : Maximal (AlgebraicIndepOn R _root_.id) B
contrapose! :
  ∀ (h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)),
    Maximal (AlgebraicIndepOn R _root_.id) I
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Maximal (AlgebraicIndepOn R _root_.id) B
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
rw :
  ∀ (B_base : IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ B }) R (Subtype.val (p := fun (x : A) ↦ x ∈ B)))
    (h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)),
    IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
⊢ Maximal (AlgebraicIndepOn R _root_.id) I

Tactic:
rw [← isTranscendenceBasis_iff_maximal] at B_base ⊢

Premises used: isTranscendenceBasis_iff_maximal
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ B }) R (Subtype.val (p := fun (x : A) ↦ x ∈ B))
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
inl :
  Subsingleton R → IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
inr :
  Nontrivial R → IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))

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
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ B }) R (Subtype.val (p := fun (x : A) ↦ x ∈ B))
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Subsingleton R
inl :
  ∀ (B_base : Nonempty.{w + 1} { x : A // x ∈ B })
    (h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)),
    Subsingleton R → Nonempty.{w + 1} { x : A // x ∈ I }
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))

Tactic:
rw [isTranscendenceBasis_iff_of_subsingleton] at B_base ⊢

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
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty.{w + 1} { x : A // x ∈ B }
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Subsingleton R
inl : ∀ (this : ¬Nonempty.{w + 1} { x : A // x ∈ I }), False
⊢ Nonempty.{w + 1} { x : A // x ∈ I }

Tactic:
by_contra this
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty.{w + 1} { x : A // x ∈ B }
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Subsingleton R
this : ¬Nonempty.{w + 1} { x : A // x ∈ I }
inl : ∀ (b : A) (hb : b ∈ B), False
⊢ False

Tactic:
have ⟨b, hb⟩ := B_base
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty.{w + 1} { x : A // x ∈ B }
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Subsingleton R
this : ¬Nonempty.{w + 1} { x : A // x ∈ I }
b : A
hb : b ∈ B
⊢ False

Tactic:
h b ⟨hb, fun hbI ↦ this ⟨b, hbI⟩⟩ .of_subsingleton

Premises used: Nonempty.intro, Subtype.mk, And.intro, AlgebraicIndependent.of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty.{w + 1} { x : A // x ∈ B }
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Subsingleton R
this : ¬Nonempty.{w + 1} { x : A // x ∈ I }
b : A
hb : b ∈ B
⊢ False

Tactic:
exact h b ⟨hb, fun hbI ↦ this ⟨b, hbI⟩⟩ .of_subsingleton

Premises used: Nonempty.intro, Subtype.mk, And.intro, AlgebraicIndependent.of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ B }) R (Subtype.val (p := fun (x : A) ↦ x ∈ B))
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
inr : Algebra.IsAlgebraic (↥(adjoin R (range fun (i : (↑I : Type w)) ↦ _root_.id (↑i : A)))) A
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))

Tactic:
apply I_ind.isTranscendenceBasis_iff_isAlgebraic.mpr

Premises used: Iff.mpr, AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ B }) R (Subtype.val (p := fun (x : A) ↦ x ∈ B))
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range (ι := { x : A // x ∈ B }) (Subtype.val (p := fun (x : A) ↦ x ∈ B))))) A

Tactic:
replace B_base := B_base.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R (range (ι := { x : A // x ∈ B }) (Subtype.val (p := fun (x : A) ↦ x ∈ B))))) A
inr : ∀ (B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A), Algebra.IsAlgebraic (↥(adjoin R I)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun (i : (↑I : Type w)) ↦ (↑i : A)))) A

Tactic:
rw [Subtype.range_val] at B_base ⊢

Premises used: Subtype.range_val
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A

Tactic:
⟨fun a ↦ (B_base.1 a).adjoin_of_forall_isAlgebraic fun x hx ↦ ?_⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, Algebra.IsAlgebraic.mk, IsAlgebraic.adjoin_of_forall_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
inr : ∀ (a x : A) (hx : x ∈ B \ I), IsAlgebraic (↥(adjoin R I)) x
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A

Tactic:
refine ⟨fun a ↦ (B_base.1 a).adjoin_of_forall_isAlgebraic fun x hx ↦ ?_⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x_1 : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
inr : ∀ (h : ¬IsAlgebraic (↥(adjoin R I)) x), ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)
⊢ IsAlgebraic (↥(adjoin R I)) x

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x_1 : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
rwa rwa₁ rwa₂ rwa₃ : Transcendental (↥(adjoin R I)) (_root_.id x)
⊢ Transcendental (↥(adjoin R (_root_.id '' I))) (_root_.id x)

Tactic:
rwa [image_id]

Premises used: Set.image_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x_1 : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)

Tactic:
exact ⟨x, hx, I_ind.insert <| by rwa [image_id]⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
B : Set A
simp_rw : Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B
⊢ (fun (s : Set A) ↦
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)))
      B ↔
    (indepMatroid R A).matroid.IsBase B

Tactic:
simp_rw [Matroid.isBase_iff_maximal_indep, isTranscendenceBasis_iff_maximal]

Premises used: isTranscendenceBasis_iff_maximal, Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
B : Set A
⊢ Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B

Tactic:
rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
⊢ (matroid R A).E = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
⊢ (matroid R A).cRank = trdeg R A

Tactic:
(trdeg_eq_iSup_cardinalMk_isTranscendenceBasis _).symm

Premises used: IsTranscendenceBasis, Matroid.cRank, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, Eq.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s : Set A
⊢ (matroid R A).Indep s ↔ AlgebraicIndepOn R _root_.id s

Tactic:
Iff.rfl

Premises used: AlgebraicIndependent, Iff.rfl, Function.Injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s : Set A
⊢ (matroid R A).IsBase s ↔
    IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsTranscendenceBasis
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s t : Set A
rw :
  (((matroid R A).Indep s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬((matroid R A).Indep (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
⊢ (matroid R A).IsBasis s t ↔ AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a

Tactic:
rw [Matroid.IsBasis, maximal_iff_forall_insert fun s t h hst ↦ ⟨h.1.subset hst, hst.trans h.2⟩]

Premises used: Set.maximal_iff_forall_insert, Matroid.IsBasis