ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → { x // x ∈ N }), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ ∀ (x : M), x ∈ N → x = 0
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → { x // x ∈ N }), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ N = ⊥
rw [Submodule.eq_bot_iff]
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → { x // x ∈ N }), LinearIndependent R (Subtype.val ∘ v) → m = 0
x : M
hx : x ∈ N
⊢ x = 0
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → { x // x ∈ N }), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ ∀ (x : M), x ∈ N → x = 0
intro x hx
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ Exists fun {m} => ∃ v, LinearIndependent R (Subtype.val ∘ v) ∧ m ≠ 0
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → { x // x ∈ N }), LinearIndependent R (Subtype.val ∘ v) → m = 0
x : M
hx : x ∈ N
⊢ x = 0
contrapose! rank_eq with x_ne
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ LinearIndependent R (Subtype.val ∘ fun x_1 => { val := x, property := hx })
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ Exists fun {m} => ∃ v, LinearIndependent R (Subtype.val ∘ v) ∧ m ≠ 0
refine' ⟨1, fun _ => ⟨x, hx⟩, _, one_ne_zero⟩
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∀ (g : Fin 1 → R),
    ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) i = 0 → ∀ (i : Fin 1), g i = 0
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ LinearIndependent R (Subtype.val ∘ fun x_1 => { val := x, property := hx })
rw [Fintype.linearIndependent_iff]
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
sum_eq : ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) i = 0
i : Fin 1
⊢ g i = 0
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∀ (g : Fin 1 → R),
    ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) i = 0 → ∀ (i : Fin 1), g i = 0
rintro g sum_eq i
case mk
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
sum_eq : ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) i = 0
val✝ : ℕ
hi : val✝ < 1
⊢ g { val := val✝, isLt := hi } = 0
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
sum_eq : ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) i = 0
i : Fin 1
⊢ g i = 0
cases' i with _ hi
case mk
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
val✝ : ℕ
hi : val✝ < 1
sum_eq : g 0 • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) 0 = 0
⊢ g { val := val✝, isLt := hi } = 0
case mk
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
sum_eq : ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) i = 0
val✝ : ℕ
hi : val✝ < 1
⊢ g { val := val✝, isLt := hi } = 0
simp only [Function.const_apply, Fin.default_eq_zero, Submodule.coe_mk, Finset.univ_unique,
  Function.comp_const, Finset.sum_singleton] at sum_eq
no goals
case mk
ι : Type u_2
ι' : Type ?u.602198
R : Type u_1
R₂ : Type ?u.602204
K : Type ?u.602207
M : Type u_3
M' : Type ?u.602213
M'' : Type ?u.602216
V : Type u
V' : Type ?u.602221
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
g : Fin 1 → R
val✝ : ℕ
hi : val✝ < 1
sum_eq : g 0 • (Subtype.val ∘ fun x_1 => { val := x, property := hx }) 0 = 0
⊢ g { val := val✝, isLt := hi } = 0
convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne