Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x✝ : M
⊢ (↑{ val := (↑f).comp ↑g, inv := ↑(symm P P (comp f g)), val_inv := ⋯, inv_val := ⋯ }).weightMap x✝ =
    (↑({ val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
            { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ })).weightMap
      x✝

pp: case coweightMap
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x✝ : N
⊢ (↑{ val := (↑f).comp ↑g, inv := ↑(symm P P (comp f g)), val_inv := ⋯, inv_val := ⋯ }).coweightMap x✝ =
    (↑({ val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
            { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ })).coweightMap
      x✝

pp: case indexEquiv
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x✝ : ι
⊢ (↑{ val := (↑f).comp ↑g, inv := ↑(symm P P (comp f g)), val_inv := ⋯, inv_val := ⋯ }).indexEquiv x✝ =
    (↑({ val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
            { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ })).indexEquiv
      x✝

Tactic:
<;>

Goal state after:
case weightMap
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x✝ : M
⊢ (↑{ val := (↑f).comp ↑g, inv := ↑(symm P P (comp f g)), val_inv := ⋯, inv_val := ⋯ }).weightMap x✝ =
    (↑({ val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
            { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ })).weightMap
      x✝

case coweightMap
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x✝ : N
⊢ (↑{ val := (↑f).comp ↑g, inv := ↑(symm P P (comp f g)), val_inv := ⋯, inv_val := ⋯ }).coweightMap x✝ =
    (↑({ val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
            { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ })).coweightMap
      x✝

case indexEquiv
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x✝ : ι
⊢ (↑{ val := (↑f).comp ↑g, inv := ↑(symm P P (comp f g)), val_inv := ⋯, inv_val := ⋯ }).indexEquiv x✝ =
    (↑({ val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
            { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ })).indexEquiv
      x✝