k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.343704
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Coplanar k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 2
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.343704
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
have h : Coplanar k s ↔ Module.rank k (vectorSpan k s) ≤ 2 := Iff.rfl
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.343704
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Coplanar k s ↔ ↑(finrank k { x // x ∈ vectorSpan k s }) ≤ 2
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.343704
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Coplanar k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 2
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
rw [← finrank_eq_rank] at h
no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.343704
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Coplanar k s ↔ ↑(finrank k { x // x ∈ vectorSpan k s }) ≤ 2
⊢ Coplanar k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 2
exact_mod_cast h