-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {n : ℕ}
    (H : ∀ s : Finset A, (AlgebraicIndependent R fun i : s => (i : A)) → s.card ≤ n) :
    ∀ s : Set A, AlgebraicIndependent R ((↑) : s → A) → Cardinal.mk s ≤ n

Proof state:
case H
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), s_1.card ≤ n

Tactic:
intro t

Result:
case H
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n

Proof state:
case H
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n

Tactic:
rw [← Finset.card_map (Embedding.subtype s)]

Result:
case H
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ (Finset.map (Embedding.subtype s) t).card ≤ n

Proof state:
case H
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ (Finset.map (Embedding.subtype s) t).card ≤ n

Tactic:
apply H

Result:
case H.a
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R fun i => ↑i

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ Cardinal.mk ↑s ≤ ↑n

Tactic:
apply Cardinal.card_le_of

Result:
case H
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), s_1.card ≤ n

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

Tactic:
intro s li

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ Cardinal.mk ↑s ≤ ↑n

Proof state:
case H.a
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R fun i => ↑i

Tactic:
apply algebraicIndependent_finset_map_embedding_subtype _ li

Result:
no goals