awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
h : Nontrivial R
this : InjOn f s
⊢ LinearIndepOn R g (f '' s)

Tactic:
(linearIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

Premises used: linearIndependent_equiv', Equiv.Set.imageOfInjOn, Iff.mp, rfl, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
h : Nontrivial R
this : InjOn f s
⊢ LinearIndepOn R g (f '' s)

Tactic:
exact (linearIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hs : LinearIndepOn R v s
⊢ LinearIndepOn R id (v '' s)

Tactic:
LinearIndepOn.image_of_comp v id hs

Premises used: LinearIndepOn.image_of_comp, id
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
inst_3 : Nontrivial R
⊢ LinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ InjOn v s

Tactic:
⟨fun h ↦ ⟨h.id_image, h.injOn⟩, fun h ↦ (linearIndepOn_iff_image h.2).2 h.1⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Iff.intro, linearIndepOn_iff_image, LinearIndepOn.id_image, LinearIndepOn.injOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → M
h : EqOn v w s
⊢ (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → M
h : EqOn v w s
h₁ : Eq (α := (↑s : Type u') → M) (fun (x : (↑s : Type u')) ↦ w (↑x : ι)) fun (x : (↑s : Type u')) ↦ v (↑x : ι)
⊢ (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ w (↑x : ι)

Tactic:
convert! Iff.rfl using 2

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → M
h : EqOn v w s
h₁ : ∀ (x : (↑s : Type u')), w (↑x : ι) = v (↑x : ι)
⊢ Eq (α := (↑s : Type u') → M) (fun (x : (↑s : Type u')) ↦ w (↑x : ι)) fun (x : (↑s : Type u')) ↦ v (↑x : ι)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → M
h : EqOn v w s
x : (↑s : Type u')
⊢ w (↑x : ι) = v (↑x : ι)

Tactic:
h.symm x.2

Premises used: Set.EqOn.symm, Subtype.property
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → M
h : EqOn v w s
x : (↑s : Type u')
⊢ w (↑x : ι) = v (↑x : ι)

Tactic:
exact h.symm x.2

Premises used: Set.EqOn.symm, Subtype.property
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → M
hli : LinearIndepOn R v s
h : EqOn v w s
⊢ LinearIndepOn R w s

Tactic:
(linearIndepOn_congr h).1 hli

Premises used: linearIndepOn_congr, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
rw :
  ∀
    (hv :
      ∀ (s : Finset ι) (f g : ι → R),
        (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i)
    (w : ι → G) (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) →
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • (w • v) i) (∑ i ∈ s, g i • (w • v) i) → ∀ (i : ι), f i = g i
⊢ LinearIndependent R (w • v)

Tactic:
rw [linearIndependent_iff''ₛ] at hv ⊢

Premises used: linearIndependent_iff''ₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ g₁ i = g₂ i

Tactic:
(Group.isUnit (w i)).smul_left_cancel.mp ?_

Premises used: Group.isUnit, IsUnit.smul_left_cancel, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
refine : w i • g₁ i = w i • g₂ i
⊢ g₁ i = g₂ i

Tactic:
refine (Group.isUnit (w i)).smul_left_cancel.mp ?_

Premises used: Group.isUnit, IsUnit.smul_left_cancel, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ w i • g₁ i = w i • g₂ i

Tactic:
hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i

Premises used: HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
refine_1 : ∀ (i : ι) (hi : i ∉ s), Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) ((fun (i : ι) ↦ w i • g₂ i) i)
refine_2 :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ w i • g₂ i) i) (v i))
⊢ w i • g₁ i = w i • g₂ i

Tactic:
refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i

Premises used: HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i_1 i : ι
hi : i ∉ s
refine_1 refine_1₁ : w i • g₁ i = w i • g₂ i
⊢ Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) ((fun (i : ι) ↦ w i • g₂ i) i)

Tactic:
simp_rw [hgs i hi]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ w i • g₂ i) i) (v i))

Tactic:
simpa only [smul_assoc, smul_comm] using hsum

Premises used: smul_assoc, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩

Premises used: Iff.intro, LinearIndependent.group_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
refine : ∀ (h : LinearIndependent R (w • v)), LinearIndependent R v
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ LinearIndependent R (HSMul.hSMul (α := ι → G) (fun (i : ι) ↦ (w i)⁻¹) (w • v))

Tactic:
h.group_smul (fun i ↦ (w i)⁻¹)

Premises used: Inv.inv, LinearIndependent.group_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
h₁ : v = HSMul.hSMul (α := ι → G) (fun (i : ι) ↦ (w i)⁻¹) (w • v)
⊢ LinearIndependent R v

Tactic:
convert! h.group_smul (fun i ↦ (w i)⁻¹)

Premises used: Inv.inv, LinearIndependent.group_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ v = HSMul.hSMul (α := ι → G) (fun (i : ι) ↦ (w i)⁻¹) (w • v)

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hv : LinearIndependent R v
w : ι → Rˣ
rw :
  ∀
    (hv :
      ∀ (s : Finset ι) (f g : ι → R),
        (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i)
    (w : ι → Rˣ) (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) →
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • (w • v) i) (∑ i ∈ s, g i • (w • v) i) → ∀ (i : ι), f i = g i
⊢ LinearIndependent R (w • v)

Tactic:
rw [linearIndependent_iff''ₛ] at hv ⊢

Premises used: linearIndependent_iff''ₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
rw : g₁ i * (↑(w i) : R) = g₂ i * (↑(w i) : R)
⊢ g₁ i = g₂ i

Tactic:
rw [← (w i).mul_left_inj]

Premises used: Units.mul_left_inj
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ g₁ i * (↑(w i) : R) = g₂ i * (↑(w i) : R)

Tactic:
hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i

Premises used: Units.val, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
refine_1 :
  ∀ (i : ι) (hi : i ∉ s),
    Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i)
refine_2 :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i) (v i))
⊢ g₁ i * (↑(w i) : R) = g₂ i * (↑(w i) : R)

Tactic:
refine hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i

Premises used: Units.val, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i_1 i : ι
hi : i ∉ s
refine_1 refine_1₁ : g₁ i • (↑(w i) : R) = g₂ i • (↑(w i) : R)
⊢ Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i)

Tactic:
simp_rw [hgs i hi]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i) (v i))

Tactic:
simpa only [smul_eq_mul, mul_smul, Pi.smul_apply'] using hsum

Premises used: Pi.smul_apply', smul_eq_mul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → Rˣ
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩

Premises used: Iff.intro, LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → Rˣ
refine : ∀ (h : LinearIndependent R (w • v)), LinearIndependent R v
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ LinearIndependent R (HSMul.hSMul (α := ι → Rˣ) (fun (i : ι) ↦ (w i)⁻¹) (w • v))

Tactic:
h.units_smul (fun i ↦ (w i)⁻¹)

Premises used: Inv.inv, LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → Rˣ
h : LinearIndependent R (w • v)
h₁ : v = HSMul.hSMul (α := ι → Rˣ) (fun (i : ι) ↦ (w i)⁻¹) (w • v)
⊢ LinearIndependent R v

Tactic:
convert! h.units_smul (fun i ↦ (w i)⁻¹)

Premises used: Inv.inv, LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ v = HSMul.hSMul (α := ι → Rˣ) (fun (i : ι) ↦ (w i)⁻¹) (w • v)

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
hs : LinearIndependent R v
⊢ LinearIndependent.{u', u_2, u_4} R (M := ↥(span R (range v))) fun (i : ι) ↦
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯

Tactic:
LinearIndependent.of_comp (span R (range v)).subtype hs

Premises used: LinearIndependent.of_comp, Submodule.span, Submodule.subtype, Set.range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
li : LinearIndependent.{u_4, u_2, u_4} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type u_4)
x : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)
⊢ x.1 ∈ s

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
li : LinearIndependent.{u_4, u_2, u_4} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type u_4)
a₁ : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)
⊢ ∀ ⦃a₂ : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)⦄,
    Eq.{u_4 + 1} (α := { x : M // x ∈ s })
        ((fun (x : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)) ↦
            (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x.1 ⋯ : { x : M // x ∈ s }))
          a₁)
        ((fun (x : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)) ↦
            (Subtype.mk (p := fun (x : M) ↦ x ∈ s) x.1 ⋯ : { x : M // x ∈ s }))
          a₂) →
      a₁ = a₂

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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 ι
H : ∀ t ⊆ s, t.Finite → LinearIndepOn R v t
⊢ LinearIndepOn R v s

Tactic:
linearIndepOn_iffₛ.2 fun f hf g hg eq ↦
    linearIndepOn_iffₛ.1 (H _ (union_subset hf hg) <| (Finset.finite_toSet _).union <|
      Finset.finite_toSet _) f Set.subset_union_left g Set.subset_union_right eq

Premises used: Iff.mpr, Set.Finite.union, linearIndepOn_iffₛ, Set.subset_union_right, Finsupp.support, Set.union_subset, Set.subset_union_left, SetLike.coe, Iff.mp, Finset.finite_toSet, Union.union
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ Eq.{u_6 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i c) : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single j d) : M)

Tactic:
simpa [Finsupp.linearCombination_apply] using h

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)

Tactic:
have h_single_eq : Finsupp.single i c = Finsupp.single j d :=
    li <| by simpa [Finsupp.linearCombination_apply] using h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
inl : ∀ (H : i = j), c = d → i = j
inr : ∀ (hc : c = 0), d = 0 → i = j
⊢ i = j

Tactic:
rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)

Premises used: Finsupp.single_eq_single_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
H : i = j
right : c = d
⊢ i = j

Tactic:
H
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
H : i = j
right : c = d
⊢ i = j

Tactic:
exact H
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc_1 : c ≠ 0
h : c • v i = d • v j
h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
hc : c = 0
right : d = 0
⊢ i = j

Tactic:
contradiction