awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∉ s
h : ¬Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ False

Tactic:
xs (h₁ <| Finsupp.mem_support_iff.2 h)

Premises used: Iff.mpr, Finsupp.mem_support_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∉ s
h : ¬Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ False

Tactic:
exact xs (h₁ <| Finsupp.mem_support_iff.2 h)

Premises used: Iff.mpr, Finsupp.mem_support_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : Equiv.{u_1 + 1, u_7 + 1} (↑s : Type u_1) (↑t : Type u_7)
haveI : (this : DecidablePred fun (x : α) ↦ x ∈ s) → ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
haveI := Classical.decPred fun x => x ∈ s
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : Equiv.{u_1 + 1, u_7 + 1} (↑s : Type u_1) (↑t : Type u_7)
this : DecidablePred fun (x : α) ↦ x ∈ s
haveI : (this : DecidablePred fun (x : α') ↦ x ∈ t) → ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
haveI := Classical.decPred fun x => x ∈ t
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : Equiv.{u_1 + 1, u_7 + 1} (↑s : Type u_1) (↑t : Type u_7)
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
this : DecidablePred fun (x : α') ↦ x ∈ t
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
exact Finsupp.supportedEquivFinsupp s ≪≫ₗ
    (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)

Premises used: LinearEquiv.symm, Finsupp.supportedEquivFinsupp, Finsupp.domLCongr, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : ∀ (i : ι), Free.{u_2, u_3} R (M i)
⊢ Free R (Π₀ (i : ι), M i)

Tactic:
.of_basis <| DFinsupp.basis fun i => Module.Free.chooseBasis R (M i)

Premises used: DFinsupp.basis, Module.Free.of_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
h :
  ∀ (a : (i : ι) × φ i) (i : ι),
    (((linearCombination R fun (ix : (i : ι) × φ i) ↦
                  single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
                    (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))) ∘ₗ
                Finsupp.lsingle a :
              (a : R) → Π₀ (i : ι), M i)
            1 :
          (a : ι) → M a)
        i =
      ((((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
                    linearCombination R (f i)) ∘ₗ
                  (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) ∘ₗ
                Finsupp.lsingle a :
              (a : R) → Π₀ (i : ι), M i)
            1 :
          (a : ι) → M a)
        i
⊢ Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
a : (i : ι) × φ i
i : ι
⊢ (((linearCombination R fun (ix : (i : ι) × φ i) ↦
                single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
                  (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))) ∘ₗ
              Finsupp.lsingle a :
            (a : R) → Π₀ (i : ι), M i)
          1 :
        (a : ι) → M a)
      i =
    ((((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
                  linearCombination R (f i)) ∘ₗ
                (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) ∘ₗ
              Finsupp.lsingle a :
            (a : R) → Π₀ (i : ι), M i)
          1 :
        (a : ι) → M a)
      i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))

Tactic:
have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
rw :
  Function.Injective (α := (i : ι) × φ i →₀ R) (β := Π₀ (i : ι), M i)
    (⇑((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
            linearCombination R (f i)) ∘ₗ
          (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) :
      (a : (i : ι) × φ i →₀ R) → Π₀ (i : ι), M i)
⊢ LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))

Tactic:
rw [LinearIndependent, this]

Premises used: LinearIndependent
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
⊢ Function.Injective (α := (i : ι) × φ i →₀ R) (β := Π₀ (i : ι), M i)
    (⇑((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
            linearCombination R (f i)) ∘ₗ
          (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) :
      (a : (i : ι) × φ i →₀ R) → Π₀ (i : ι), M i)

Tactic:
((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)

Premises used: Iff.mpr, map_zero, DFinsupp.mapRange, DFinsupp.mapRange_injective, Function.Injective.comp, Equiv.injective
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
⊢ Function.Injective (α := (i : ι) × φ i →₀ R) (β := Π₀ (i : ι), M i)
    (⇑((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
            linearCombination R (f i)) ∘ₗ
          (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) :
      (a : (i : ι) × φ i →₀ R) → Π₀ (i : ι), M i)

Tactic:
exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)

Premises used: Iff.mpr, map_zero, DFinsupp.mapRange_injective, Function.Injective.comp, Equiv.injective
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
⊢ (LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))) ↔
    ∀ (i : ι), LinearIndependent R (f i)

Tactic:
⟨fun h i ↦ (h.comp _ sigma_mk_injective).of_comp (lsingle i), linearIndependent_single _⟩

Premises used: LinearIndependent.of_comp, Iff.intro, DFinsupp.lsingle, Sigma.mk, LinearIndependent.comp, DFinsupp.linearIndependent_single, sigma_mk_injective
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent (ι := (i : ι) × φ i) R (M := ι →₀ M)
    (Function.comp (β := Π₀ (i : ι), M)
      (⇑(↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (Π₀ (x : ι), M) →ₗ[R] ι →₀ M) : (a : Π₀ (i : ι), M) → ι →₀ M)
      fun (ix : (i : ι) × φ i) ↦
      DFinsupp.single (β := fun (i : ι) ↦ M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))

Tactic:
(DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn

Premises used: LinearEquiv.symm, Function.Injective.injOn, LinearIndependent.map_injOn, finsuppLequivDFinsupp, LinearEquiv.injective, DFinsupp.linearIndependent_single
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
h :
  ∀ (x : (i : ι) × φ i),
    Eq (α := ι →₀ M)
      (single (x.fst (β := fun (i : ι) ↦ φ i)) (f (x.fst (β := fun (i : ι) ↦ φ i)) (x.snd (β := fun (i : ι) ↦ φ i))))
      (Function.comp (β := Π₀ (i : ι), M)
        (⇑(↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (Π₀ (x : ι), M) →ₗ[R] ι →₀ M) : (a : Π₀ (i : ι), M) → ι →₀ M)
        (fun (ix : (i : ι) × φ i) ↦
          DFinsupp.single (β := fun (i : ι) ↦ M) (ix.fst (β := fun (i : ι) ↦ φ i))
            (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
        x)
⊢ LinearIndependent R (M := ι →₀ M) fun (ix : (i : ι) × φ i) ↦
    single (ix.fst (β := fun (i : ι) ↦ φ i)) (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))

Tactic:
convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn

Premises used: LinearEquiv.symm, Function.Injective.injOn, LinearIndependent.map_injOn, finsuppLequivDFinsupp, LinearEquiv.injective, DFinsupp.linearIndependent_single
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
x : (i : ι) × φ i
⊢ Eq (α := ι →₀ M)
    (single (x.fst (β := fun (i : ι) ↦ φ i)) (f (x.fst (β := fun (i : ι) ↦ φ i)) (x.snd (β := fun (i : ι) ↦ φ i))))
    (Function.comp (β := Π₀ (i : ι), M)
      (⇑(↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (Π₀ (x : ι), M) →ₗ[R] ι →₀ M) : (a : Π₀ (i : ι), M) → ι →₀ M)
      (fun (ix : (i : ι) × φ i) ↦
        DFinsupp.single (β := fun (i : ι) ↦ M) (ix.fst (β := fun (i : ι) ↦ φ i))
          (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
      x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
h :
  ∀ (x : (i : ι) × φ i),
    Eq (α := ι →₀ M)
      (single (x.fst (β := fun (i : ι) ↦ φ i)) (f (x.fst (β := fun (i : ι) ↦ φ i)) (x.snd (β := fun (i : ι) ↦ φ i))))
      (Function.comp (β := Π₀ (i : ι), M)
        (⇑(↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (Π₀ (x : ι), M) →ₗ[R] ι →₀ M) : (a : Π₀ (i : ι), M) → ι →₀ M)
        (fun (ix : (i : ι) × φ i) ↦
          DFinsupp.single (β := fun (i : ι) ↦ M) (ix.fst (β := fun (i : ι) ↦ φ i))
            (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
        x)
⊢ LinearIndependent R (M := ι →₀ M) fun (ix : (i : ι) × φ i) ↦
    single (ix.fst (β := fun (i : ι) ↦ φ i)) (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))

Tactic:
classical
  convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn
  simp
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
⊢ (LinearIndependent R (M := ι →₀ M) fun (ix : (i : ι) × φ i) ↦
      single (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))) ↔
    ∀ (i : ι), LinearIndependent R (f i)

Tactic:
⟨fun h i ↦ (h.comp _ sigma_mk_injective).of_comp (lsingle i), linearIndependent_single _⟩

Premises used: LinearIndependent.of_comp, Iff.intro, Finsupp.linearIndependent_single, Sigma.mk, LinearIndependent.comp, sigma_mk_injective, Finsupp.lsingle
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
g : ι →₀ M
ix : (i : ι) × φ i
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R) g : (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        ix :
      R)
    ((((Basis.repr (b (ix.fst (β := fun (i : ι) ↦ φ i))) : (a : M) → φ ix.fst →₀ R)
              ((g : (a : ι) → M) (ix.fst (β := fun (i : ι) ↦ φ i))) :
            Finsupp.{u_4, u_1} (φ (ix.fst (β := fun (i : ι) ↦ φ i))) R) :
          (a : φ ix.fst) → R)
        (ix.snd (β := fun (i : ι) ↦ φ i)) :
      R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
h :
  ∀ (j : ι) (y : φ j),
    Eq.{u_1 + 1} (α := R)
      (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
                (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                  ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                    ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
              (i : ι) × φ i →₀ R) :
            (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
      ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
⊢ Eq (α := (i : ι) × φ i →₀ R)
    (((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
        (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
          ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
            ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
      (i : ι) × φ i →₀ R)
    (single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (i : ι) × φ i →₀ R)

Tactic:
ext ⟨j, y⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
pos :
  ∀ (h : i = j),
    Eq.{u_1 + 1} (α := R)
      (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
                (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                  ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                    ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
              (i : ι) × φ i →₀ R) :
            (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
      ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
neg :
  ∀ (h : ¬i = j),
    Eq.{u_1 + 1} (α := R)
      (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
                (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                  ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                    ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
              (i : ι) × φ i →₀ R) :
            (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
      ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)

Tactic:
by_cases h : i = j
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
pos :
  ∀ (y : φ i),
    Eq.{u_1 + 1} (α := R)
      (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
                (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                  ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                    ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
              (i : ι) × φ i →₀ R) :
            (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) i y) :
        R)
      ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) i y) :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)

Tactic:
cases h
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x y : φ i
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) i y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) i y) :
      R)

Tactic:
simp [Finsupp.single_apply_left sigma_mk_injective]

Premises used: Finsupp.single_apply_left, sigma_mk_injective