ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
⊢ x = y
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Injective ↑(fromEnd R b)
intro x y e
case h
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ ↑x m = ↑y m
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
⊢ x = y
ext m
case h.intro
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : ι → R
⊢ ↑x (↑(↑(Fintype.total R R) b) m) = ↑y (↑(↑(Fintype.total R R) b) m)
case h
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ ↑x m = ↑y m
obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.total R R b) := by
  rw [(Fintype.range_total R b).trans hb]
  exact Submodule.mem_top
no goals
case h.intro
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : ι → R
⊢ ↑x (↑(↑(Fintype.total R R) b) m) = ↑y (↑(↑(Fintype.total R R) b) m)
exact (LinearMap.congr_fun e m : _)
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ ⊤
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ LinearMap.range (↑(Fintype.total R R) b)
rw [(Fintype.range_total R b).trans hb]
no goals
ι : Type u_3
inst✝³ : Fintype ι
M : Type u_1
inst✝² : AddCommGroup M
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ ⊤
exact Submodule.mem_top