-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma reflection_inv (P : RootPairing ι R M N) (i : ι) :
    (reflection P i)⁻¹ = (reflection P i)

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
i j : ι
⊢ ((indexHom P) (reflection P i))⁻¹ j = ((indexHom P) (reflection P i)) j

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
ι : 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
i : ι
⊢ (↑(reflection P i)⁻¹).weightMap = (↑(reflection P i)).weightMap

Tactic:
exact LinearMap.ext_iff.mpr (fun x => by simp [← weightEquiv_apply])

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
i : ι
⊢ (reflection P i)⁻¹ = reflection P i

Tactic:
refine Equiv.ext ?_ ?_ ?_

Result:
case refine_1
ι : 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
i : ι
⊢ (↑(reflection P i)⁻¹).weightMap = (↑(reflection P i)).weightMap

case refine_2
ι : 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
i : ι
⊢ (↑(reflection P i)⁻¹).coweightMap = (↑(reflection P i)).coweightMap

case refine_3
ι : 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
i : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv = (↑(reflection P i)).indexEquiv

Proof state:
case refine_2
ι : 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
i : ι
⊢ (↑(reflection P i)⁻¹).coweightMap = (↑(reflection P i)).coweightMap

Tactic:
exact LinearMap.ext_iff.mpr (fun x => by simp [← coweightEquiv_apply])

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
i : ι
x : M
⊢ (↑(reflection P i)⁻¹).weightMap x = (↑(reflection P i)).weightMap x

Tactic:
simp [← weightEquiv_apply]

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
i j : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv j = (↑(reflection P i)).indexEquiv j

Tactic:
simp only [← indexHom_apply, map_inv]

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
i j : ι
⊢ ((indexHom P) (reflection P i))⁻¹ j = ((indexHom P) (reflection P i)) j

Proof state:
case refine_3
ι : 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
i : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv = (↑(reflection P i)).indexEquiv

Tactic:
exact _root_.Equiv.ext (fun j => by simp only [← indexHom_apply, map_inv]; simp)

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
i : ι
x : N
⊢ (↑(reflection P i)⁻¹).coweightMap x = (↑(reflection P i)).coweightMap x

Tactic:
simp [← coweightEquiv_apply]

Result:
no goals