ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
⊢ AlgebraicIndependent R Subtype.val
ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val
refine' algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => _
case intro.intro
ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
I : Set η
fi : Set.Finite I
hI : t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
⊢ AlgebraicIndependent R Subtype.val
ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
⊢ AlgebraicIndependent R Subtype.val
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
case intro.intro.intro
ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
I : Set η
fi : Set.Finite I
hI : t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
i : η
hi : ∀ (i_1 : η), i_1 ∈ Finite.toFinset fi → s i_1 ⊆ s i
⊢ AlgebraicIndependent R Subtype.val
case intro.intro
ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
I : Set η
fi : Set.Finite I
hI : t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
⊢ AlgebraicIndependent R Subtype.val
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
no goals
case intro.intro.intro
ι : Type ?u.871631
ι' : Type ?u.871634
R : Type u_3
K : Type ?u.871640
A : Type u_2
A' : Type ?u.871646
A'' : Type ?u.871649
V : Type u
V' : Type ?u.871654
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 u_1
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : Set.Finite t
I : Set η
fi : Set.Finite I
hI : t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
i : η
hi : ∀ (i_1 : η), i_1 ∈ Finite.toFinset fi → s i_1 ⊆ s i
⊢ AlgebraicIndependent R Subtype.val
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))