-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
lemma coweightHom_injective (P : RootPairing ι R M N) : Injective (coweightHom P)

Proof state:
case indexEquiv.H
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y)
⊢ y = g.indexEquiv x

Tactic:
rw [coroot_coweightMap_apply, coroot_coweightMap_apply, Embedding.apply_eq_iff_eq, hy] at this

Result:
case indexEquiv.H
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : f.indexEquiv.symm (f.indexEquiv x) = g.indexEquiv.symm (f.indexEquiv x)
⊢ y = g.indexEquiv x

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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : f.weightMap.dualMap ∘ₗ ↑P.toDualRight = g.weightMap.dualMap ∘ₗ ↑P.toDualRight
⊢ f.weightMap = g.weightMap

Tactic:
haveI : Module.IsReflexive R M := PerfectPairing.reflexive_left P.toPerfectPairing

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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : f.weightMap.dualMap ∘ₗ ↑P.toDualRight = g.weightMap.dualMap ∘ₗ ↑P.toDualRight
this : Module.IsReflexive R M
⊢ f.weightMap = g.weightMap

Proof state:
case weightMap.h
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
⊢ f.weightMap x = g.weightMap x

Tactic:
have h := congrArg (LinearMap.comp (M₃ := Module.Dual R M)
    (σ₂₃ := RingHom.id R) (P.toDualRight)) hfg

Result:
case weightMap.h
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : ↑P.toDualRight ∘ₗ f.coweightMap = ↑P.toDualRight ∘ₗ g.coweightMap
⊢ f.weightMap x = g.weightMap x

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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
⊢ f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y)

Tactic:
exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)

Result:
no goals

Proof state:
case indexEquiv.H
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
rw [MulOpposite.op_inj] at hfg

Result:
case indexEquiv.H
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Proof state:
case indexEquiv.H
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : x = g.indexEquiv.symm (f.indexEquiv x)
⊢ y = g.indexEquiv x

Tactic:
rw [this, Equiv.apply_symm_apply]

Result:
no goals

Proof state:
case indexEquiv.H
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
dsimp [coweightHom] at hfg

Result:
case indexEquiv.H
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Proof state:
case weightMap.h
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : f.weightMap.dualMap ∘ₗ ↑P.toDualRight = g.weightMap.dualMap ∘ₗ ↑P.toDualRight
⊢ f.weightMap x = g.weightMap x

Tactic:
have : f.weightMap = g.weightMap := by
  haveI : Module.IsReflexive R M := PerfectPairing.reflexive_left P.toPerfectPairing
  refine (Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
    ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))

Result:
case weightMap.h
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h : f.weightMap.dualMap ∘ₗ ↑P.toDualRight = g.weightMap.dualMap ∘ₗ ↑P.toDualRight
this : f.weightMap = g.weightMap
⊢ f.weightMap x = g.weightMap x

Proof state:
case indexEquiv.H
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
set y := f.indexEquiv x with hy

Result:
case indexEquiv.H
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
⊢ y = g.indexEquiv x

Proof state:
case coweightMap.h
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : N
⊢ f.coweightMap x = g.coweightMap x

Tactic:
dsimp [coweightHom] at hfg

Result:
case coweightMap.h
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : N
⊢ f.coweightMap x = g.coweightMap x