-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem AlgebraicIndependent.isTranscendenceBasis_iff {ι : Type w} {R : Type u} [CommRing R]
    [Nontrivial R] {A : Type v} [CommRing A] [Algebra R A] {x : ι → A}
    (i : AlgebraicIndependent R x) :
    IsTranscendenceBasis R x ↔
      ∀ (κ : Type v) (w : κ → A) (_ : AlgebraicIndependent R w) (j : ι → κ) (_ : w ∘ j = x),
        Surjective j

Proof state:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
q : (fun s => Subtype.val '' s) (range fun i => ⟨x i, ⋯⟩) = (fun s => Subtype.val '' s) univ
⊢ range x = w

Tactic:
dsimp at q

Result:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
q : (Subtype.val '' range fun i => ⟨x i, ⋯⟩) = Subtype.val '' univ
⊢ range x = w

Proof state:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
q : (fun x_1 => ↑⟨x x_1, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range x = w

Tactic:
simpa using q

Result:
no goals

Proof state:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Tactic:
exact range_eq_univ.mp (image_injective.mpr i'.injective p)

Result:
no goals

Proof state:
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
⊢ (Subtype.val ∘ fun i => ⟨x i, ⋯⟩) = x

Tactic:
ext

Result:
case h
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
x✝ : ι
⊢ (Subtype.val ∘ fun i => ⟨x i, ⋯⟩) x✝ = x x✝

Proof state:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
⊢ range x = w

Tactic:
specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)

Result:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
⊢ range x = w

Proof state:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
q : (Subtype.val '' range fun i => ⟨x i, ⋯⟩) = Subtype.val '' univ
⊢ range x = w

Tactic:
rw [← image_univ, image_image] at q

Result:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
q : (fun x_1 => ↑⟨x x_1, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range x = w

Proof state:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
⊢ range x = w

Tactic:
have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq

Result:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
p : Surjective fun i => ⟨x i, ⋯⟩
q : (fun s => Subtype.val '' s) (range fun i => ⟨x i, ⋯⟩) = (fun s => Subtype.val '' s) univ
⊢ range x = w

Proof state:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j

Tactic:
rw [range_comp, ← @image_univ _ _ w] at p

Result:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Proof state:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → range x ≤ s → range x = s

Tactic:
intro w i' h

Result:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
⊢ range x = w

Proof state:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p : IsTranscendenceBasis R (w ∘ j)
⊢ Surjective j

Tactic:
have p := p.2 (range w) i'.coe_range (range_comp_subset_range _ _)

Result:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j

Proof state:
case mpr
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ IsTranscendenceBasis R x

Tactic:
use i

Result:
case right
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → range x ≤ s → range x = s