awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
refine_1 :
  ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
    (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ⋃₀ c ⊆ t
refine_2 :
  ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
    (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), LinearIndepOn K v (⋃₀ c)
refine_3 :
  ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
    (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ∀ x ∈ c, x ⊆ ⋃₀ c
⊢ ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub

Tactic:
refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
sUnion_subset fun x xc => (hc xc).1

Premises used: Set.sUnion_subset, And.left
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
exact sUnion_subset fun x xc => (hc xc).1

Premises used: Set.sUnion_subset, And.left
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K v (⋃₀ c)

Tactic:
linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2

Premises used: IsChain.directedOn, And.right, linearIndepOn_sUnion_of_directed
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K v (⋃₀ c)

Tactic:
exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2

Premises used: IsChain.directedOn, And.right, linearIndepOn_sUnion_of_directed
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c

Tactic:
subset_sUnion_of_mem

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c

Tactic:
exact subset_sUnion_of_mem

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
obtain :
  ∀ (b : Set ι) (sb : s ⊆ b)
    (h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b),
    ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b

Tactic:
obtain ⟨b, sb, h⟩ := by
    refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩
    · refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
      · exact sUnion_subset fun x xc => (hc xc).1
      · exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
      · exact subset_sUnion_of_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b

Tactic:
⟨b, h.prop.1, sb, fun _ ⟨x, hx, hvx⟩ => by_contra fun hn ↦ hn ?_, h.prop.2⟩

Premises used: Maximal.prop, Membership.mem, SetLike.coe, And.right, And.left, And.intro, Exists.intro, Submodule.span, _private.0.exists_linearIndepOn_extension.match_1, by_contra, Set.image
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
refine :
  ∀ x ∈ v '' t,
    ∀ (x_2 : ι) (hx : x_2 ∈ t) (hvx : v x_2 = x) (hn : x ∉ (↑(span K (v '' b)) : Set V)),
      x ∈ (↑(span K (v '' b)) : Set V)
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b

Tactic:
refine ⟨b, h.prop.1, sb, fun _ ⟨x, hx, hvx⟩ => by_contra fun hn ↦ hn ?_, h.prop.2⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
x_1 : V
h_1 : x_1 ∈ v '' t
x : ι
hx : x ∈ t
hvx : v x = x_1
hn : x_1 ∉ (↑(span K (v '' b)) : Set V)
subst : v x ∈ v '' t → ∀ (hn : v x ∉ (↑(span K (v '' b)) : Set V)), v x ∈ (↑(span K (v '' b)) : Set V)
⊢ x_1 ∈ (↑(span K (v '' b)) : Set V)

Tactic:
subst hvx
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
x : ι
hx : x ∈ t
h_1 : v x ∈ v '' t
hn : v x ∉ (↑(span K (v '' b)) : Set V)
⊢ v x ∈ (↑(span K (v '' b)) : Set V)

Tactic:
subset_span <| mem_image_of_mem v <| h.mem_of_prop_insert
    ⟨insert_subset hx h.prop.1, h.prop.2.insert hn⟩

Premises used: LinearIndepOn.insert, Maximal.prop, Maximal.mem_of_prop_insert, And.right, And.left, Set.mem_image_of_mem, And.intro, Submodule.subset_span, Set.insert_subset
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
x : ι
hx : x ∈ t
h_1 : v x ∈ v '' t
hn : v x ∉ (↑(span K (v '' b)) : Set V)
⊢ v x ∈ (↑(span K (v '' b)) : Set V)

Tactic:
exact subset_span <| mem_image_of_mem v <| h.mem_of_prop_insert
    ⟨insert_subset hx h.prop.1, h.prop.2.insert hn⟩

Premises used: LinearIndepOn.insert, Maximal.prop, Maximal.mem_of_prop_insert, And.right, And.left, Set.mem_image_of_mem, And.intro, Submodule.subset_span, Set.insert_subset
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ ∃ b ⊆ t, s ⊆ b ∧ id '' t ⊆ (↑(span K (id '' b)) : Set V) ∧ LinearIndepOn K id b

Tactic:
exists_linearIndepOn_extension hs hst

Premises used: exists_linearIndepOn_extension
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
h : ∀ (x : Set V), t = id '' t
h₁ : ∀ (x : Set V), x = id '' x
⊢ ∃ b ⊆ t, s ⊆ b ∧ t ⊆ (↑(span K b) : Set V) ∧ LinearIndepOn K id b

Tactic:
convert! exists_linearIndepOn_extension hs hst

Premises used: exists_linearIndepOn_extension
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x : Set V
⊢ t = id '' t

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x : Set V
⊢ x = id '' x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
t : Set V
obtain :
  ∀ (b : Set V) (hb₁ : b ⊆ t) (hb₂ : t ⊆ (↑(span K b) : Set V)) (hb₃ : LinearIndepOn K id b),
    ∃ b ⊆ t,
      Eq (α := Submodule K V) (span K b) (span K t) ∧
        LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ b }) K (Subtype.val (p := fun (x : V) ↦ x ∈ b))
⊢ ∃ b ⊆ t,
    Eq (α := Submodule K V) (span K b) (span K t) ∧
      LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ b }) K (Subtype.val (p := fun (x : V) ↦ x ∈ b))

Tactic:
obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
    exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)

Premises used: Set.empty_subset, linearIndependent_empty, exists_linearIndepOn_id_extension
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
t b : Set V
hb₁ : b ⊆ t
hb₂ : t ⊆ (↑(span K b) : Set V)
hb₃ : LinearIndepOn K id b
⊢ ∃ b ⊆ t,
    Eq (α := Submodule K V) (span K b) (span K t) ∧
      LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ b }) K (Subtype.val (p := fun (x : V) ↦ x ∈ b))

Tactic:
⟨b, hb₁, (span_eq_of_le _ hb₂ (Submodule.span_mono hb₁)).symm, hb₃⟩

Premises used: Submodule.span_eq_of_le, And.intro, Submodule.span_mono, Exists.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
t b : Set V
hb₁ : b ⊆ t
hb₂ : t ⊆ (↑(span K b) : Set V)
hb₃ : LinearIndepOn K id b
⊢ ∃ b ⊆ t,
    Eq (α := Submodule K V) (span K b) (span K t) ∧
      LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ b }) K (Subtype.val (p := fun (x : V) ↦ x ∈ b))

Tactic:
exact ⟨b, hb₁, (span_eq_of_le _ hb₂ (Submodule.span_mono hb₁)).symm, hb₃⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
obtain :
  ∀ (t : Set V) (ht : t ⊆ range v) (hsp : Eq (α := Submodule K V) (span K t) (span K (range v)))
    (hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))),
    ∃ (κ : Type u') (a : κ → ι),
      Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (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)

Premises used: exists_linearIndependent, Set.range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
ht : t ⊆ range v
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
choose :
  ∀ (f : ⦃a : V⦄ → a ∈ t → ι) (hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a),
    ∃ (κ : Type u') (a : κ → ι),
      Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)

Tactic:
choose f hf using ht
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
i : ι
hi : i ∈ s
obtain : ∀ (a : (↑t : Type u)), v ((fun (a : (↑t : Type u)) ↦ f ⋯) a) ∈ t
⊢ v i ∈ t

Tactic:
obtain ⟨a, rfl⟩ := hi

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
a : (↑t : Type u)
⊢ v ((fun (a : (↑t : Type u)) ↦ f ⋯) a) ∈ t

Tactic:
simp [hf]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
⊢ ∀ {i : ι} (hi : i ∈ s), v i ∈ t

Tactic:
have hs {i : ι} (hi : i ∈ s) : v i ∈ t := by obtain ⟨a, rfl⟩ := hi; simp [hf]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
e_s : range (ι := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) = t
⊢ Eq (α := Submodule K V) (span K (range (ι := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))) (span K t)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
⊢ range (ι := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) = t

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
refine : LinearIndependent (ι := (↑s : Type u')) K (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)

Tactic:
refine ⟨s, Subtype.val, Subtype.val_injective, hsp.symm ▸ by congr; aesop, ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
h :
  ∀ (x : (↑s : Type u')),
    (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f') x = (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) x
⊢ Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f' = v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
x : (↑s : Type u')
⊢ (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f') x = (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) x

Tactic:
simp [f']
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
rw : LinearIndependent K (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f')
⊢ LinearIndependent (ι := (↑s : Type u')) K (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))

Tactic:
rw [← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
hf₁ : Injective f'
⊢ LinearIndependent K (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f')

Tactic:
apply hli.comp

Premises used: LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
x y : (↑t : Type u)
hij :
  f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) x) ⋯) =
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) y) ⋯)
⊢ (↑x : V) = (↑y : V)

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

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
x y : (↑t : Type u)
hij : (↑x : V) = (↑y : V)
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) x) ⋯ =
    Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) y) ⋯

Tactic:
simp [hij]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ hs.extend (s := s) (t := t) hst ⊆ t

Tactic:
let ⟨hbt, _hsb, _htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  hbt

Premises used: LinearIndepOn.extend, exists_linearIndepOn_extension, HasSubset.Subset, Classical.choose_spec, _private.0.LinearIndepOn.extend_subset.match_1
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ s ⊆ hs.extend (s := s) (t := t) hst

Tactic:
let ⟨_hbt, hsb, _htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  hsb

Premises used: LinearIndepOn.extend, exists_linearIndepOn_extension, HasSubset.Subset, Classical.choose_spec, _private.0.LinearIndepOn.extend_subset.match_1
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ v '' t ⊆ (↑(span K (v '' hs.extend (s := s) (t := t) hst)) : Set V)

Tactic:
let ⟨_hbt, _hsb, htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  htb

Premises used: LinearIndepOn.extend, exists_linearIndepOn_extension, HasSubset.Subset, Classical.choose_spec, SetLike.coe, Submodule.span, Set.image, _private.0.LinearIndepOn.extend_subset.match_1