internlm/Lean-Github huggingface dataset:
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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])]
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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
Proof 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
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof 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
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof 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
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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⟩
Proof 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
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof 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
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof 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
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof 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]
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff'
Proof 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 : Set ι
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:
obtain ⟨s,rfl⟩ := s.toFinite.exists_finset_coe
Proof state after:
case intro
α : 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
f : ι → M
s : Finset ι
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ ↑s, c i ≠ 0) ∧ ∀ i ∉ ↑s, c i = 0
Theorem: Fintype.not_linearIndependent_restrict_iff'
Proof state before:
case intro
α : 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
f : ι → M
s : Finset ι
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ ↑s, c i ≠ 0) ∧ ∀ i ∉ ↑s, c i = 0
Tactic:
exact Fintype.not_linearIndependent_restrict_iff
Proof state after:
no goals
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ LinearIndependent (ι := ↑s) R (s.restrict f) ↔ ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
Tactic:
rw [linearIndependent_iff]
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ (∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0) ↔
    ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ (∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0) ↔
    ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
Tactic:
refine ⟨fun h l hl0 hls ↦ ?_, fun h l hl0 ↦ ?_⟩
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : (Finsupp.total ι M R f) l = 0
hls : ↑l.support ⊆ s
⊢ l = 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
⊢ l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
⊢ l = 0
Tactic:
specialize h l.extendDomain
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total ι M R f) l.extendDomain = 0 → ↑l.extendDomain.support ⊆ s → l.extendDomain = 0
⊢ l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total ι M R f) l.extendDomain = 0 → ↑l.extendDomain.support ⊆ s → l.extendDomain = 0
⊢ l = 0
Tactic:
rw [Finsupp.extendDomain_eq_embDomain_subtype, Finsupp.total_embDomain] at h
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h :
  (Finsupp.total { x // x ∈ s } M R (f ∘ ⇑(Embedding.subtype fun x => x ∈ s))) l = 0 →
    ↑(Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l).support ⊆ s →
      Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l = 0
⊢ l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h :
  (Finsupp.total { x // x ∈ s } M R (f ∘ ⇑(Embedding.subtype fun x => x ∈ s))) l = 0 →
    ↑(Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l).support ⊆ s →
      Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l = 0
⊢ l = 0
Tactic:
simp only [Embedding.coe_subtype, Finsupp.support_embDomain, Finset.coe_map, image_subset_iff,
  Subtype.coe_preimage_self, subset_univ, Finsupp.embDomain_eq_zero, forall_true_left] at h
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total { x // x ∈ s } M R (f ∘ Subtype.val)) l = 0 → l = 0
⊢ l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total { x // x ∈ s } M R (f ∘ Subtype.val)) l = 0 → l = 0
⊢ l = 0
Tactic:
exact h hl0
Proof state after:
no goals
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : (Finsupp.total ι M R f) l = 0
hls : ↑l.support ⊆ s
⊢ l = 0
Tactic:
rw [Finsupp.total_apply, Finsupp.sum_of_support_subset _ Subset.rfl _ (by simp)] at hl0
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
⊢ l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
⊢ l = 0
Tactic:
specialize h (Finsupp.comapDomain ((↑) : s → ι) l Subtype.val_injective.injOn)
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h :
  (Finsupp.total (↑s) M R (s.restrict f)) (Finsupp.comapDomain Subtype.val l ⋯) = 0 →
    Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0
Theorem: linearIndependent_restrict_iff
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h :
  (Finsupp.total (↑s) M R (s.restrict f)) (Finsupp.comapDomain Subtype.val l ⋯) = 0 →
    Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0
Tactic:
simp only [Finsupp.total_comapDomain, restrict_apply] at h
Proof 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support.preimage Subtype.val ⋯, l ↑x • f ↑x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0