[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
[PROOFSTEP]
rcases Fintype.exists_pair_of_one_lt_card h with ⟨j, i, hij⟩
[GOAL]
case intro.intro
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
[PROOFSTEP]
let A := Eb R i j hij
[GOAL]
case intro.intro
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
[PROOFSTEP]
let B := Eb R j i hij.symm
[GOAL]
case intro.intro
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
[PROOFSTEP]
intro c
[GOAL]
case intro.intro
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
⊢ False
[PROOFSTEP]
have c' : A.val * B.val = B.val * A.val := by rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
⊢ ↑A * ↑B = ↑B * ↑A
[PROOFSTEP]
rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
[GOAL]
case intro.intro
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
c' : ↑A * ↑B = ↑B * ↑A
⊢ False
[PROOFSTEP]
simpa [stdBasisMatrix, Matrix.mul_apply, hij] using congr_fun (congr_fun c' i) i
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ A ∈ so n R ↔ Aᵀ = -A
[PROOFSTEP]
rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ IsSkewAdjoint 1 A ↔ Aᵀ = -A
[PROOFSTEP]
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ Pso p q R i * Pso p q R (-i) = 1
[PROOFSTEP]
ext (x y)
[GOAL]
case a.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ (Pso p q R i * Pso p q R (-i)) x y = OfNat.ofNat 1 x y
[PROOFSTEP]
rcases x with ⟨x⟩ | ⟨x⟩
[GOAL]
case a.h.inl
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = OfNat.ofNat 1 (Sum.inl x) y
[PROOFSTEP]
rcases y with ⟨y⟩ | ⟨y⟩
[GOAL]
case a.h.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = OfNat.ofNat 1 (Sum.inr x) y
[PROOFSTEP]
rcases y with ⟨y⟩ | ⟨y⟩
[GOAL]
case a.h.inl.inl
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = OfNat.ofNat 1 (Sum.inl x) (Sum.inl y)
[PROOFSTEP]
by_cases h : x = y
[GOAL]
case pos
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = OfNat.ofNat 1 (Sum.inl x) (Sum.inl y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h]
[GOAL]
case neg
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = OfNat.ofNat 1 (Sum.inl x) (Sum.inl y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h]
[GOAL]
case a.h.inl.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x : p
y : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inr y) = OfNat.ofNat 1 (Sum.inl x) (Sum.inr y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal]
[GOAL]
case a.h.inr.inl
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x : q
y : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inl y) = OfNat.ofNat 1 (Sum.inr x) (Sum.inl y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal]
[GOAL]
case a.h.inr.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = OfNat.ofNat 1 (Sum.inr x) (Sum.inr y)
[PROOFSTEP]
by_cases h : x = y
[GOAL]
case pos
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = OfNat.ofNat 1 (Sum.inr x) (Sum.inr y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h, hi]
[GOAL]
case neg
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = OfNat.ofNat 1 (Sum.inr x) (Sum.inr y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h, hi]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ (Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i = 1
[PROOFSTEP]
ext (x y)
[GOAL]
case a.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = OfNat.ofNat 1 x y
[PROOFSTEP]
rcases x with ⟨x⟩ | ⟨x⟩
[GOAL]
case a.h.inl
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = OfNat.ofNat 1 (Sum.inl x) y
[PROOFSTEP]
rcases y with ⟨y⟩ | ⟨y⟩
[GOAL]
case a.h.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = OfNat.ofNat 1 (Sum.inr x) y
[PROOFSTEP]
rcases y with ⟨y⟩ | ⟨y⟩
[GOAL]
case a.h.inl.inl
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) =
    OfNat.ofNat 1 (Sum.inl x) (Sum.inl y)
[PROOFSTEP]
by_cases h : x = y
[GOAL]
case pos
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) =
    OfNat.ofNat 1 (Sum.inl x) (Sum.inl y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h]
[GOAL]
case neg
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) =
    OfNat.ofNat 1 (Sum.inl x) (Sum.inl y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h]
[GOAL]
case a.h.inl.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x : p
y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inr y) =
    OfNat.ofNat 1 (Sum.inl x) (Sum.inr y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal]
[GOAL]
case a.h.inr.inl
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x : q
y : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inl y) =
    OfNat.ofNat 1 (Sum.inr x) (Sum.inl y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal]
[GOAL]
case a.h.inr.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) =
    OfNat.ofNat 1 (Sum.inr x) (Sum.inr y)
[PROOFSTEP]
by_cases h : x = y
[GOAL]
case pos
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) =
    OfNat.ofNat 1 (Sum.inr x) (Sum.inr y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h, hi]
[GOAL]
case neg
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) =
    OfNat.ofNat 1 (Sum.inr x) (Sum.inr y)
[PROOFSTEP]
simp [Pso, indefiniteDiagonal, h, hi]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ { x // x ∈ so' p q R } ≃ₗ⁅R⁆ { x // x ∈ so (p ⊕ q) R }
[PROOFSTEP]
apply (skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)).trans
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ { x // x ∈ skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) } ≃ₗ⁅R⁆
    { x // x ∈ so (p ⊕ q) R }
[PROOFSTEP]
apply LieEquiv.ofEq
[GOAL]
case h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ ↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) = ↑(so (p ⊕ q) R)
[PROOFSTEP]
ext A
[GOAL]
case h.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ↔
    A ∈ ↑(so (p ⊕ q) R)
[PROOFSTEP]
rw [indefiniteDiagonal_transform p q R hi]
[GOAL]
case h.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra 1) ↔ A ∈ ↑(so (p ⊕ q) R)
[PROOFSTEP]
rfl
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : { x // x ∈ so' p q R }
⊢ ↑(↑(soIndefiniteEquiv p q R hi) A) = (Pso p q R i)⁻¹ * ↑A * Pso p q R i
[PROOFSTEP]
rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply, skewAdjointMatricesLieSubalgebraEquiv_apply]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
⊢ S l R = fromBlocks 1 0 0 (-1)
[PROOFSTEP]
rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
⊢ S l R = diagonal (Sum.elim (fun x => 1) fun i => -1)
[PROOFSTEP]
rfl
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R
[PROOFSTEP]
have h : (PD l R)ᵀ * JD l R = Matrix.fromBlocks 1 1 1 (-1) := by
  simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
[PROOFSTEP]
simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R
[PROOFSTEP]
rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 * 1 + 1 * 1) (1 * -1 + 1 * 1) (1 * 1 + -1 * 1) (1 * -1 + -1 * 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
[PROOFSTEP]
congr
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks (1 * 1 + 1 * 1) (1 * -1 + 1 * 1) (1 * 1 + -1 * 1) (1 * -1 + -1 * 1) =
    fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
[PROOFSTEP]
simp [two_smul]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PD l R * ⅟2 • (PD l R)ᵀ = 1
[PROOFSTEP]
rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul, Matrix.fromBlocks_multiply]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • 1ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • (-1)ᵀ)
      (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • 1ᵀ) =
    1
[PROOFSTEP]
simp
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ { x // x ∈ typeD l R } ≃ₗ⁅R⁆ { x // x ∈ so' l l R }
[PROOFSTEP]
apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ Invertible (PD l R)
[PROOFSTEP]
infer_instance
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ { x // x ∈ skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R) } ≃ₗ⁅R⁆ { x // x ∈ so' l l R }
[PROOFSTEP]
apply LieEquiv.ofEq
[GOAL]
case h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ ↑(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) = ↑(so' l l R)
[PROOFSTEP]
ext A
[GOAL]
case h.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) ↔ A ∈ ↑(so' l l R)
[PROOFSTEP]
rw [jd_transform, ← unitOfInvertible_val (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
  mem_skewAdjointMatricesLieSubalgebra_unit_smul]
[GOAL]
case h.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (S l R) ↔ A ∈ ↑(so' l l R)
[PROOFSTEP]
rfl
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1
[PROOFSTEP]
rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * 1 + 0 * 0) (1 * 0 + 0 * ⅟(PD l R)) (0 * 1 + PD l R * 0) (0 * 0 + 1) = 1
[PROOFSTEP]
simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero, Matrix.fromBlocks_one]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ (PB l R)ᵀ * JB l R * PB l R = 2 • fromBlocks 1 0 0 (S l R)
[PROOFSTEP]
simp [PB, JB, jd_transform, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
[PROOFSTEP]
ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
[GOAL]
case a.inl.inl.unit.h.inl.inl.unit
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inl.inl.unit.h.inl.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inl.inl.unit.h.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val✝) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val✝)
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inl.inr.h.inl.inl.unit
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
i₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inl.inr.h.inl.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
i₃ j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inl.inr.h.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
i₃ val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inr val✝) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inr val✝)
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inr.h.inl.inl.unit
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝) (Sum.inl (Sum.inl PUnit.unit)) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝)
      (Sum.inl (Sum.inl PUnit.unit))
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inr.h.inl.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
val✝ j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝) (Sum.inl (Sum.inr j₃)) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝)
      (Sum.inl (Sum.inr j₃))
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inr.h.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
val✝¹ val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝¹) (Sum.inr val✝) =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝¹)
      (Sum.inr val✝)
[PROOFSTEP]
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply,
  Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true,
  Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false,
  Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
  Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff]
[GOAL]
case a.inl.inl.unit.h.inl.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
j₃ : l
⊢ 0 = OfNat.ofNat 0 PUnit.unit (Sum.inl j₃)
[PROOFSTEP]
congr 1
[GOAL]
case a.inl.inl.unit.h.inr
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
val✝ : l
⊢ 0 = OfNat.ofNat 0 PUnit.unit (Sum.inr val✝)
[PROOFSTEP]
congr 1
[GOAL]
case a.inl.inr.h.inl.inl.unit
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
i₃ : l
⊢ 0 = OfNat.ofNat 0 (Sum.inl i₃) PUnit.unit
[PROOFSTEP]
congr 1
[GOAL]
case a.inr.h.inl.inl.unit
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
val✝ : l
⊢ 0 = OfNat.ofNat 0 (Sum.inr val✝) PUnit.unit
[PROOFSTEP]
congr 1
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ { x // x ∈ typeB l R } ≃ₗ⁅R⁆ { x // x ∈ so' (Unit ⊕ l) l R }
[PROOFSTEP]
apply (skewAdjointMatricesLieSubalgebraEquiv (JB l R) (PB l R) (by infer_instance)).trans
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ Invertible (PB l R)
[PROOFSTEP]
infer_instance
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ { x // x ∈ skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R) } ≃ₗ⁅R⁆ { x // x ∈ so' (Unit ⊕ l) l R }
[PROOFSTEP]
symm
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ { x // x ∈ so' (Unit ⊕ l) l R } ≃ₗ⁅R⁆ { x // x ∈ skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R) }
[PROOFSTEP]
apply
  (skewAdjointMatricesLieSubalgebraEquivTranspose (indefiniteDiagonal (Sum Unit l) l R)
      (Matrix.reindexAlgEquiv _ (Equiv.sumAssoc PUnit l l)) (Matrix.transpose_reindex _ _)).trans
[GOAL]
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ { x //
      x ∈
        skewAdjointMatricesLieSubalgebra
          (↑(reindexAlgEquiv R (Equiv.sumAssoc PUnit l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) } ≃ₗ⁅R⁆
    { x // x ∈ skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R) }
[PROOFSTEP]
apply LieEquiv.ofEq
[GOAL]
case h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ ↑(skewAdjointMatricesLieSubalgebra
        (↑(reindexAlgEquiv R (Equiv.sumAssoc PUnit l l)) (indefiniteDiagonal (Unit ⊕ l) l R))) =
    ↑(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
[PROOFSTEP]
ext A
[GOAL]
case h.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (PUnit ⊕ l ⊕ l) (PUnit ⊕ l ⊕ l) R
⊢ A ∈
      ↑(skewAdjointMatricesLieSubalgebra
          (↑(reindexAlgEquiv R (Equiv.sumAssoc PUnit l l)) (indefiniteDiagonal (Unit ⊕ l) l R))) ↔
    A ∈ ↑(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
[PROOFSTEP]
rw [jb_transform, ← unitOfInvertible_val (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe, LieSubalgebra.mem_coe,
  mem_skewAdjointMatricesLieSubalgebra_unit_smul]
[GOAL]
case h.h
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
A : Matrix (PUnit ⊕ l ⊕ l) (PUnit ⊕ l ⊕ l) R
⊢ A ∈
      skewAdjointMatricesLieSubalgebra
        (↑(reindexAlgEquiv R (Equiv.sumAssoc PUnit l l)) (indefiniteDiagonal (Unit ⊕ l) l R)) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (fromBlocks 1 0 0 (S l R))
[PROOFSTEP]
simp [indefiniteDiagonal_assoc, S]
