awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
dsimp : LinearIndepOn R v (⋃ I ∈ c, (↑I : Set ι))
⊢ indep (⋃ I ∈ c, (↑I : Set ι))

Tactic:
dsimp [indep]
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
rw :
  ∀ (f : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f →
      ∀ (g : ι →₀ R),
        Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g →
          Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
              ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) →
            f = g
⊢ LinearIndepOn R v (⋃ I ∈ c, (↑I : Set ι))

Tactic:
rw [linearIndepOn_iffₛ]

Premises used: linearIndepOn_iffₛ
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
inl :
  ∀ (hc : IsChain r ∅)
    (hfsupp :
      Membership.mem (γ := Submodule R (ι →₀ R))
        (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f)
    (hgsupp :
      Membership.mem (γ := Submodule R (ι →₀ R))
        (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g),
    f = g
inr : ∀ (hn : c.Nonempty), f = g
⊢ f = g

Tactic:
rcases eq_empty_or_nonempty c with (rfl | hn)

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
f g : ι →₀ R
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hc : IsChain r ∅
hfsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f
hgsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g
⊢ f = 0

Tactic:
simpa using hfsupp
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
f g : ι →₀ R
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hc : IsChain r ∅
hfsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f
hgsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g
⊢ g = 0

Tactic:
simpa using hgsupp
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
f g : ι →₀ R
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hc : IsChain r ∅
hfsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f
hgsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g
inl : 0 = g
inl₁ inl₂ : Eq (α := ι →₀ R) 0 0
⊢ f = g

Tactic:
rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
⊢ Std.Refl r

Tactic:
haveI : Std.Refl r := ⟨fun _ => Set.Subset.refl _⟩
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
⊢ (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ ⋃ i ∈ c, (↑i : Set ι)

Tactic:
simpa using And.intro hfsupp hgsupp

Premises used: And.intro
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
inr : ∀ (I : X) (_I_mem : I ∈ c) (hI : (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ (↑I : Set ι)), f = g
⊢ f = g

Tactic:
obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp

Premises used: Finsupp.support, SetLike.coe, Union.union
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
I : X
_I_mem : I ∈ c
hI : (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ (↑I : Set ι)
⊢ f = g

Tactic:
linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum

Premises used: linearIndepOn_iffₛ, Set.subset_union_right, HasSubset.Subset.trans, Set.subset_union_left, Iff.mp, Subtype.property
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
I : X
_I_mem : I ∈ c
hI : (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ (↑I : Set ι)
⊢ f = g

Tactic:
exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum

Premises used: linearIndepOn_iffₛ, Set.subset_union_right, HasSubset.Subset.trans, Set.subset_union_left, Iff.mp, Subtype.property
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
inr : ∀ (I : X) (_I_mem : I ∈ c) (hI : (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ (↑I : Set ι)), f = g
⊢ f = g

Tactic:
classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum

Premises used: Finsupp.support, SetLike.coe, Union.union
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
⊢ ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, (↑I : Set ι))

Tactic:
have key : ∀ c : Set X, IsChain r c → indep (⋃ (I : X) (_ : I ∈ c), I) := by
    intro c hc
    dsimp [indep]
    rw [linearIndepOn_iffₛ]
    intro f hfsupp g hgsupp hsum
    rcases eq_empty_or_nonempty c with (rfl | hn)
    · rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
    haveI : Std.Refl r := ⟨fun _ => Set.Subset.refl _⟩
    classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, (↑I : Set ι))
obtain :
  ∀ (I : Set ι) (hli : indep I)
    (hmax :
      ∀ (a : X),
        r (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli) a →
          r a (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli)),
    ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
⊢ ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
    exists_maximal_of_chains_bounded (r := r)
      (fun c hc => ⟨⟨⋃ I ∈ c, (I : Set ι), key c hc⟩, fun I => Set.subset_biUnion_of_mem⟩)
      Set.Subset.trans

Premises used: exists_maximal_of_chains_bounded, Set.Subset.trans, Set.subset_biUnion_of_mem, Subtype.mk, Exists.intro, Subtype.val, Set.iUnion
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, (↑I : Set ι))
I : Set ι
hli : indep I
hmax :
  ∀ (a : X),
    r (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli) a → r a (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli)
⊢ ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
⟨I, hli, fun J hsub hli => Set.Subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩

Premises used: Set.Subset.antisymm, Subtype.mk, And.intro, Exists.intro
-- 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
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, (↑I : Set ι))
I : Set ι
hli : indep I
hmax :
  ∀ (a : X),
    r (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli) a → r a (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli)
⊢ ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
exact ⟨I, hli, fun J hsub hli => Set.Subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩
-- 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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
rw :
  Codisjoint (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R s))
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R t))
⊢ Codisjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))

Tactic:
rw [Finsupp.span_image_eq_map_linearCombination, Finsupp.span_image_eq_map_linearCombination]

Premises used: Finsupp.span_image_eq_map_linearCombination
-- 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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R s))
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R t))

Tactic:
Submodule.codisjoint_map ?_ (Finsupp.codisjoint_supported_supported hst)

Premises used: Submodule.codisjoint_map, Finsupp.codisjoint_supported_supported
-- 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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
refine : Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)
⊢ Codisjoint (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R s))
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R t))

Tactic:
refine Submodule.codisjoint_map ?_ (Finsupp.codisjoint_supported_supported hst)

Premises used: Submodule.codisjoint_map, Finsupp.codisjoint_supported_supported
-- 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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
rwa : Eq (α := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v)) ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : Eq (α := Submodule R M) (span R (range v)) ⊤
⊢ Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)

Tactic:
rwa [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination
-- 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
h₁ : LinearIndependent R v
h₂ : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : IsCompl s t
⊢ IsCompl (α := Submodule R M) (span R (v '' s)) (span R (v '' t))

Tactic:
⟨h₁.disjoint_span_image hst.1, Submodule.codisjoint_span_image_of_codisjoint h₂ hst.2⟩

Premises used: Submodule.codisjoint_span_image_of_codisjoint, LinearIndependent.disjoint_span_image, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
inst_3 : Fintype ι
inst_4 : DecidableEq ι
⊢ LinearIndependent R v ↔
    Eq (α := Submodule R ((i : ι) → R))
      (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R)
        ((LinearMap.lsum R (fun (x : ι) ↦ R) ℕ : (a : (i : ι) → R →ₗ[R] M) → ((i : ι) → R) →ₗ[R] M) fun (i : ι) ↦
          LinearMap.smulRight LinearMap.id (v i)))
      ⊥

Tactic:
simp [Fintype.linearIndependent_iff, LinearMap.ker_eq_bot', funext_iff]

Premises used: funext_iff, LinearMap.ker_eq_bot', Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
rw [linearIndepOn_iff'']

Premises used: linearIndepOn_iff''
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
refine_2 :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
⊢ (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h :
  ∀ (t : Finset ι) (g : ι → R),
    (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ (↑{i, j} : Set ι) ⊆ {i, j} →
    (∀ i_1 ∉ {i, j},
        HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
            (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 =
          0) →
      Eq.{u_4 + 1} (α := M)
          (∑ i_1 ∈ {i, j},
            HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
                (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 •
              f i_1)
          0 →
        ∀ (i_1 : ι),
          Membership.mem (γ := Finset ι) {i, j} i_1 →
            HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
                (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 =
              0

Tactic:
specialize h {i, j} (Pi.single i c + Pi.single j d)

Premises used: Insert.insert, Pi.single, HAdd.hAdd, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
c d : R
hcd : c • f i + d • f j = 0
h :
  (↑{i, j} : Set ι) ⊆ {i, j} →
    (∀ i_1 ∉ {i, j},
        HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
            (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 =
          0) →
      Eq.{u_4 + 1} (α := M)
          (∑ i_1 ∈ {i, j},
            HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
                (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 •
              f i_1)
          0 →
        ∀ (i_1 : ι),
          Membership.mem (γ := Finset ι) {i, j} i_1 →
            HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
                (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 =
              0
⊢ c = 0 ∧ d = 0

Tactic:
simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h

Premises used: Finset.sum_pair, Pi.single_apply, Ne.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
⊢ t ⊆ {i, j}

Tactic:
simpa [← Finset.coe_subset]

Premises used: Finset.coe_subset