case a.h
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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
ext (x y)
case a.h.inl.inl
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)

case a.h.inl.inr
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)

case a.h.inr.inl
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)

case a.h.inr.inr
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)
case a.h
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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
rcases x with ⟨x⟩|⟨x⟩ <;> rcases y with ⟨y⟩|⟨y⟩
no goals
case a.h.inl.inl
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)
by_cases h : x = y <;>
simp [Pso, indefiniteDiagonal, h]
no goals
case a.h.inl.inr
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)
simp [Pso, indefiniteDiagonal]
no goals
case a.h.inr.inl
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)
simp [Pso, indefiniteDiagonal]
no goals
case a.h.inr.inr
n : Type ?u.52016
p : Type u_1
q : Type u_2
l : Type ?u.52025
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)
by_cases h : x = y <;>
simp [Pso, indefiniteDiagonal, h, hi]