Theorem: finrank_span_set_eq_card' (FltRegular/NumberTheory/SystemOfUnits.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : NumberField K
inst✝¹⁰ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
r : ℕ
inst✝⁶ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁵ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card
Tactic:
have : Module.rank R (span R s) = #s := rank_span_set hs
State after:
p : ℕ+
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : NumberField K
inst✝¹⁰ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
r : ℕ
inst✝⁶ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁵ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
this : Module.rank R ↥(span R s) = #↑s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card

State before:
p : ℕ+
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : NumberField K
inst✝¹⁰ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
r : ℕ
inst✝⁶ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁵ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
this : Module.rank R ↥(span R s) = #↑s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card
Tactic:
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this
State after:
no goals