-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
lemma coweightHom_injective (P : RootPairing ι R M N) : Injective (Equiv.coweightHom 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ ↑g = ↑g'

Tactic:
apply Hom.coweightHom_injective P

Result:
case a
ι : 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ (Hom.coweightHom P) ↑g = (Hom.coweightHom P) ↑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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
⊢ g = g'

Tactic:
have h : (MulOpposite.unop (coweightHom P g)).toLinearMap =
    (MulOpposite.unop (coweightHom P g')).toLinearMap := by
  simp_all

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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : ↑(MulOpposite.unop ((coweightHom P) g)) = ↑(MulOpposite.unop ((coweightHom 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
h' : ↑g = ↑g'
⊢ g = g'

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

Result:
no goals

Proof state:
case a
ι : 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ (Hom.coweightHom P) ↑g = (Hom.coweightHom P) ↑g'

Tactic:
exact MulOpposite.unop_inj.mp h

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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ g = g'

Tactic:
suffices h' : g.toHom = g'.toHom by
  exact Equiv.ext (congrArg Hom.weightMap h') 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : ↑(MulOpposite.unop ((coweightHom P) g)) = ↑(MulOpposite.unop ((coweightHom P) g'))
⊢ g = g'

Tactic:
rw [coweightHom_toLinearMap, coweightHom_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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
⊢ ↑(MulOpposite.unop ((coweightHom P) g)) = ↑(MulOpposite.unop ((coweightHom P) g'))

Tactic:
simp_all

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
⊢ Injective ⇑(coweightHom P)

Tactic:
refine Injective.of_comp (f := fun a => MulOpposite.op a) 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' : ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a => MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
⊢ g = g'