-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
lemma weightHom_injective (P : RootPairing ι R M N) : Injective (Equiv.weightHom P)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : (Hom.weightHom P) ↑g = (Hom.weightHom P) ↑g'
⊢ ↑g = ↑g'

Tactic:
exact Hom.weightHom_injective P hgg'

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
⊢ g = g'

Tactic:
let h : (weightHom P g).toLinearMap = (weightHom P g').toLinearMap := hgg'

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : ↑((weightHom P) g) = ↑((weightHom P) g') := hgg'
⊢ g = g'

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : ↑((weightHom P) g) = ↑((weightHom P) g') := hgg'
⊢ g = g'

Tactic:
rw [weightHom_toLinearMap, weightHom_toLinearMap] at h

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : (Hom.weightHom P) ↑g = (Hom.weightHom P) ↑g'
⊢ g = g'

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : (Hom.weightHom P) ↑g = (Hom.weightHom P) ↑g'
⊢ g = g'

Tactic:
suffices h' : g.toHom = g'.toHom by
  exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : (Hom.weightHom P) ↑g = (Hom.weightHom P) ↑g'
⊢ ↑g = ↑g'

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ Injective ⇑(weightHom P)

Tactic:
refine Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
⊢ g = g'

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' : (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g = (LinearEquiv.toLinearMap ∘ ⇑(weightHom P)) g'
h : (Hom.weightHom P) ↑g = (Hom.weightHom P) ↑g'
h' : ↑g = ↑g'
⊢ g = g'

Tactic:
exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')

Result:
no goals