ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ _root_.IsAlgebraic { x_1 // x_1 ∈ adjoin R (range x) } a
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ Algebra.IsAlgebraic { x_1 // x_1 ∈ adjoin R (range x) } A
intro a
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o => Option.elim o a x
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ _root_.IsAlgebraic { x_1 // x_1 ∈ adjoin R (range x) } a
rw [← not_iff_comm.1 (hx.1.option_iff _).symm]
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
⊢ False
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o => Option.elim o a x
intro ai
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
⊢ False
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
⊢ False
have h₁ : range x ⊆ range fun o : Option ι => o.elim a x := by
  rintro x ⟨y, rfl⟩
  exact ⟨some y, rfl⟩
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h₂ : range x ≠ range fun o => Option.elim o a x
⊢ False
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
⊢ False
have h₂ : range x ≠ range fun o : Option ι => o.elim a x := by
  intro h
  have : a ∈ range x := by
    rw [h]
    exact ⟨none, rfl⟩
  rcases this with ⟨b, rfl⟩
  have : some b = none := ai.injective rfl
  simpa
no goals
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h₂ : range x ≠ range fun o => Option.elim o a x
⊢ False
exact h₂ (hx.2 (Set.range fun o : Option ι => o.elim a x)
  ((algebraicIndependent_subtype_range ai.injective).2 ai) h₁)
case intro
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
y : ι
⊢ x y ∈ range fun o => Option.elim o a x
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
⊢ range x ⊆ range fun o => Option.elim o a x
rintro x ⟨y, rfl⟩
no goals
case intro
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
y : ι
⊢ x y ∈ range fun o => Option.elim o a x
exact ⟨some y, rfl⟩
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ False
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
⊢ range x ≠ range fun o => Option.elim o a x
intro h
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
this : a ∈ range x
⊢ False
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ False
have : a ∈ range x := by
  rw [h]
  exact ⟨none, rfl⟩
case intro
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a b✝ : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => Option.elim o (x b) x
h₁ : range x ⊆ range fun o => Option.elim o (x b) x
h : range x = range fun o => Option.elim o (x b) x
⊢ False
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
this : a ∈ range x
⊢ False
rcases this with ⟨b, rfl⟩
case intro
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a b✝ : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => Option.elim o (x b) x
h₁ : range x ⊆ range fun o => Option.elim o (x b) x
h : range x = range fun o => Option.elim o (x b) x
this : some b = none
⊢ False
case intro
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a b✝ : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => Option.elim o (x b) x
h₁ : range x ⊆ range fun o => Option.elim o (x b) x
h : range x = range fun o => Option.elim o (x b) x
⊢ False
have : some b = none := ai.injective rfl
no goals
case intro
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a b✝ : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => Option.elim o (x b) x
h₁ : range x ⊆ range fun o => Option.elim o (x b) x
h : range x = range fun o => Option.elim o (x b) x
this : some b = none
⊢ False
simpa
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ a ∈ range fun o => Option.elim o a x
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ a ∈ range x
rw [h]
no goals
ι : Type u_2
ι' : Type ?u.1381427
R : Type u_1
K : Type ?u.1381433
A : Type u_3
A' : Type ?u.1381439
A'' : Type ?u.1381442
V : Type u
V' : Type ?u.1381447
x : ι → A
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing A'
inst✝⁴ : CommRing A''
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : Algebra R A''
a✝ b : R
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => Option.elim o a x
h₁ : range x ⊆ range fun o => Option.elim o a x
h : range x = range fun o => Option.elim o a x
⊢ a ∈ range fun o => Option.elim o a x
exact ⟨none, rfl⟩