Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i : ι
⊢ ∀ (i : ι), f (P.root i) ∈ range ⇑P₂.root → f (P.root ((P.reflectionPerm i) i)) ∈ range ⇑P₂.root

pp: case 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i : ι
⊢ ∀ i ∈ b.support, f (P.root i) ∈ range ⇑P₂.root

pp: case 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i : ι
⊢ ∀ (i j : ι), f (P.root i) ∈ range ⇑P₂.root → j ∈ b.support → f (P.root ((P.reflectionPerm j) i)) ∈ range ⇑P₂.root

Tactic:
· exact fun j ⟨k, hk⟩ ↦ ⟨P₂.reflectionPerm k k, by simpa⟩

Goal state after:
case 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i : ι
⊢ ∀ i ∈ b.support, f (P.root i) ∈ range ⇑P₂.root

case 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i : ι
⊢ ∀ (i j : ι), f (P.root i) ∈ range ⇑P₂.root → j ∈ b.support → f (P.root ((P.reflectionPerm j) i)) ∈ range ⇑P₂.root