awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
i' : ι'
hi' :
  repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯) =
      Finsupp.single i' 1 ∧
    (f : (a : ι') → ι) i' = i
⊢ (f : (a : ι') → ι) i' = i

Tactic:
hi'.2

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
i' : ι'
hi' :
  repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯) =
      Finsupp.single i' 1 ∧
    (f : (a : ι') → ι) i' = i
⊢ (f : (a : ι') → ι) i' = i

Tactic:
exact hi'.2

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
apply :
  (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ⊆
    (↑(span R
          (range (ι := (↑t : Type u_4))
            ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))))) :
      Set M)
⊢ Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))

Tactic:
apply surjective_of_linearIndependent_of_span hs f _

Premises used: surjective_of_linearIndependent_of_span
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ s ⊆ (↑(span R t) : Set M)

Tactic:
hst
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h₁ : (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) = s
h₂ :
  range (ι := (↑t : Type u_4))
      ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))) =
    t
⊢ (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ⊆
    (↑(span R
          (range (ι := (↑t : Type u_4))
            ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))))) :
      Set M)

Tactic:
convert! hst
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ (range fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) = s

Tactic:
simp [f, comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ range (ι := (↑t : Type u_4))
      ((fun (x : (↑s : Type u_4)) ↦ id (↑x : M)) ∘ (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))) =
    t

Tactic:
simp [f, comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
⊢ Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))

Tactic:
have h_surj : Surjective f := by
    apply surjective_of_linearIndependent_of_span hs f _
    convert! hst <;> simp [f, comp_def]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
apply : s ⊆ t
⊢ s = t

Tactic:
apply Subset.antisymm _ h

Premises used: Set.Subset.antisymm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
rcases :
  ∀ (y : (↑t : Type u_4))
    (hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx), x ∈ t
⊢ x ∈ t

Tactic:
rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
y : (↑t : Type u_4)
hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
⊢ (↑y : M) ∈ t

Tactic:
y.mem

Premises used: Subtype.mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
y : (↑t : Type u_4)
hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
h₁ : x = (↑y : M)
⊢ x ∈ t

Tactic:
convert! y.mem

Premises used: Subtype.mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ (↑(span R t) : Set M)
f : (↑t : Type u_4) ↪ (↑s : Type u_4) :=
  { toFun := fun (x : (↑t : Type u_4)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑x : M) ⋯, inj' := ⋯ }
h_surj : Surjective (α := (↑t : Type u_4)) (β := (↑s : Type u_4)) (⇑f : (a : (↑t : Type u_4)) → (↑s : Type u_4))
x : M
hx : x ∈ s
y : (↑t : Type u_4)
hy : (f : (a : (↑t : Type u_4)) → (↑s : Type u_4)) y = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
h₁ h₂ : (↑y : M) = (↑y : M)
⊢ x = (↑y : M)

Tactic:
rw [← Subtype.mk.inj hy]

Premises used: Subtype.mk.inj
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : LE.le (α := Submodule R M) (span R s) (span R t)
⊢ s ∪ t = t

Tactic:
have :=
    eq_of_linearIndepOn_id_of_span_subtype (hl.mono (Set.union_subset hsu htu))
      Set.subset_union_right (Set.union_subset (Set.Subset.trans subset_span hst) subset_span)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : LE.le (α := Submodule R M) (span R s) (span R t)
this : s ∪ t = t
rw : s ⊆ s ∪ t
⊢ s ⊆ t

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : LE.le (α := Submodule R M) (span R s) (span R t)
this : s ∪ t = t
⊢ s ⊆ s ∪ t

Tactic:
apply Set.subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s t u : Set M
hl : LinearIndependent.{u_4, u_2, u_4} (ι := { x : M // x ∈ u }) R (Subtype.val (p := fun (x : M) ↦ x ∈ u))
hsu : s ⊆ u
htu : t ⊆ u
⊢ LE.le (α := Submodule R M) (span R s) (span R t) ↔ s ⊆ t

Tactic:
⟨le_of_span_le_span hl hsu htu, span_mono⟩

Premises used: le_of_span_le_span, Submodule.span_mono, Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i)
i : ι
rw : ∀ (heq : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x • v x - g x • v x)) 0) (i : ι), f i = g i
⊢ f i = g i

Tactic:
rw [← sub_eq_zero, ← sum_sub_distrib] at heq

Premises used: sub_eq_zero, Finset.sum_sub_distrib
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x • v x - g x • v x)) 0
i : ι
⊢ Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x - g x) • v x) 0

Tactic:
simp_rw [← sub_smul] at heq

Premises used: sub_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
i : ι
heq : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x - g x) • v x) 0
⊢ f i = g i

Tactic:
sub_eq_zero.mp ((linearIndependent_iff'.mp hv) univ (fun i ↦ f i - g i) heq i (mem_univ i))

Premises used: Finset.mem_univ, Finset.univ, sub_eq_zero, HSub.hSub, linearIndependent_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
i : ι
heq : Eq.{u_4 + 1} (α := M) (∑ x : ι, (f x - g x) • v x) 0
⊢ f i = g i

Tactic:
exact sub_eq_zero.mp ((linearIndependent_iff'.mp hv) univ (fun i ↦ f i - g i) heq i (mem_univ i))

Premises used: Finset.mem_univ, Finset.univ, sub_eq_zero, HSub.hSub, linearIndependent_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : Disjoint (span R (range v)) f.ker
⊢ LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v)

Tactic:
(f.linearIndependent_iff_of_disjoint hf_inj).mpr hv

Premises used: Iff.mpr, LinearMap.linearIndependent_iff_of_disjoint
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
simp_rw : Disjoint (α := Submodule R M) (span R (range v)) ⊥
⊢ Disjoint (span R (range v)) f.ker

Tactic:
simp_rw [hf_inj, disjoint_bot_right]

Premises used: disjoint_bot_right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
rw :
  ∀ (hv : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) (i : R' → R)
    (j : M →+ M') (hi : ∀ (r : R'), i r = 0 → r = 0)
    (hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0)
    (hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M'))
    (s : Finset ι) (g : ι → R'),
    Eq.{u_7 + 1} (α := M') (∑ i ∈ s, HSMul.hSMul (β := M') (g i) (((⇑j : (a : M) → M') ∘ v) i)) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)

Tactic:
rw [linearIndependent_iff'] at hv ⊢

Premises used: linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
S : Finset ι
r' : ι → R'
H : Eq.{u_7 + 1} (α := M') (∑ i ∈ S, HSMul.hSMul (β := M') (r' i) (((⇑j : (a : M) → M') ∘ v) i)) 0
s : ι
hs : s ∈ S
⊢ Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') (∑ x ∈ S, i (r' x) • v x) : M') (0 : M')

Tactic:
simp_rw [comp_apply, ← hc, ← map_sum] at H

Premises used: map_sum, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') (∑ x ∈ S, i (r' x) • v x) : M') (0 : M')
⊢ r' s = 0

Tactic:
hi _ <| hv _ _ (hj _ H) s hs
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') (∑ x ∈ S, i (r' x) • v x) : M') (0 : M')
⊢ r' s = 0

Tactic:
exact hi _ <| hv _ _ (hj _ H) s hs
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : ∀ (m : M), Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') m : M') (0 : M') → m = 0
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)

Tactic:
hv.map_of_surjective_injectiveₛ i _ hi ((injective_iff_map_eq_zero _).mpr hj) hc

Premises used: Iff.mpr, LinearIndependent.map_of_surjective_injectiveₛ, injective_iff_map_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : f.ker = ⊥
simp_rw : Disjoint (α := Submodule R M) (span R (Set.range v)) ⊥
⊢ Disjoint (span R (Set.range v)) f.ker

Tactic:
simp_rw [hf_inj, disjoint_bot_right]

Premises used: disjoint_bot_right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
rw :
  ∀ (hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0)
    (x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0)
    (g : Fin (m + 1) → R),
    Eq.{u_4 + 1} (α := M)
        (∑ i : Fin (m + 1), HSMul.hSMul (β := M) (g i) (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x v i : M)) 0 →
      ∀ (i : Fin (m + 1)), g i = 0
⊢ LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M) (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x v)

Tactic:
rw [Fintype.linearIndependent_iff] at hli ⊢

Premises used: Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
total_eq :
  Eq.{u_4 + 1} (α := M)
    (∑ i : Fin (m + 1), HSMul.hSMul (β := M) (g i) (Fin.cons (α := fun (a : Fin m.succ) ↦ M) x v i : M)) 0
j : Fin (m + 1)
⊢ g 0 • x + ∑ x : Fin m, g x.succ • v x = 0

Tactic:
simp_rw [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] at total_eq

Premises used: Fin.cons_succ, Fin.sum_univ_succ, Fin.cons_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g 0 = 0

Tactic:
x_ortho (g 0) (∑ i : Fin m, g i.succ • v i) ?_ total_eq

Premises used: Finset.univ, Fin.succ, HSMul.hSMul, OfNat.ofNat, Finset.sum
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
refine : Membership.mem (γ := Submodule R M) (span R (range v)) (∑ i : Fin m, g i.succ • v i)
⊢ g 0 = 0

Tactic:
refine x_ortho (g 0) (∑ i : Fin m, g i.succ • v i) ?_ total_eq

Premises used: Finset.univ, Fin.succ, HSMul.hSMul, OfNat.ofNat, Finset.sum
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (∑ i : Fin m, g i.succ • v i)

Tactic:
sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)

Premises used: Fin.succ, Exists.intro, Submodule.span, Submodule.subset_span, Set.range, sum_mem, rfl, Submodule.smul_mem