awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ 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 ((⇑(algebraMap S A) : (a : S) → A) '' range 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]
-- 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)
⊢ Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))))) A
have inr : Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) 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]]
-- 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)
⊢ Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) A
have inr : Algebra.IsAlgebraic (↥Rxy) A
Tactic: change Algebra.IsAlgebraic Rxy A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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)
⊢ Algebra.IsAlgebraic (↥Rxy) A
have this : Nontrivial S
Tactic: have := hx.1.algebraMap_injective.nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ Algebra.IsAlgebraic (↥Rxy) A
have this₁ : Nontrivial A
Tactic: have := hy.1.algebraMap_injective.nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 (↥Rxy) A
have this₁ : Algebra.IsAlgebraic (↥(adjoin S (range y))) A
Tactic: have := hy.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)
this_1 : Nontrivial S
this_2 : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
⊢ Algebra ↥Rxy ↥Sy
have refine : range y ⊆ (↑(Subalgebra.restrictScalars (↥Rx) Sy) : Set A)
Tactic: refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 ⋯))
⊢ Algebra.IsAlgebraic (↥Rxy) A
have this₁ : IsScalarTower (↥Rxy) (↥Sy) A
Tactic: have : IsScalarTower Rxy Sy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ Algebra.IsAlgebraic (↥Rxy) A
have this₁ : IsScalarTower.{v, w, w} ↥Rx ↥Rxy ↥Sy
Tactic: have : IsScalarTower Rx Rxy Sy := .of_algebraMap_eq fun ⟨a, _⟩ ↦ Subtype.ext rfl
-- 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)
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
have 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 sorry)
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
-- 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)
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 ⋯)
⊢ Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy
have refine_2 : ∀ (x : ↥Sy) (a : A) (ha : a ∈ Sy) (x : S),
  Injective.{v + 1, w + 1} (α := ↥Rx) (β := ↥Rxy) (⇑(algebraMap ↥Rx ↥Rxy) : (a : ↥Rx) → ↥Rxy)
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
-- 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)
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)
⊢ Algebra.IsAlgebraic.{w, w} ↥Rxy ↥Sy
have 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) sorry : ↥Sy)
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 (↥Rxy) A
have this₁ : 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)
-- 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
hx : IsTranscendenceBasis R x
⊢ IsEmpty ι ↔ Algebra.IsAlgebraic R A
have refine : IsEmpty ι → Algebra.IsAlgebraic R A
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ hx.1.isEmpty_of_isAlgebraic⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 R A
have this : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
Tactic: have := hx.isAlgebraic
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 R A
have this₁ : Algebra.IsAlgebraic (↥⊥) A
Tactic: rw [Set.range_eq_empty x, adjoin_empty] at this
Cleared hypotheses: this
-- 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
hx : IsTranscendenceBasis R x
⊢ Nonempty ι ↔ Algebra.Transcendental R A
have rw : ¬IsEmpty ι ↔ Algebra.Transcendental R A
Tactic: rw [← not_isEmpty_iff, Algebra.transcendental_iff_not_isAlgebraic, hx.isEmpty_iff_isAlgebraic]
-- 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
hx : IsTranscendenceBasis R x
rw : ¬IsEmpty ι ↔ Algebra.Transcendental R A
⊢ Nonempty ι ↔ Algebra.Transcendental R A
have rw₁ : ¬IsEmpty ι ↔ ¬Algebra.IsAlgebraic R A
Tactic: rw [← not_isEmpty_iff, Algebra.transcendental_iff_not_isAlgebraic, hx.isEmpty_iff_isAlgebraic]
-- 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
hx : IsTranscendenceBasis R x
rw : ¬IsEmpty ι ↔ Algebra.Transcendental R A
rw₁ : ¬IsEmpty ι ↔ ¬Algebra.IsAlgebraic R A
⊢ Nonempty ι ↔ Algebra.Transcendental R A
have rw₂ : ¬Algebra.IsAlgebraic R A ↔ ¬Algebra.IsAlgebraic R A
Tactic: rw [← not_isEmpty_iff, Algebra.transcendental_iff_not_isAlgebraic, hx.isEmpty_iff_isAlgebraic]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 (↥(IntermediateField.adjoin F (range x))) E
have this : Algebra.IsAlgebraic (↥(adjoin F (range x))) E
Tactic: haveI := hx.isAlgebraic
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E
have set : let S := range x;
∀ (this : Algebra.IsAlgebraic (↥(adjoin F S)) E), Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E
Tactic: set S := range x
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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 ⋯))
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E
have this₁ : 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)
-- 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
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
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)
have contrapose! : ∀ (h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)), Maximal (AlgebraicIndepOn R _root_.id) I
Tactic: contrapose! h
Cleared hypotheses: 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
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)
⊢ Maximal (AlgebraicIndepOn R _root_.id) I
have 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))
Tactic: rw [← isTranscendenceBasis_iff_maximal] at B_base ⊢
Cleared hypotheses: B_base, 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
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)
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
have inl : Subsingleton R → IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
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
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))
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
have inr : Nontrivial R → IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
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
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
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
have 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 }
Tactic: rw [isTranscendenceBasis_iff_of_subsingleton] at B_base ⊢
Cleared hypotheses: B_base, h, h_1
-- 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
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
⊢ Nonempty.{w + 1} { x : A // x ∈ I }
have inl : ∀ (this : ¬Nonempty.{w + 1} { x : A // x ∈ I }), False
Tactic: by_contra this
-- 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
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 }
⊢ False
have inl : ∀ (b : A) (hb : b ∈ B), False
Tactic: have ⟨b, hb⟩ := B_base
-- 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
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
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ I }) R (Subtype.val (p := fun (x : A) ↦ x ∈ I))
have inr : Algebra.IsAlgebraic (↥(adjoin R (range fun (i : (↑I : Type w)) ↦ _root_.id (↑i : A)))) A
Tactic: apply I_ind.isTranscendenceBasis_iff_isAlgebraic.mpr