awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
a : ι
w : Set ι
right : a ∈ w
i : η
h_1 : (fun (x : η) ↦ s x) i = w
⊢ Membership.mem (γ := Set ι) ∅ a

Tactic:
hη ⟨i⟩

Premises used: Set.Mem, Nonempty.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
a : ι
w : Set ι
right : a ∈ w
i : η
h_1 : (fun (x : η) ↦ s x) i = w
⊢ Membership.mem (γ := Set ι) ∅ a

Tactic:
exact hη ⟨i⟩

Premises used: Nonempty.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
s : Set (Set ι)
hs : DirectedOn (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
rw : LinearIndepOn R v (⋃ (i : (↑s : Type u')), (↑i : Set ι))
⊢ LinearIndepOn R v (⋃₀ s)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
s : Set (Set ι)
hs : DirectedOn (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ ∀ (i : (↑s : Type u')), LinearIndepOn R v (↑i : Set ι)

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
s : Set (Set ι)
hs : DirectedOn (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃ (i : (↑s : Type u')), (↑i : Set ι))

Tactic:
exact linearIndepOn_iUnion_of_directed hs.directed_val (by simpa using h)

Premises used: linearIndepOn_iUnion_of_directed, DirectedOn.directed_val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
rw : LinearIndepOn R v (⋃ (x : (↑s : Type u_6)), t (↑x : η))
⊢ LinearIndepOn R v (⋃ a ∈ s, t a)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ ∀ (i : (↑s : Type u_6)), LinearIndepOn R v (t (↑i : η))

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ (x : (↑s : Type u_6)), t (↑x : η))

Tactic:
exact linearIndepOn_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)

Premises used: Iff.mpr, linearIndepOn_iUnion_of_directed, DirectedOn.directed_val, directed_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ iSupIndep (α := Submodule R (ι →₀ M)) fun (i : ι) ↦ LinearMap.range (Finsupp.lsingle i)

Tactic:
fun i ↦ disjoint_iff_inf_le.mpr ?_

Premises used: Iff.mpr, iSupIndep, disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
refine :
  ∀ (i : ι),
    LE.le (α := Submodule R (ι →₀ M))
      ((fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) i ⊓
        ⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j)
      ⊥
⊢ iSupIndep (α := Submodule R (ι →₀ M)) fun (i : ι) ↦ LinearMap.range (Finsupp.lsingle i)

Tactic:
refine fun i ↦ disjoint_iff_inf_le.mpr ?_

Premises used: Iff.mpr, disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
this :
  LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)
⊢ (↑(Finsupp.support.{u', u_4} (M := M) ((Finsupp.lsingle i : (a : M) → ι →₀ M) m)) : Set ι) ⊆ {i}ᶜ

Tactic:
have := (Finsupp.mem_supported ..).mp (this hm)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
this_1 :
  LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)
this : (↑(Finsupp.support.{u', u_4} (M := M) ((Finsupp.lsingle i : (a : M) → ι →₀ M) m)) : Set ι) ⊆ {i}ᶜ
⊢ Membership.mem (α := ι →₀ M) (γ := Submodule R (ι →₀ M)) ⊥ ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
suffices :
  LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)
⊢ Membership.mem (α := ι →₀ M) (γ := Submodule R (ι →₀ M)) ⊥ ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)

Tactic:
suffices ⨆ j ≠ i, LinearMap.range (Finsupp.lsingle j) ≤ Finsupp.supported M R {i}ᶜ by
    have := (Finsupp.mem_supported ..).mp (this hm); simp_all
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
⊢ LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)

Tactic:
iSup₂_le fun j ne ↦ ?_

Premises used: iSup₂_le, Set.Mem, setOf
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m : ι →₀ M)
refine :
  ∀ (j : ι) (ne : j ≠ i),
    LE.le (α := Submodule R (ι →₀ M)) (LinearMap.range (Finsupp.lsingle j)) (Finsupp.supported M R {i}ᶜ)
⊢ LE.le (α := Submodule R (ι →₀ M)) (⨆ (j : ι), ⨆ (_ : j ≠ i), LinearMap.range (Finsupp.lsingle j))
    (Finsupp.supported M R {i}ᶜ)

Tactic:
refine iSup₂_le fun j ne ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι
m_1 : M
hm :
  Membership.mem (α := ι →₀ M)
    (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), (fun (i : ι) ↦ (LinearMap.range (Finsupp.lsingle i) : Submodule R (ι →₀ M))) j) :
      Set (ι →₀ M))
    ((Finsupp.lsingle i : (a : M) → ι →₀ M) m_1 : ι →₀ M)
j : ι
ne : j ≠ i
m : M
⊢ Membership.mem (α := ι →₀ M) (γ := Submodule R (ι →₀ M)) (Finsupp.supported M R {i}ᶜ)
    ((Finsupp.lsingle j : (a : M) → ι →₀ M) m : ι →₀ M)

Tactic:
simp [Finsupp.mem_supported, ne]

Premises used: Finsupp.mem_supported
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : iSupIndep m
simp_rw :
  ∀ (ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥) (i : ι),
    map f (m i) ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j) ≤ ⊥
⊢ iSupIndep.{u' + 1, u_5} (α := Submodule R M') fun (i : ι) ↦ map f (m i)

Tactic:
simp_rw [iSupIndep, disjoint_iff_inf_le] at ind ⊢

Premises used: iSupIndep, disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j)) : Set M') ((f : (a : M) → M') x : M')
rw : Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') 0 : M')
rw₁ : x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)
⊢ Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') x : M')

Tactic:
rw [ind i ⟨hxi, _⟩]

Premises used: And.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j)) : Set M') ((f : (a : M) → M') x : M')
⊢ Membership.mem.{u_5, u_5} (α := M') (γ := Submodule R M') ⊥ ((f : (a : M) → M') 0 : M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), map f (m j)) : Set M') ((f : (a : M) → M') x : M')
⊢ Membership.mem (α := M') (↑(map f (⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1)) : Set M') ((f : (a : M) → M') x : M')

Tactic:
simp_rw [← Submodule.map_iSup] at hx

Premises used: Submodule.map_iSup
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(map f (⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1)) : Set M') ((f : (a : M) → M') x : M')
have :
  ∀ (y : M) (hy : y ∈ (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1) : Set M))
    (eq : Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') y : M') ((f : (a : M) → M') x : M')),
    x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)
⊢ x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)

Tactic:
have ⟨y, hy, eq⟩ := hx
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inj : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ (j : ι), ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ (↑(m i) : Set M)
hx : Membership.mem (α := M') (↑(map f (⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1)) : Set M') ((f : (a : M) → M') x : M')
y : M
hy : y ∈ (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), m i_1) : Set M)
eq : Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') y : M') ((f : (a : M) → M') x : M')
⊢ x ∈ (↑(⨆ (j : ι), ⨆ (_ : j ≠ i), m j) : Set M)

Tactic:
simpa [← inj eq]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
⊢ iSupIndep.{u' + 1, u_4} (α := Submodule R M) fun (i : ι) ↦
    Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle i))

Tactic:
LinearMap.iSupIndep_map _ hv (iSupIndep_range_lsingle ι R R)

Premises used: LinearMap.iSupIndep_map, iSupIndep_range_lsingle
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
h :
  ∀ (x : ι),
    Eq (α := Submodule R M) (R ∙ v x)
      (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x)))
⊢ iSupIndep.{u' + 1, u_4} (α := Submodule R M) fun (i : ι) ↦ R ∙ v i

Tactic:
convert! LinearMap.iSupIndep_map _ hv (iSupIndep_range_lsingle ι R R)

Premises used: LinearMap.iSupIndep_map, iSupIndep_range_lsingle
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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 : ι
h :
  ∀ (x_1 : M),
    Membership.mem (γ := Submodule R M) (R ∙ v x) x_1 ↔
      Membership.mem (γ := Submodule R M)
        (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x))) x_1
⊢ Eq (α := Submodule R M) (R ∙ v x)
    (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x)))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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 : ι
x_1 : M
⊢ Membership.mem (γ := Submodule R M) (R ∙ v x) x_1 ↔
    Membership.mem (γ := Submodule R M)
      (Submodule.map (Finsupp.linearCombination R v) (LinearMap.range (Finsupp.lsingle x))) x_1

Tactic:
simp [mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
h :
  ∀ (val : ι),
    Eq.{u_4 + 1} (α := M)
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
h₁ :
  ∀ (val : ι),
    Eq.{u_5 + 1} (α := M')
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).2
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).2
h₂ :
  ∀ (val : ι'),
    Eq.{u_4 + 1} (α := M)
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inr val) :
            (a : R) → M × M')
          1).1
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inr val) :
            (a : R) → M × M')
          1).1
h₃ :
  ∀ (val : ι'),
    Eq.{u_5 + 1} (α := M')
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inr val) :
            (a : R) → M × M')
          1).2
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inr val) :
            (a : R) → M × M')
          1).2
⊢ Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))

Tactic:
ext (_ | _)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val : ι
⊢ Eq.{u_4 + 1} (α := M)
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).1
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val : ι
⊢ Eq.{u_5 + 1} (α := M')
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).2
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inl val) :
          (a : R) → M × M')
        1).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val : ι'
⊢ Eq.{u_4 + 1} (α := M)
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).1
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val : ι'
⊢ Eq.{u_5 + 1} (α := M')
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).2
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))

Tactic:
have : linearCombination R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) =
      .prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (sumFinsuppLEquivProdFinsupp R).toLinearMap := by ext (_ | _) <;> simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
rw :
  Injective (α := ι ⊕ ι' →₀ R) (β := M × M')
    (⇑(prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
          (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) :
      (a : ι ⊕ ι' →₀ R) → M × M')
⊢ LinearIndependent R (M := M × M')
    (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v'))

Tactic:
rw [LinearIndependent, this]

Premises used: LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
⊢ Injective (α := ι ⊕ ι' →₀ R) (β := M × M')
    (⇑(prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
          (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) :
      (a : ι ⊕ ι' →₀ R) → M × M')

Tactic:
simpa [LinearMap.coe_prodMap] using ⟨hv, hv'⟩

Premises used: LinearMap.coe_prodMap