ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
this : ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
have : ∀ x, f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b) := by
  rw [Ideal.range_finsuppTotal, hb]
  exact fun x => hI (LinearMap.mem_range_self f x)
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
this : ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
choose bM' hbM' using this
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
let A : Matrix ι ι R := fun i j => bM' (b j) i
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
this : Represents b A f
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
have : A.Represents b f := by
  rw [Matrix.represents_iff']
  dsimp
  intro j
  specialize hbM' (b j)
  rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'
no goals
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
this : Represents b A f
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
exact
  ⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this,
    fun i j => (bM' (b j) i).prop⟩
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ I • ⊤
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
rw [Ideal.range_finsuppTotal, hb]
no goals
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ I • ⊤
exact fun x => hI (LinearMap.mem_range_self f x)
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ Represents b A f
rw [Matrix.represents_iff']
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
dsimp
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
intro j
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
hbM' : ↑(Ideal.finsuppTotal ι M I b) (bM' (b j)) = ↑f (b j)
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
specialize hbM' (b j)
no goals
ι : Type u_3
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
hbM' : ↑(Ideal.finsuppTotal ι M I b) (bM' (b j)) = ↑f (b j)
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'