-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_linearDependent {K : Type*} [Ring K] {M : Type*} [AddCommGroup M] [Module K M]
    {N : Type*} [AddCommGroup N] [Module K N] [NoZeroSMulDivisors K N] (f : M [⋀^ι]→ₗ[K] N)
    (v : ι → M) (h : ¬LinearIndependent K v) : f v = 0

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
⊢ f v = 0

Tactic:
letI := Classical.decEq ι

Result:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ f v = 0

Proof state:
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : g i = 0 ∨ f v = 0
⊢ f v = 0

Tactic:
exact Or.resolve_left this hz

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.h.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ f (update v i (g j • v j)) = 0

Tactic:
rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.h
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
⊢ f (update v i (g j • v j)) = 0

Tactic:
obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj

Result:
case intro.intro.intro.intro.intro.h.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ f (update v i (g j • v j)) = 0

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ f (update v i (g i • v i)) = 0

Tactic:
rw [h, f.map_update_neg, f.map_update_sum, neg_eq_zero]

Result:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ ∑ a ∈ s.erase i, f (update v i (g a • v a)) = 0

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
h : (∑ x ∈ s, if i = x then g x • v x else g x • v x) = 0
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ f (update v i (g i • v i)) = 0

Tactic:
rw [Finset.sum_ite, Finset.filter_eq, Finset.filter_ne, if_pos hi, Finset.sum_singleton,
  add_eq_zero_iff_eq_neg] at h

Result:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ f (update v i (g i • v i)) = 0

Proof state:
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : f (update v i (g i • v i)) = 0
⊢ f v = 0

Tactic:
rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this

Result:
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : g i = 0 ∨ f v = 0
⊢ f v = 0

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ ∑ a ∈ s.erase i, f (update v i (g a • v a)) = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case intro.intro.intro.intro.intro.h
ι : Type u_7
K : Type u_12
inst✝⁵ : Ring K
M : Type u_13
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
N : Type u_14
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : NoZeroSMulDivisors K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ ∀ x ∈ s.erase i, f (update v i (g x • v x)) = 0