Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₀
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i : ι),
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
      ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b ((P.reflectionPerm i) i) ∈ U → ∃ j, u j ∈ U

pp: case h₁
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ i ∈ b.support, ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U

pp: case h₂
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
        j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b k ∈ U → ∃ j, u j ∈ U

Tactic:
· intro i h U hi
      replace hi : v b i ∈ ωConjLieSubmodule U := by simpa [hωv]
      obtain ⟨j, hj⟩ := h hi
      exact ⟨j, by simpa [hωu] using! hj⟩

Goal state after:
case h₁
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ i ∈ b.support, ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U

case h₂
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
        j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b k ∈ U → ∃ j, u j ∈ U