-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem IsTranscendenceBasis.isAlgebraic [Nontrivial R] (hx : IsTranscendenceBasis R x) :
    Algebra.IsAlgebraic (adjoin R (range x)) A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
⊢ a ∈ range x

Tactic:
rw [h]

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
⊢ a ∈ range fun o => o.elim a x

Proof state:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h₂ : range x ≠ range fun o => o.elim a x
⊢ False

Tactic:
exact h₂ (hx.2 (Set.range fun o : Option ι => o.elim a x)
  ((algebraicIndependent_subtype_range ai.injective).2 ai) h₁)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
constructor

Result:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ ∀ (x_1 : A), _root_.IsAlgebraic (↥(adjoin R (range x))) x_1

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
this : a ∈ range x
⊢ False

Tactic:
rcases this with ⟨b, rfl⟩

Result:
case intro
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => o.elim (x b) x
h₁ : range x ⊆ range fun o => o.elim (x b) x
h : range x = range fun o => o.elim (x b) x
⊢ False

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
⊢ range x ⊆ range fun o => o.elim a x

Tactic:
rintro x ⟨y, rfl⟩

Result:
case intro
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
y : ι
⊢ x y ∈ range fun o => o.elim a x

Proof state:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
⊢ False

Tactic:
have h₁ : range x ⊆ range fun o : Option ι => o.elim a x := by
  rintro x ⟨y, rfl⟩
  exact ⟨some y, rfl⟩

Result:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
⊢ False

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
⊢ range x ≠ range fun o => o.elim a x

Tactic:
intro h

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
⊢ False

Proof state:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
⊢ False

Tactic:
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

Result:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h₂ : range x ≠ range fun o => o.elim a x
⊢ False

Proof state:
case intro
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => o.elim (x b) x
h₁ : range x ⊆ range fun o => o.elim (x b) x
h : range x = range fun o => o.elim (x b) x
⊢ False

Tactic:
have : some b = none := ai.injective rfl

Result:
case intro
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => o.elim (x b) x
h₁ : range x ⊆ range fun o => o.elim (x b) x
h : range x = range fun o => o.elim (x b) x
this : some b = none
⊢ False

Proof state:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o => o.elim a x

Tactic:
intro ai

Result:
case isAlgebraic
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
⊢ False

Proof state:
case intro
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o => o.elim (x b) x
h₁ : range x ⊆ range fun o => o.elim (x b) x
h : range x = range fun o => o.elim (x b) x
this : some b = none
⊢ False

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
⊢ False

Tactic:
have : a ∈ range x := by
  rw [h]
  exact ⟨none, rfl⟩

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o => o.elim a x
h₁ : range x ⊆ range fun o => o.elim a x
h : range x = range fun o => o.elim a x
this : a ∈ range x
⊢ False