ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
⊢ w ≤ Set.range ↑b
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
⊢ Set.range ↑b = w
apply le_antisymm h
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
⊢ x ∈ Set.range ↑b
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
⊢ w ≤ Set.range ↑b
intro x p
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
⊢ x ∈ Set.range ↑b
by_contra q
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : ↑(Finsupp.total ι M R ↑b) (↑b.repr x) = x
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
⊢ False
have e := b.total_repr x
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : ↑(Finsupp.total ι M R ↑b) (↑b.repr x) = x
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : ↑(Finsupp.total ι M R ↑b) (↑b.repr x) = x
⊢ False
let u : ι ↪ w :=
  ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
    b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : (Finsupp.sum (↑b.repr x) fun i a => a • ↑b i) = x
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : ↑(Finsupp.total ι M R ↑b) (↑b.repr x) = x
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
⊢ False
simp_rw [Finsupp.total_apply] at e
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : (Finsupp.sum (↑b.repr x) fun i a => a • ↑(↑u i)) = ↑{ val := x, property := p }
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : (Finsupp.sum (↑b.repr x) fun i a => a • ↑b i) = x
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
⊢ False
replace e : ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) =
    ((⟨x, p⟩ : w) : M) := e
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : (Finsupp.sum (↑b.repr x) fun i a => a • ↑(↑u i)) = ↑{ val := x, property := p }
⊢ False
rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)), ← Finsupp.total_apply] at e
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
⊢ ¬{ val := x, property := p } ∈ (Finsupp.embDomain u (↑b.repr x)).support
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
⊢ False
refine' hi.total_ne_of_not_mem_support _ _ e
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
⊢ ¬∃ a,
      a ∈ (↑b.repr x).support ∧
        ↑{ toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
                inj' :=
                  (_ :
                    ∀ (i i' : ι),
                      (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
                          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
                        i = i') }
            a =
          { val := x, property := p }
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
⊢ ¬{ val := x, property := p } ∈ (Finsupp.embDomain u (↑b.repr x)).support
simp only [Finset.mem_map, Finsupp.support_embDomain]
case intro.intro
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
j : ι
W :
  ↑{ toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
          inj' :=
            (_ :
              ∀ (i i' : ι),
                (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
                    (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
                  i = i') }
      j =
    { val := x, property := p }
⊢ False
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
⊢ ¬∃ a,
      a ∈ (↑b.repr x).support ∧
        ↑{ toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
                inj' :=
                  (_ :
                    ∀ (i i' : ι),
                      (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
                          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
                        i = i') }
            a =
          { val := x, property := p }
rintro ⟨j, -, W⟩
case intro.intro
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
j : ι
W : ↑b j = x
⊢ False
case intro.intro
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
j : ι
W :
  ↑{ toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
          inj' :=
            (_ :
              ∀ (i i' : ι),
                (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
                    (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
                  i = i') }
      j =
    { val := x, property := p }
⊢ False
simp only [Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
no goals
case intro.intro
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
u : ι ↪ ↑w :=
  { toFun := fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) },
    inj' :=
      (_ :
        ∀ (i i' : ι),
          (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i =
              (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i' →
            i = i') }
e : ↑(Finsupp.total (↑w) M R fun x => ↑x) (Finsupp.embDomain u (↑b.repr x)) = ↑{ val := x, property := p }
j : ι
W : ↑b j = x
⊢ False
apply q ⟨j, W⟩
no goals
ι : Type u_2
ι' : Type ?u.778808
R : Type u_1
R₂ : Type ?u.778814
K : Type ?u.778817
M : Type u_3
M' : Type ?u.778823
M'' : Type ?u.778826
V : Type u
V' : Type ?u.778831
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x✝ y : M
b✝ : Basis ι R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : Set.range ↑b ≤ w
x : M
p : x ∈ w
q : ¬x ∈ Set.range ↑b
e : ↑(Finsupp.total ι M R ↑b) (↑b.repr x) = x
i i' : ι
r : (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i = (fun i => { val := ↑b i, property := (_ : ↑b i ∈ w) }) i'
⊢ ↑b i = ↑b i'
simpa only [Subtype.mk_eq_mk] using r