awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
refine_2₁ :
  Eq (α := Submodule R ↥(span R (range v)))
    (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤) ⊤
refine_2₂ :
  Eq (α := Submodule R ↥(span R (range v)))
    (comap (Submodule.subtype (span R (range v))) (map (Finsupp.linearCombination R v) ⊤)) ⊤
refine_2₃ :
  LE.le (α := Submodule R M) (LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))))
    (map (Finsupp.linearCombination R v) ⊤)
refine_2₄ : LE.le (α := Submodule R M) (span R (range v)) (map (Finsupp.linearCombination R v) ⊤)
refine_2₅ : LE.le (α := Submodule R M) (span R (range v)) (LinearMap.range (Finsupp.linearCombination R v))
refine_2₆ refine_2₇ : LE.le (α := Submodule R M) (span R (range v)) (span R (range v))
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))

Tactic:
rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]

Premises used: Submodule.map_top, LinearMap.range_eq_top, LinearMap.range_le_iff_comap, Finsupp.range_linearCombination, LinearMap.map_codRestrict, LinearMap.range_eq_map, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
x : ↥(span R (range v))
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R) =
    (↑x : M)

Tactic:
Subtype.ext_iff.1 (LinearEquiv.apply_symm_apply hv.linearCombinationEquiv x)

Premises used: Subtype.ext_iff, LinearEquiv.apply_symm_apply, Iff.mp, LinearIndependent.linearCombinationEquiv
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
⊢ Finsupp.linearCombination R v ∘ₗ hv.repr = Submodule.subtype (span R (range v))

Tactic:
LinearMap.ext <| hv.linearCombination_repr

Premises used: LinearIndependent.linearCombination_repr, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
rw : (↑hv.linearCombinationEquiv.symm : ↥(span R (range v)) →ₗ[R] ι →₀ R).ker = ⊥
rw₁ rw₂ : Eq.{u_4 + 1} (α := Submodule R ↥(span R (range v))) ⊥ ⊥
⊢ hv.repr.ker = ⊥

Tactic:
rw [LinearIndependent.repr, LinearEquiv.ker]

Premises used: LinearEquiv.ker, LinearIndependent.repr
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
rw : (↑hv.linearCombinationEquiv.symm : ↥(span R (range v)) →ₗ[R] ι →₀ R).range = ⊤
rw₁ rw₂ : Eq (α := Submodule R (ι →₀ R)) ⊤ ⊤
⊢ hv.repr.range = ⊤

Tactic:
rw [LinearIndependent.repr, LinearEquiv.range]

Premises used: LinearIndependent.repr, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
⊢ Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)

Tactic:
have :
    ↑((LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l) =
      Finsupp.linearCombination R v l :=
    rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
⊢ (↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) : M) =
    (↑x : M)

Tactic:
rw [eq] at this
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this :
  (↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) : M) =
    (↑x : M)
⊢ ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x

Tactic:
Subtype.ext_iff.2 this

Premises used: Iff.mpr, Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this :
  (↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) : M) =
    (↑x : M)
⊢ ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x

Tactic:
exact Subtype.ext_iff.2 this

Premises used: Iff.mpr, Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
⊢ ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x

Tactic:
have : (LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x := by
    rw [eq] at this
    exact Subtype.ext_iff.2 this
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this_1 :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
this : ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
rw :
  Eq (α := ι →₀ R) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R)
    ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
        ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)
⊢ (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x = l

Tactic:
rw [← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l]

Premises used: LinearEquiv.symm_apply_apply, LinearIndependent.linearCombinationEquiv
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this_1 :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
this : ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
rw :
  Eq (α := ι →₀ R)
    ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R)
        (((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)
    ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
        ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)
⊢ Eq (α := ι →₀ R) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R)
    ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
        ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = (↑x : M)
this_1 :
  Eq.{u_4 + 1} (α := M)
    ((↑(((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
        M) :
      M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
this : ((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l = x
⊢ Eq (α := ι →₀ R)
    ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R)
        (((↑hv.linearCombinationEquiv : (ι →₀ R) →ₗ[R] ↥(span R (range v))) : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)
    ((hv.linearCombinationEquiv.symm : (a : ↥(span R (range v))) → ι →₀ R)
        ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v))) l) :
      ι →₀ R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
x : ↥(span R (range v))
hx : (↑x : M) = v i
apply : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) = (↑x : M)
⊢ Eq (α := ι →₀ R) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x : ι →₀ R) (Finsupp.single i 1 : ι →₀ R)

Tactic:
apply hv.repr_eq

Premises used: LinearIndependent.repr_eq
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
x : ↥(span R (range v))
hx : (↑x : M) = v i
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) = (↑x : M)

Tactic:
simp [Finsupp.linearCombination_single, hx]

Premises used: Finsupp.linearCombination_single
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
inst_3 : Nontrivial R
x : ↥(span R (range v))
a :
  Eq.{u_4 + 1} (α := ↥(span R (range v)))
    ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x)) :
      ↥(span R (range v)))
    ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
      ↥(span R (range v)))
⊢ Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) =
    (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x

Tactic:
apply (LinearIndependent.linearCombinationEquiv hv).injective

Premises used: LinearIndependent.linearCombinationEquiv, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
inst_3 : Nontrivial R
x : ↥(span R (range v))
a :
  Eq.{u_4 + 1} (α := M)
    (↑((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
          (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x))) :
      M)
    (↑((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
          ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x)) :
      M)
⊢ Eq.{u_4 + 1} (α := ↥(span R (range v)))
    ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x)) :
      ↥(span R (range v)))
    ((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
        ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
      ↥(span R (range v)))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
inst_3 : Nontrivial R
x : ↥(span R (range v))
⊢ Eq.{u_4 + 1} (α := M)
    (↑((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
          (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x))) :
      M)
    (↑((hv.linearCombinationEquiv : (a : ι →₀ R) → ↥(span R (range v)))
          ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x)) :
      M)

Tactic:
simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
      LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
      Span.finsupp_linearCombination_repr]

Premises used: LinearIndependent.linearCombination_repr, LinearIndependent.linearCombinationEquiv_apply_coe, Span.finsupp_linearCombination_repr, Finsupp.linearCombination_equivMapDomain, Equiv.self_comp_ofInjective_symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
inst_3 : Nontrivial R
x : ↥(span R (range v))
⊢ Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) =
    (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x

Tactic:
have p :
    (Span.repr R (Set.range v) x).equivMapDomain (Equiv.ofInjective _ hv.injective).symm =
      hv.repr x := by
    apply (LinearIndependent.linearCombinationEquiv hv).injective
    ext
    simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
      LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
      Span.finsupp_linearCombination_repr]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
inst_3 : Nontrivial R
x : ↥(span R (range v))
p :
  Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) =
    (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x
h :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((Span.repr R (range v) x : (a : (↑(range v) : Type u_4)) → R)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ range v) (v i) ⋯) :
        R)
      ((Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
            (a : (↑(range v) : Type u_4)) → R)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ range v) (v i) ⋯) :
        R)
⊢ Span.repr R (range v) x =
    Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x)

Tactic:
ext ⟨_, ⟨i, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
inst_3 : Nontrivial R
x : ↥(span R (range v))
p :
  Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) =
    (hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x
i : ι
⊢ Eq.{u_2 + 1} (α := R)
    ((Span.repr R (range v) x : (a : (↑(range v) : Type u_4)) → R)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ range v) (v i) ⋯) :
      R)
    ((Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) ((hv.repr : (a : ↥(span R (range v))) → ι →₀ R) x) :
          (a : (↑(range v) : Type u_4)) → R)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ range v) (v i) ⋯) :
      R)

Tactic:
simp [← p]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha : Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i)
⊢ ∃ (y : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) y ∧
      (Finsupp.linearCombination R v : (a : ι →₀ R) → M) y = a • v i

Tactic:
rw [Finsupp.span_image_eq_map_linearCombination, mem_map] at ha

Premises used: Submodule.mem_map, Finsupp.span_image_eq_map_linearCombination
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha :
  ∃ (y : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) y ∧
      (Finsupp.linearCombination R v : (a : ι →₀ R) → M) y = a • v i
rcases :
  ∀ (l : ι →₀ R) (hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) l)
    (e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i), a = 0
⊢ a = 0

Tactic:
rcases ha with ⟨l, hl, e⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) l
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i a) : M)

Tactic:
simp [e]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) l
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
⊢ Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)

Tactic:
rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl

Premises used: linearIndependent_iffₛ, Iff.mp, Finsupp.single
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) l
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
hl₁ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i

Tactic:
rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl

Premises used: linearIndependent_iffₛ, Iff.mp, Finsupp.single
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
by_contra : ∀ (hn : ¬a = 0), False
⊢ a = 0

Tactic:
by_contra hn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
hn : ¬a = 0
⊢ i ∈ (↑(Finsupp.support (Finsupp.single i a)) : Set ι)

Tactic:
simp [hn]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i})) (Finsupp.single i a)
e : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = a • v i
hn : ¬a = 0
⊢ False

Tactic:
exact (notMem_of_mem_diff (hl <| by simp [hn])) (mem_singleton _)

Premises used: Set.mem_singleton, Set.notMem_of_mem_diff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
hv : LinearIndepOn R v s
hi : i ∈ s
a : R
ha : Membership.mem (γ := Submodule R M) (span R (v '' (s \ {i}))) (a • v i)
⊢ Membership.mem (γ := Submodule R M)
    (span R ((fun (x : (↑s : Type u')) ↦ v (↑x : ι)) '' (univ \ {Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi})))
    (a • v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
simpa [← comp_def, image_comp, image_diff Subtype.val_injective]

Premises used: Subtype.val_injective, Set.image_diff, Function.comp_def, Set.image_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
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
i : ι
hi : Membership.mem (γ := Submodule R M) (span R (v '' {i}ᶜ)) (v i)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (HSMul.hSMul.{u_2, u_4, u_4} (α := R) 1 (v i))

Tactic:
simpa [Set.compl_eq_univ_diff] using hi

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
inst_3 : Nontrivial R
hv : LinearIndepOn R v s
hi : i ∈ s
hi' : Membership.mem (γ := Submodule R M) (span R (v '' (s \ {i}))) (v i)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (s \ {i}))) (HSMul.hSMul.{u_2, u_4, u_4} (α := R) 1 (v i))

Tactic:
simpa [Set.compl_eq_univ_diff] using hi'

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
inst_3 : Nontrivial R
hv : LinearIndepOn R v (insert i s)
hi : i ∉ s
⊢ v i ∉ span R (v '' s)

Tactic:
simpa [hi] using hv.notMem_span <| mem_insert ..

Premises used: LinearIndepOn.notMem_span, Set.mem_insert
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
mp : i.Maximal → ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
mpr : (∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j) → i.Maximal
⊢ i.Maximal ↔ ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j

Tactic:
constructor