-- Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
theorem linearIndependent_of_top_le_span_of_card_eq_finrank {ι : Type*} [Fintype ι] {b : ι → V}
    (spans : ⊤ ≤ span K (Set.range b)) (card_eq : Fintype.card ι = finrank K V) :
    LinearIndependent K b :=
  linearIndependent_iff'.mpr fun s g dependent i i_mem_s => by
    classical
    by_contra gx_ne_zero
    -- We'll derive a contradiction by showing `b '' (univ \ {i})` of cardinality `n - 1`
    -- spans a vector space of dimension `n`.
    refine not_le_of_gt (span_lt_top_of_card_lt_finrank
      (show (b '' (Set.univ \ {i})).toFinset.card < finrank K V from ?_)) ?_
    · calc
        (b '' (Set.univ \ {i})).toFinset.card = ((Set.univ \ {i}).toFinset.image b).card

Proof state:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ s.erase i
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))

Tactic:
obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk

Result:
case pos.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ s.erase i
k_ne_i : k ≠ i
right✝ : k ∈ s
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))

Proof state:
case refine_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ⊤ ≤ span K (b '' (Set.univ \ {i}))

Tactic:
refine spans.trans (span_le.mpr ?_)

Result:
case refine_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ range b ⊆ ↑(span K (b '' (Set.univ \ {i})))

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b i = -((g i)⁻¹ • ∑ j ∈ s.erase i, g j • b j)

Tactic:
apply eq_neg_of_add_eq_zero_left

Result:
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b i + (g i)⁻¹ • ∑ j ∈ s.erase i, g j • b j = 0

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ False

Tactic:
refine not_le_of_gt (span_lt_top_of_card_lt_finrank
  (show (b '' (Set.univ \ {i})).toFinset.card < finrank K V from ?_)) ?_

Result:
case refine_1
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ (b '' (Set.univ \ {i})).toFinset.card < finrank K V

case refine_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ⊤ ≤ span K (b '' (Set.univ \ {i}))

Proof state:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))

case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))

Tactic:
swap

Result:
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))

case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ∀ (a : ι), a ∈ (Set.univ \ {i}).toFinset ↔ a ∈ Finset.univ.erase i

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ -((g i)⁻¹ • ∑ j ∈ s.erase i, g j • b j) ∈ span K (b '' (Set.univ \ {i}))

Tactic:
refine neg_mem (smul_mem _ _ (sum_mem fun k hk => ?_))

Result:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : ∑ i ∈ s, g i • b i = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ s.erase i
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))