ι : Type ?u.873393
ι' : Type ?u.873396
R : Type u_2
K : Type ?u.873402
A : Type u_1
A' : Type ?u.873408
A'' : Type ?u.873411
V : Type u
V' : Type ?u.873416
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
s : Set (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
ι : Type ?u.873393
ι' : Type ?u.873396
R : Type u_2
K : Type ?u.873402
A : Type u_1
A' : Type ?u.873408
A'' : Type ?u.873411
V : Type u
V' : Type ?u.873416
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
s : Set (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val
letI : Nonempty s := Nonempty.to_subtype hsn
ι : Type ?u.873393
ι' : Type ?u.873396
R : Type u_2
K : Type ?u.873402
A : Type u_1
A' : Type ?u.873408
A'' : Type ?u.873411
V : Type u
V' : Type ?u.873416
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
s : Set (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
ι : Type ?u.873393
ι' : Type ?u.873396
R : Type u_2
K : Type ?u.873402
A : Type u_1
A' : Type ?u.873408
A'' : Type ?u.873411
V : Type u
V' : Type ?u.873416
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
s : Set (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
rw [sUnion_eq_iUnion]
no goals
ι : Type ?u.873393
ι' : Type ?u.873396
R : Type u_2
K : Type ?u.873402
A : Type u_1
A' : Type ?u.873408
A'' : Type ?u.873411
V : Type u
V' : Type ?u.873416
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
s : Set (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ AlgebraicIndependent R Subtype.val
exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)
no goals
ι : Type ?u.873393
ι' : Type ?u.873396
R : Type u_2
K : Type ?u.873402
A : Type u_1
A' : Type ?u.873408
A'' : Type ?u.873411
V : Type u
V' : Type ?u.873416
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
s : Set (Set A)
hsn : Set.Nonempty s
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set A), a ∈ s → AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ ∀ (i : ↑s), AlgebraicIndependent R Subtype.val
simpa using h