k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
hn : Nonempty ι
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
hn : Nonempty ι
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
cases' hn with i₁
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ AffineIndependent k p ↔ finrank k { x // x ∈ vectorSpan k (Set.range p) } = n
rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
  linearIndependent_iff_card_eq_finrank_span, eq_comm,
  vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
congr
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
rw [← Finset.card_univ] at hc
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } =
      Finset.card (Finset.filter (fun x => x ≠ i₁) Finset.univ) ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = Fintype.card { x // x ≠ i₁ } ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
rw [Fintype.subtype_card]
no goals
case intro
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Finset.card Finset.univ = n + 1
i₁ : ι
⊢ finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } =
      Finset.card (Finset.filter (fun x => x ≠ i₁) Finset.univ) ↔
    finrank k { x // x ∈ Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁) } = n
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
no goals
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ Nonempty ι
simp [← Fintype.card_pos_iff, hc]