-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.exists_nontrivial_relation_of_finrank_lt_card {t : Finset M}
    (h : finrank R M < t.card) : ∃ f : M → R, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
case intro.intro.intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ ∑ i : ↑↑t, extend Subtype.val g 0 ↑i • ↑i = 0

Tactic:
convert sum

Result:
case h.e'_2.a.h.e'_5
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
x✝ : ↑↑t
a✝ : x✝ ∈ Finset.univ
⊢ extend Subtype.val g 0 ↑x✝ = g x✝

Proof state:
case intro.intro.intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ ∑ e ∈ t, extend Subtype.val g 0 e • e = 0

Tactic:
rw [← Finset.sum_finset_coe]

Result:
case intro.intro.intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ ∑ i : ↑↑t, extend Subtype.val g 0 ↑i • ↑i = 0

Proof state:
case h.e'_2.a.h.e'_5
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
x✝ : ↑↑t
a✝ : x✝ ∈ Finset.univ
⊢ extend Subtype.val g 0 ↑x✝ = g x✝

Tactic:
apply Subtype.val_injective.extend_apply

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
obtain ⟨g, sum, z, nonzero⟩ := Fintype.not_linearIndependent_iff.mp
  (mt LinearIndependent.finset_card_le_finrank h.not_le)

Result:
case intro.intro.intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
case intro.intro.intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩

Result:
case intro.intro.intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ ∑ e ∈ t, extend Subtype.val g 0 e • e = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : { x // x ∈ t } → R
sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0
z : { x // x ∈ t }
nonzero : g z ≠ 0
⊢ extend Subtype.val g 0 ↑z ≠ 0

Tactic:
rwa [Subtype.val_injective.extend_apply]

Result:
no goals