awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R _root_.id s
hf_inj : Disjoint (span R s) f.ker
⊢ LinearIndepOn.{u_5, u_2, u_5} (ι := M') R _root_.id ((⇑f : (a : M) → M') '' s)

Tactic:
hs.id_imageₛ <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj

Premises used: le_rfl, LinearIndepOn.id_imageₛ, LinearMap.injOn_of_disjoint_ker
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
apply :
  ∀ (s : Finset (G →* L)) (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent L (M := G → L) fun (f : G →* L) ↦ (⇑f : (a : G) → L)

Tactic:
apply linearIndependent_iff'.2

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
⊢ ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ ∅, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 →
      ∀ (i : G →* L), Membership.mem (γ := Finset (G →* L)) ∅ i → g i = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
h :
  ∀ (x : G),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x =
      HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x
⊢ HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x : G
h :
  HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x -
      HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x =
    0
⊢ HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x : G
apply :
  Eq (α := G → L)
    (∑ i ∈ s,
      HSMul.hSMul (α := L) (β := G → L)
        ((fun (j : G →* L) ↦
            HMul.hMul (β := L) (g j) ((j : (a : G) → L) x : L) - HMul.hMul (β := L) (g j) ((a : (a : G) → L) x : L))
          i)
        (⇑i : (a : G) → L))
    0
⊢ HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x -
      HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x =
    0

Tactic:
apply ih (fun j => g j * j x - g j * a x) _ i his

Premises used: HMul.hMul, HSub.hSub, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x : G
h :
  ∀ (y : G),
    Eq.{u_7 + 1} (α := L)
      ((∑ i ∈ s,
          HSMul.hSMul (α := L) (β := G → L)
            ((fun (j : G →* L) ↦
                HMul.hMul (β := L) (g j) ((j : (a : G) → L) x : L) - HMul.hMul (β := L) (g j) ((a : (a : G) → L) x : L))
              i)
            (⇑i : (a : G) → L))
        y)
      (0 y)
⊢ Eq (α := G → L)
    (∑ i ∈ s,
      HSMul.hSMul (α := L) (β := G → L)
        ((fun (j : G →* L) ↦
            HMul.hMul (β := L) (g j) ((j : (a : G) → L) x : L) - HMul.hMul (β := L) (g j) ((a : (a : G) → L) x : L))
          i)
        (⇑i : (a : G) → L))
    0

Tactic:
ext y
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ s,
        HSMul.hSMul (β := (a : G) → L)
          (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L) - HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L))
          (⇑i : (a : G) → L))
      y =
    HSub.hSub (α := L)
      (∑ i ∈ s, HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))
      (∑ i ∈ s, HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))

Tactic:
simp [sub_mul]

Premises used: sub_mul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
⊢ HSub.hSub (α := L)
      (∑ i ∈ s, HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))
      (∑ i ∈ s, HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L)) =
    HSub.hSub (α := L)
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))

Tactic:
simp [Finset.sum_insert has]

Premises used: Finset.sum_insert
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
refine_1 :
  ∀ (i : G →* L),
    HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
      g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)
refine_2 :
  ∀ (i : G →* L),
    HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
      HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
⊢ HSub.hSub (α := L)
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L)) =
    HSub.hSub (α := L)
      (∑ i ∈ insert a s, g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L)))

Tactic:
congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_

Premises used: Insert.insert
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i_1 : G →* L
his : i_1 ∈ s
x y : G
i : G →* L
refine_1 refine_1₁ :
  g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L) =
    g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)
⊢ HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i_1 : G →* L
his : i_1 ∈ s
x y : G
i : G →* L
refine_2 :
  g i * HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L) ((i : (a : G) → L) y : L) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
refine_2₁ refine_2₂ :
  HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L)) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
⊢ HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))

Tactic:
rw [mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
⊢ HSub.hSub (α := L)
      (∑ i ∈ insert a s, g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))) =
    (∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) (x * y) -
      HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L)
        ((∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) y : L)

Tactic:
simp [Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
rw : 0 (x * y) - HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L) (0 y : L) = 0
⊢ (∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) (x * y) -
      HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L)
        ((∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) y : L) =
    0

Tactic:
rw [hg]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L) (0 y : L) = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
⊢ ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)

Tactic:
have h1 (i) (his : i ∈ s) : (g i • i : G → L) = g i • a := by
    ext x
    rw [← sub_eq_zero]
    apply ih (fun j => g j * j x - g j * a x) _ i his
    ext y
    -- After that, it's just a chase scene.
    calc
      (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
by_contra! : ∀ (hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)), False
⊢ ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)

Tactic:
by_contra! hia
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ i = a

Tactic:
MonoidHom.ext hia

Premises used: MonoidHom.ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ i ∉ s

Tactic:
obtain rfl : i = a := MonoidHom.ext hia

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
has₁ : i ∉ s
⊢ Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0

Tactic:
obtain rfl : i = a := MonoidHom.ext hia

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
has₁ : i ∉ s
hg₁ : Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
⊢ ∀ (i_1 : G →* L) (his : i_1 ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i_1 : (a : G) → L) =
      HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i : (a : G) → L)

Tactic:
obtain rfl : i = a := MonoidHom.ext hia

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
has₁ : i ∉ s
hg₁ : Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1₁ :
  ∀ (i_1 : G →* L) (his : i_1 ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i_1 : (a : G) → L) =
      HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i : (a : G) → L)
⊢ ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((i : (a : G) → L) y : L)

Tactic:
obtain rfl : i = a := MonoidHom.ext hia

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
s : Finset (G →* L)
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
i : G →* L
his : i ∈ s
has : i ∉ s
hg : Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i_1 : G →* L) (his : i_1 ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i_1 : (a : G) → L) =
      HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i : (a : G) → L)
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((i : (a : G) → L) y : L)
⊢ False

Tactic:
contradiction