Theorem: Fintype.not_linearIndependent_restrict_iff (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, c i ≠ 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
simp only [Finset.coe_sort_coe, not_linearIndependent_iff, Finset.univ_eq_attach, restrict_apply,
  ne_eq, Subtype.exists, Finset.mem_coe]
State after:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ (∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ (∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
refine ⟨fun ⟨g, hg0, b, hbs, hgb⟩ ↦ ?_, fun ⟨c,hc0,⟨b,hbs, hb0⟩,hc'⟩ ↦ ?_⟩
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0

case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
Tactic:
refine ⟨c ∘ Subtype.val, ?_, b, hbs, by simpa⟩
State after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, (c ∘ Subtype.val) x • f ↑x = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, (c ∘ Subtype.val) x • f ↑x = 0
Tactic:
simp only [comp_apply]
State after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, c ↑x • f ↑x = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, c ↑x • f ↑x = 0
Tactic:
rwa [s.sum_attach (fun x ↦ c x • f x),
  Finset.sum_subset (s.subset_univ) (fun x _ hx ↦ by simp [hc' x hx])]
State after:
no goals

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
set c := Function.extend Subtype.val g 0 with hc
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
have hc0 : ∀ x ∉ s, c x = 0 :=
  fun x hxs ↦ by rw [hc, extend_apply' _ _ _ (by simpa), Pi.zero_apply]
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
have hc1 : ∀ x : s, c x = g x :=
  fun ⟨x,hx⟩ ↦ by rw [hc, Subtype.val_injective.extend_apply]
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
refine ⟨c, ?_, ⟨b, hbs, by rwa [← hc1] at hgb⟩, hc0⟩
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∑ i : ι, c i • f i = 0

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
x : ι
hxs : x ∉ s
⊢ c x = 0
Tactic:
rw [hc, extend_apply' _ _ _ (by simpa), Pi.zero_apply]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
x : ι
hxs : x ∉ s
⊢ ¬∃ a, ↑a = x
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝¹ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
x✝ : { x // x ∈ s }
x : ι
hx : x ∈ s
⊢ c ↑⟨x, hx⟩ = g ⟨x, hx⟩
Tactic:
rw [hc, Subtype.val_injective.extend_apply]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ¬c b = 0
Tactic:
rwa [← hc1] at hgb
State after:
no goals

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∑ i : ι, c i • f i = 0
Tactic:
rw [← Finset.sum_subset s.subset_univ (fun x _ hx ↦ by simp [hc0 x hx]), ← Finset.sum_attach]
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∑ x ∈ s.attach, c ↑x • f ↑x = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∑ x ∈ s.attach, c ↑x • f ↑x = 0
Tactic:
simp_rw [hc1]
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∑ x ∈ s.attach, g x • f ↑x = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
⊢ ∑ x ∈ s.attach, g x • f ↑x = 0
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝¹ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
c : ι → R := extend Subtype.val g 0
hc : c = extend Subtype.val g 0
hc0 : ∀ x ∉ s, c x = 0
hc1 : ∀ (x : { x // x ∈ s }), c ↑x = g x
x : ι
x✝ : x ∈ Finset.univ
hx : x ∉ s
⊢ c x • f x = 0
Tactic:
simp [hc0 x hx]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ¬(c ∘ Subtype.val) ⟨b, hbs⟩ = 0
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝¹ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
x : ι
x✝ : x ∈ Finset.univ
hx : x ∉ s
⊢ c x • f x = 0
Tactic:
simp [hc' x hx]
State after:
no goals