-- 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 (⇑f '' range b') = Submodule.map f (span K (range b'))
⊢ x ∈ ⊤ → x ∈ span K (range b')

Tactic:
have hf : f '' Set.range b' = Set.range b := by
  ext x
  simp [f, b', Set.mem_image, Set.mem_range]

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'))
hf : ⇑f '' range b' = 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))
h : span K (⇑f '' range b') = Submodule.map f (span K (range b'))
hf : ⇑f '' range b' = range b
⊢ x ∈ ⊤ → x ∈ span K (range b')

Tactic:
rw [hf] at h

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
⊢ 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))
h : span K (range b) = Submodule.map f (span K (range b'))
hf : ⇑f '' range b' = range b
⊢ x ∈ ⊤ → x ∈ span K (range b')

Tactic:
have hx : (x : V) ∈ span K (Set.range b) := x.property

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 ∈ 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
hc : Fintype.card ι = Set.finrank K (range b)
f : ↥(span K (range b)) →ₗ[K] V := (span K (range b)).subtype
⊢ LinearIndependent K b

Tactic:
let b' : ι → span K (Set.range b) := fun i =>
  ⟨b i, mem_span.2 fun p hp => hp (Set.mem_range_self _)⟩

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, ⋯⟩
⊢ LinearIndependent K b

Proof state:
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)

Tactic:
intro h

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
h : LinearIndependent K b
⊢ Fintype.card ι = Set.finrank 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))
h : span K (⇑f '' range b') = Submodule.map f (span K (range b'))
⊢ ⇑f '' range b' = range b

Tactic:
ext x

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
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

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

Tactic:
exact (finrank_span_eq_card h).symm

Result:
no goals