ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ Cardinal.mk ↑s ≤ ↑n
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
intro s li
case H
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), Finset.card s_1 ≤ n
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ Cardinal.mk ↑s ≤ ↑n
apply Cardinal.card_le_of
case H
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card t ≤ n
case H
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), Finset.card s_1 ≤ n
intro t
case H
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card (Finset.map (Embedding.subtype s) t) ≤ n
case H
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card t ≤ n
rw [← Finset.card_map (Embedding.subtype s)]
case H.a
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R fun i => ↑i
case H
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card (Finset.map (Embedding.subtype s) t) ≤ n
apply H
no goals
case H.a
ι : Type ?u.505754
ι' : Type ?u.505757
R : Type u_2
K : Type ?u.505763
A : Type u_1
A' : Type ?u.505769
A'' : Type ?u.505772
V : Type u
V' : Type ?u.505777
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R fun i => ↑i
apply algebraicIndependent_finset_map_embedding_subtype _ li