-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
/-- Indexed version of `exists_linearIndependent`. -/
lemma exists_linearIndependent' (v : ι → V) :
    ∃ (κ : Type u') (a : κ → ι), Injective a ∧
      Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧
      LinearIndependent K (v ∘ a)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
i : ι
hi : i ∈ s
⊢ v i ∈ t

Tactic:
obtain ⟨a, rfl⟩ := hi

Result:
case intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
a : ↑t
⊢ v ((fun a => f ⋯) a) ∈ t

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ ∃ κ a, Injective a ∧ span K (range (v ∘ a)) = span K (range v) ∧ LinearIndependent K (v ∘ a)

Tactic:
obtain ⟨t, ht, hsp, hli⟩ := exists_linearIndependent K (Set.range v)

Result:
case intro.intro.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
ht : t ⊆ range v
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
⊢ ∃ κ a, Injective a ∧ span K (range (v ∘ a)) = span K (range v) ∧ LinearIndependent K (v ∘ a)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
⊢ span K (range (v ∘ Subtype.val)) = span K t

Tactic:
congr

Result:
case e_s
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
⊢ range (v ∘ Subtype.val) = t

Proof state:
case intro.intro.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
⊢ ∃ κ a, Injective a ∧ span K (range (v ∘ a)) = span K (range v) ∧ LinearIndependent K (v ∘ a)

Tactic:
let f' (a : s) : t := ⟨v a.val, hs a.property⟩

Result:
case intro.intro.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
⊢ ∃ κ a, Injective a ∧ span K (range (v ∘ a)) = span K (range v) ∧ LinearIndependent K (v ∘ a)

Proof state:
case intro.intro.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
⊢ LinearIndependent (ι := ↑s) K (Subtype.val ∘ f')

Tactic:
apply hli.comp

Result:
case intro.intro.intro.hf
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
⊢ Injective f'

Proof state:
case intro.intro.intro.hf
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
⊢ Injective f'

Tactic:
rintro ⟨i, x, rfl⟩ ⟨j, y, rfl⟩ hij

Result:
case intro.intro.intro.hf.mk.intro.mk.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
x y : ↑t
hij : f' ⟨(fun a => f ⋯) x, ⋯⟩ = f' ⟨(fun a => f ⋯) y, ⋯⟩
⊢ ⟨(fun a => f ⋯) x, ⋯⟩ = ⟨(fun a => f ⋯) y, ⋯⟩

Proof state:
case intro.intro.intro.hf.mk.intro.mk.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
x y : ↑t
hij : f' ⟨(fun a => f ⋯) x, ⋯⟩ = f' ⟨(fun a => f ⋯) y, ⋯⟩
⊢ ⟨(fun a => f ⋯) x, ⋯⟩ = ⟨(fun a => f ⋯) y, ⋯⟩

Tactic:
simp only [Subtype.ext_iff, hf, f'] at hij

Result:
case intro.intro.intro.hf.mk.intro.mk.intro
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a => f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a => ⟨v ↑a, ⋯⟩
x y : ↑t
hij : ↑x = ↑y
⊢ ⟨(fun a => f ⋯) x, ⋯⟩ = ⟨(fun a => f ⋯) y, ⋯⟩