-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem PiToModule.fromEnd_injective (hb : Submodule.span R (Set.range b) = ⊤) :
    Function.Injective (PiToModule.fromEnd R b)

Proof state:
case h
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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

Tactic:
obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R R b) := by
  rw [(Fintype.range_linearCombination R b).trans hb]
  exact Submodule.mem_top

Result:
case h.intro
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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.linearCombination R R) b) m) = y (((Fintype.linearCombination R R) b) m)

Proof state:
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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.linearCombination R R) b)

Tactic:
rw [(Fintype.range_linearCombination R b).trans hb]

Result:
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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 ∈ ⊤

Proof state:
case h.intro
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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.linearCombination R R) b) m) = y (((Fintype.linearCombination R R) b) m)

Tactic:
exact (LinearMap.congr_fun e m :)

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Injective ⇑(fromEnd R b)

Tactic:
intro x y e

Result:
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : (fromEnd R b) x = (fromEnd R b) y
⊢ x = y

Proof state:
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : (fromEnd R b) x = (fromEnd R b) y
⊢ x = y

Tactic:
ext m

Result:
case h
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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

Proof state:
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
b : ι → M
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 ∈ ⊤

Tactic:
exact Submodule.mem_top

Result:
no goals