case h
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ↑(↑b.repr (∑ i : ι, c i • ↑b i)) j = c j
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
⊢ ↑(↑b.repr (∑ i : ι, c i • ↑b i)) = c
ext j
case h
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ∑ x : ι, ↑(Finsupp.single x (c x)) j = c j
case h
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ↑(↑b.repr (∑ i : ι, c i • ↑b i)) j = c j
simp only [map_sum, LinearEquiv.map_smul, repr_self, Finsupp.smul_single, smul_eq_mul, mul_one,
  Finset.sum_apply']
case h.h₀
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ∀ (b : ι), b ∈ Finset.univ → b ≠ j → ↑(Finsupp.single b (c b)) j = 0

case h.h₁
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ¬j ∈ Finset.univ → ↑(Finsupp.single j (c j)) j = 0
case h
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ∑ x : ι, ↑(Finsupp.single x (c x)) j = c j
rw [Finset.sum_eq_single j, Finsupp.single_eq_same]
case h.h₀
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j i : ι
hi : i ≠ j
⊢ ↑(Finsupp.single i (c i)) j = 0
case h.h₀
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ∀ (b : ι), b ∈ Finset.univ → b ≠ j → ↑(Finsupp.single b (c b)) j = 0
rintro i - hi
no goals
case h.h₀
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j i : ι
hi : i ≠ j
⊢ ↑(Finsupp.single i (c i)) j = 0
exact Finsupp.single_eq_of_ne hi
case h.h₁
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
a✝ : ¬j ∈ Finset.univ
⊢ ↑(Finsupp.single j (c j)) j = 0
case h.h₁
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
⊢ ¬j ∈ Finset.univ → ↑(Finsupp.single j (c j)) j = 0
intros
case h.h₁
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
a✝ : ¬j ∈ Finset.univ
this : j ∈ Finset.univ
⊢ ↑(Finsupp.single j (c j)) j = 0
case h.h₁
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
a✝ : ¬j ∈ Finset.univ
⊢ ↑(Finsupp.single j (c j)) j = 0
have := Finset.mem_univ j
no goals
case h.h₁
ι : Type u_1
ι' : Type ?u.673229
R : Type u_2
R₂ : Type ?u.673235
K : Type ?u.673238
M : Type u_3
M' : Type ?u.673244
M'' : Type ?u.673247
V : Type u
V' : Type ?u.673252
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
j : ι
a✝ : ¬j ∈ Finset.univ
this : j ∈ Finset.univ
⊢ ↑(Finsupp.single j (c j)) j = 0
contradiction