-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem affineIndependent_iff_finrank_vectorSpan_eq [Fintype ι] (p : ι → P) {n : ℕ}
    (hc : Fintype.card ι = n + 1) :
    AffineIndependent k p ↔ finrank k (vectorSpan k (Set.range p)) = n

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = #(Finset.filter (fun x => x ≠ i₁) Finset.univ) ↔
    finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = n

Tactic:
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]

Result:
no goals

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = n

Tactic:
rw [Fintype.subtype_card]

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = #(Finset.filter (fun x => x ≠ i₁) Finset.univ) ↔
    finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(vectorSpan k (Set.range p)) = n

Tactic:
classical
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
obtain ⟨i₁⟩ := hn
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]
rw [← Finset.card_univ] at hc
rw [Fintype.subtype_card]
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(vectorSpan k (Set.range p)) = n

Tactic:
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(vectorSpan k (Set.range p)) = n

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(vectorSpan k (Set.range p)) = n

Tactic:
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]

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(vectorSpan k (Set.range p)) = n

Tactic:
obtain ⟨i₁⟩ := hn

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(vectorSpan k (Set.range p)) = n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ι

Tactic:
simp [← Fintype.card_pos_iff, hc]

Result:
no goals

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
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 ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = n

Tactic:
rw [← Finset.card_univ] at hc

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₁)) = n