-- Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
theorem linearIndependent_iff_card_eq_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
    LinearIndependent K b ↔ Fintype.card ι = (Set.range b).finrank K

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
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x : ↥(span K (range b))
h : span K (range b) = Submodule.map f (span K (range b'))
hf : ⇑f '' range b' = range b
hx : ↑x ∈ span K (range b)
⊢ x ∈ ⊤ → x ∈ span K (range b')

Tactic:
simp_rw [h] at hx

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x : ↥(span K (range b))
h : span K (range b) = Submodule.map f (span K (range b'))
hf : ⇑f '' range b' = range b
hx : ↑x ∈ Submodule.map f (span K (range b'))
⊢ x ∈ ⊤ → x ∈ span K (range b')

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
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x : ↥(span K (range b))
⊢ x ∈ ⊤ → x ∈ span K (range b')

Tactic:
have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x : ↥(span K (range b))
h : span K (⇑f '' range b') = Submodule.map f (span K (range b'))
⊢ x ∈ ⊤ → x ∈ span K (range b')

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
⊢ Fintype.card ι = Set.finrank K (range b) → LinearIndependent K b

Tactic:
intro hc

Result:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
⊢ LinearIndependent K b

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
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
⊢ ⊤ ≤ span K (range b')

Tactic:
intro x

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x : ↥(span K (range b))
⊢ x ∈ ⊤ → x ∈ span K (range b')

Proof state:
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
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x✝ : ↥(span K (range b))
h : span K (⇑f '' range b') = Submodule.map f (span K (range b'))
x : V
⊢ x ∈ ⇑f '' range b' ↔ x ∈ range b

Tactic:
simp [f, b', Set.mem_image, Set.mem_range]

Result:
no goals

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
⊢ LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (range b)

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b → Fintype.card ι = Set.finrank K (range b)

case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
⊢ Fintype.card ι = Set.finrank K (range b) → LinearIndependent K b

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
hs : ⊤ ≤ span K (range b')
⊢ LinearIndependent K b

Tactic:
have hi : LinearMap.ker f = ⊥ := ker_subtype _

Result:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
hs : ⊤ ≤ span K (range b')
hi : LinearMap.ker f = ⊥
⊢ LinearIndependent K b

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
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
x : ↥(span K (range b))
h : span K (range b) = Submodule.map f (span K (range b'))
hf : ⇑f '' range b' = range b
hx : ↑x ∈ Submodule.map f (span K (range b'))
⊢ x ∈ ⊤ → x ∈ span K (range b')

Tactic:
simpa [f, mem_map] using hx

Result:
no goals

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
⊢ LinearIndependent K b

Tactic:
have hs : ⊤ ≤ span K (Set.range b') := by
  intro x
  have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
  have hf : f '' Set.range b' = Set.range b := by
    ext x
    simp [f, b', Set.mem_image, Set.mem_range]
  rw [hf] at h
  have hx : (x : V) ∈ span K (Set.range b) := x.property
  simp_rw [h] at hx
  simpa [f, mem_map] using hx

Result:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
hs : ⊤ ≤ span K (range b')
⊢ LinearIndependent K b

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
⊢ LinearIndependent K b

Tactic:
let f := Submodule.subtype (span K (Set.range b))

Result:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
⊢ LinearIndependent K b

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
b' : ι → ↥(span K (range b)) := fun i => ⟨b i, ⋯⟩
hs : ⊤ ≤ span K (range b')
hi : LinearMap.ker f = ⊥
⊢ LinearIndependent K b

Tactic:
convert (linearIndependent_of_top_le_span_of_card_eq_finrank hs hc).map' _ hi

Result:
no goals