case h.e'_1.h.e'_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ ↑(Set.Finite.toFinset hs) = s
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ Basis (↑↑(Set.Finite.toFinset hs)) K V
convert b
no goals
case h.e'_1.h.e'_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ ↑(Set.Finite.toFinset hs) = s
simp