case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
⊢ IsTranscendenceBasis R x →
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j

case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
⊢ (∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
⊢ IsTranscendenceBasis R x ↔
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
fconstructor
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
⊢ IsTranscendenceBasis R x →
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
rintro p κ w i' j rfl
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
have p := p.2 (range w) i'.coe_range (range_comp_subset_range _ _)
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
rw [range_comp, ← @image_univ _ _ w] at p
no goals
case mp
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
exact range_iff_surjective.mp (image_injective.mpr i'.injective p)
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
⊢ (∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x
intro p
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
use i
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
intro w i' h
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
⊢ range x = w
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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
specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
q :
  (fun s => Subtype.val '' s) (range fun i => { val := x i, property := (_ : x i ∈ w) }) =
    (fun s => Subtype.val '' s) univ
⊢ range x = w
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
⊢ range x = w
have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
q : (Subtype.val '' range fun i => { val := x i, property := (_ : x i ∈ w) }) = Subtype.val '' univ
⊢ range x = w
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
q :
  (fun s => Subtype.val '' s) (range fun i => { val := x i, property := (_ : x i ∈ w) }) =
    (fun s => Subtype.val '' s) univ
⊢ range x = w
dsimp at q
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
q : (fun x_1 => ↑{ val := x x_1, property := (_ : x x_1 ∈ w) }) '' univ = Subtype.val '' univ
⊢ range x = w
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
q : (Subtype.val '' range fun i => { val := x i, property := (_ : x i ∈ w) }) = Subtype.val '' univ
⊢ range x = w
rw [← image_univ, image_image] at q
no goals
case mpr
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }
q : (fun x_1 => ↑{ val := x x_1, property := (_ : x x_1 ∈ w) }) '' univ = Subtype.val '' univ
⊢ range x = w
simpa using q
case h
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }) x✝ = x x✝
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }) = x
ext
no goals
case h
ι✝ : Type ?u.1377649
ι' : Type ?u.1377652
R✝ : Type ?u.1377655
K : Type ?u.1377658
A✝ : Type ?u.1377661
A' : Type ?u.1377664
A'' : Type ?u.1377667
V : Type u
V' : Type ?u.1377672
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✝
ι : 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 => { val := x i, property := (_ : x i ∈ w) }) x✝ = x x✝
simp