[GOAL]
x : PGame
⊢ birthday x = max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ birthday (mk α✝ β✝ a✝¹ a✝) =
    max (lsub fun i => birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i)) (lsub fun i => birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i))
[PROOFSTEP]
rw [birthday]
[GOAL]
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ max (lsub fun i => birthday (a✝¹ i)) (lsub fun i => birthday (a✝ i)) =
    max (lsub fun i => birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i)) (lsub fun i => birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i))
[PROOFSTEP]
rfl
[GOAL]
x : PGame
i : LeftMoves x
⊢ birthday (moveLeft x i) < birthday x
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i) < birthday (mk α✝ β✝ a✝¹ a✝)
[PROOFSTEP]
rw [birthday]
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i) < max (lsub fun i => birthday (a✝¹ i)) (lsub fun i => birthday (a✝ i))
[PROOFSTEP]
exact lt_max_of_lt_left (lt_lsub _ i)
[GOAL]
x : PGame
i : RightMoves x
⊢ birthday (moveRight x i) < birthday x
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i) < birthday (mk α✝ β✝ a✝¹ a✝)
[PROOFSTEP]
rw [birthday]
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i) < max (lsub fun i => birthday (a✝¹ i)) (lsub fun i => birthday (a✝ i))
[PROOFSTEP]
exact lt_max_of_lt_right (lt_lsub _ i)
[GOAL]
x : PGame
o : Ordinal.{u_1}
⊢ o < birthday x ↔ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
constructor
[GOAL]
case mp
x : PGame
o : Ordinal.{u_1}
⊢ o < birthday x → (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
rw [birthday_def]
[GOAL]
case mp
x : PGame
o : Ordinal.{u_1}
⊢ o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i)) →
    (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
intro h
[GOAL]
case mp
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
⊢ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
cases' lt_max_iff.1 h with h' h'
[GOAL]
case mp.inl
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveLeft x i)
⊢ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
left
[GOAL]
case mp.inl.h
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveLeft x i)
⊢ ∃ i, o ≤ birthday (moveLeft x i)
[PROOFSTEP]
rwa [lt_lsub_iff] at h'
[GOAL]
case mp.inr
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveRight x i)
⊢ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
right
[GOAL]
case mp.inr.h
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveRight x i)
⊢ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
rwa [lt_lsub_iff] at h'
[GOAL]
case mpr
x : PGame
o : Ordinal.{u_1}
⊢ ((∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)) → o < birthday x
[PROOFSTEP]
rintro (⟨i, hi⟩ | ⟨i, hi⟩)
[GOAL]
case mpr.inl.intro
x : PGame
o : Ordinal.{u_1}
i : LeftMoves x
hi : o ≤ birthday (moveLeft x i)
⊢ o < birthday x
[PROOFSTEP]
exact hi.trans_lt (birthday_moveLeft_lt i)
[GOAL]
case mpr.inr.intro
x : PGame
o : Ordinal.{u_1}
i : RightMoves x
hi : o ≤ birthday (moveRight x i)
⊢ o < birthday x
[PROOFSTEP]
exact hi.trans_lt (birthday_moveRight_lt i)
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ birthday (PGame.mk xl xr xL xR) = birthday (PGame.mk yl yr yL yR)
[PROOFSTEP]
unfold birthday
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ max (lsub fun i => birthday (xL i)) (lsub fun i => birthday (xR i)) =
    max (lsub fun i => birthday (yL i)) (lsub fun i => birthday (yR i))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xL i)) = lsub fun i => birthday (yL i)
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xR i)) = lsub fun i => birthday (yR i)
[PROOFSTEP]
all_goals
  apply lsub_eq_of_range_eq.{u, u, u}
  ext i; constructor
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xL i)) = lsub fun i => birthday (yL i)
[PROOFSTEP]
apply lsub_eq_of_range_eq.{u, u, u}
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (Set.range fun i => birthday (xL i)) = Set.range fun i => birthday (yL i)
[PROOFSTEP]
ext i
[GOAL]
case e_a.h
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xL i)) ↔ i ∈ Set.range fun i => birthday (yL i)
[PROOFSTEP]
constructor
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xR i)) = lsub fun i => birthday (yR i)
[PROOFSTEP]
apply lsub_eq_of_range_eq.{u, u, u}
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (Set.range fun i => birthday (xR i)) = Set.range fun i => birthday (yR i)
[PROOFSTEP]
ext i
[GOAL]
case e_a.h
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xR i)) ↔ i ∈ Set.range fun i => birthday (yR i)
[PROOFSTEP]
constructor
[GOAL]
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xL i)) → i ∈ Set.range fun i => birthday (yL i)
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yL i)) → i ∈ Set.range fun i => birthday (xL i)
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xR i)) → i ∈ Set.range fun i => birthday (yR i)
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yR i)) → i ∈ Set.range fun i => birthday (xR i)
[PROOFSTEP]
all_goals rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xL i)) → i ∈ Set.range fun i => birthday (yL i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yL i)) → i ∈ Set.range fun i => birthday (xL i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xR i)) → i ∈ Set.range fun i => birthday (yR i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yR i)) → i ∈ Set.range fun i => birthday (xR i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xl
⊢ (fun i => birthday (xL i)) j ∈ Set.range fun i => birthday (yL i)
[PROOFSTEP]
exact ⟨_, (r.moveLeft j).birthday_congr.symm⟩
[GOAL]
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yl
⊢ (fun i => birthday (yL i)) j ∈ Set.range fun i => birthday (xL i)
[PROOFSTEP]
exact ⟨_, (r.moveLeftSymm j).birthday_congr⟩
[GOAL]
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xr
⊢ (fun i => birthday (xR i)) j ∈ Set.range fun i => birthday (yR i)
[PROOFSTEP]
exact ⟨_, (r.moveRight j).birthday_congr.symm⟩
[GOAL]
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yr
⊢ (fun i => birthday (yR i)) j ∈ Set.range fun i => birthday (xR i)
[PROOFSTEP]
exact ⟨_, (r.moveRightSymm j).birthday_congr⟩
[GOAL]
x : PGame
⊢ birthday x = 0 ↔ IsEmpty (LeftMoves x) ∧ IsEmpty (RightMoves x)
[PROOFSTEP]
rw [birthday_def, max_eq_zero, lsub_eq_zero_iff, lsub_eq_zero_iff]
[GOAL]
⊢ birthday 0 = 0
[PROOFSTEP]
simp [inferInstanceAs (IsEmpty PEmpty)]
[GOAL]
⊢ birthday 1 = 1
[PROOFSTEP]
rw [birthday_def]
[GOAL]
⊢ max (lsub fun i => birthday (moveLeft 1 i)) (lsub fun i => birthday (moveRight 1 i)) = 1
[PROOFSTEP]
simp
[GOAL]
⊢ birthday star = 1
[PROOFSTEP]
rw [birthday_def]
[GOAL]
⊢ max (lsub fun i => birthday (moveLeft star i)) (lsub fun i => birthday (moveRight star i)) = 1
[PROOFSTEP]
simp
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ birthday (-mk xl xr xL xR) = birthday (mk xl xr xL xR)
[PROOFSTEP]
rw [birthday_def, birthday_def, max_comm]
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ max (lsub fun i => birthday (moveRight (-mk xl xr xL xR) i)) (lsub fun i => birthday (moveLeft (-mk xl xr xL xR) i)) =
    max (lsub fun i => birthday (moveLeft (mk xl xr xL xR) i)) (lsub fun i => birthday (moveRight (mk xl xr xL xR) i))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ (fun i => birthday (moveRight (-mk xl xr xL xR) i)) = fun i => birthday (moveLeft (mk xl xr xL xR) i)
[PROOFSTEP]
funext
[GOAL]
case e_a.e_f
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ (fun i => birthday (moveLeft (-mk xl xr xL xR) i)) = fun i => birthday (moveRight (mk xl xr xL xR) i)
[PROOFSTEP]
funext
[GOAL]
case e_a.e_f.h
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝ : RightMoves (-mk xl xr xL xR)
⊢ birthday (moveRight (-mk xl xr xL xR) x✝) = birthday (moveLeft (mk xl xr xL xR) x✝)
[PROOFSTEP]
apply neg_birthday
[GOAL]
case e_a.e_f.h
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝ : LeftMoves (-mk xl xr xL xR)
⊢ birthday (moveLeft (-mk xl xr xL xR) x✝) = birthday (moveRight (mk xl xr xL xR) x✝)
[PROOFSTEP]
apply neg_birthday
[GOAL]
o : Ordinal.{u_1}
⊢ birthday (toPGame o) = o
[PROOFSTEP]
induction' o using Ordinal.induction with o IH
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ birthday (toPGame o) = o
[PROOFSTEP]
rw [toPGame_def, PGame.birthday]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ max (lsub fun i => birthday (toPGame (typein (fun x x_1 => x < x_1) i))) (lsub fun i => birthday (PEmpty.elim i)) = o
[PROOFSTEP]
simp only [lsub_empty, max_zero_right]
  -- Porting note: was `nth_rw 1 [← lsub_typein o]`
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ (lsub fun i => birthday (toPGame (typein (fun x x_1 => x < x_1) i))) = o
[PROOFSTEP]
conv_rhs => rw [← lsub_typein o]
[GOAL]
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
| o
[PROOFSTEP]
rw [← lsub_typein o]
[GOAL]
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
| o
[PROOFSTEP]
rw [← lsub_typein o]
[GOAL]
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
| o
[PROOFSTEP]
rw [← lsub_typein o]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ (lsub fun i => birthday (toPGame (typein (fun x x_1 => x < x_1) i))) = lsub (typein fun x x_1 => x < x_1)
[PROOFSTEP]
congr with x
[GOAL]
case h.e_f.h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
x : (Quotient.out o).α
⊢ birthday (toPGame (typein (fun x x_1 => x < x_1) x)) = typein (fun x x_1 => x < x_1) x
[PROOFSTEP]
exact IH _ (typein_lt_self x)
[GOAL]
xl β✝ : Type u_1
xL : xl → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk xl β✝ xL a✝)
⊢ moveLeft (mk xl β✝ xL a✝) i ≤
    moveLeft (toPGame (birthday (mk xl β✝ xL a✝)))
      (↑toLeftMovesToPGame
        { val := birthday (moveLeft (mk xl β✝ xL a✝) i),
          property := (_ : birthday (moveLeft (mk xl β✝ xL a✝) i) < birthday (mk xl β✝ xL a✝)) })
[PROOFSTEP]
simp [le_birthday (xL i)]
[GOAL]
a b x : PGame
⊢ -toPGame (birthday x) ≤ x
[PROOFSTEP]
simpa only [neg_birthday, ← neg_le_iff] using le_birthday (-x)
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ birthday (mk xl xr xL xR + mk yl yr yL yR) = birthday (mk xl xr xL xR) ♯ birthday (mk yl yr yL yR)
[PROOFSTEP]
rw [birthday_def, nadd_def]
  -- Porting note: `simp` doesn't apply
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun i => birthday (moveLeft (mk xl xr xL xR + mk yl yr yL yR) i))
      (lsub fun i => birthday (moveRight (mk xl xr xL xR + mk yl yr yL yR) i)) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
erw [lsub_sum, lsub_sum]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (moveLeft (mk xl xr xL xR + mk yl yr yL yR) (Sum.inl a)))
        (lsub fun b => birthday (moveLeft (mk xl xr xL xR + mk yl yr yL yR) (Sum.inr b))))
      (max (lsub fun a => birthday (moveRight (mk xl xr xL xR + mk yl yr yL yR) (Sum.inl a)))
        (lsub fun b => birthday (moveRight (mk xl xr xL xR + mk yl yr yL yR) (Sum.inr b)))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
simp only [lsub_sum, mk_add_moveLeft_inl, moveLeft_mk, mk_add_moveLeft_inr, mk_add_moveRight_inl, moveRight_mk,
  mk_add_moveRight_inr]
  -- Porting note: Originally `simp only [birthday_add]`, but this causes an error in
      -- `termination_by`. Use a workaround.
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
      (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun a => birthday (xL a + mk yl yr yL yR)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun a => birthday (xL a + mk yl yr yL yR)
[PROOFSTEP]
intro a
[GOAL]
case h
a✝ b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
a : xl
| birthday (xL a + mk yl yr yL yR)
[PROOFSTEP]
rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
      (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun b => birthday (mk xl xr xL xR + yL b)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun b => birthday (mk xl xr xL xR + yL b)
[PROOFSTEP]
intro b
[GOAL]
case h
a b✝ x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
b : yl
| birthday (mk xl xr xL xR + yL b)
[PROOFSTEP]
rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
      (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun a => birthday (xR a + mk yl yr yL yR)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun a => birthday (xR a + mk yl yr yL yR)
[PROOFSTEP]
intro a
[GOAL]
case h
a✝ b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
a : xr
| birthday (xR a + mk yl yr yL yR)
[PROOFSTEP]
rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
      (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun b => birthday (mk xl xr xL xR + yR b)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun b => birthday (mk xl xr xL xR + yR b)
[PROOFSTEP]
intro b
[GOAL]
case h
a b✝ x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
b : yr
| birthday (mk xl xr xL xR + yR b)
[PROOFSTEP]
rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
      (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
rw [max_max_max_comm]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)))
      (max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
congr
[GOAL]
case e_a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) =
    blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case e_a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b)) =
    blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b'
[PROOFSTEP]
apply le_antisymm
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) ≤
    blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b)) ≤
    blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b'
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
any_goals
  exact
    max_le_iff.2
      ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
        lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) ≤
    blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b)) ≤
    blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b'
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
all_goals
  refine blsub_le_iff.2 fun i hi => ?_
  rcases lt_birthday_iff.1 hi with (⟨j, hj⟩ | ⟨j, hj⟩)
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
refine blsub_le_iff.2 fun i hi => ?_
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk xl xr xL xR)
⊢ i ♯ birthday (mk yl yr yL yR) <
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
rcases lt_birthday_iff.1 hi with (⟨j, hj⟩ | ⟨j, hj⟩)
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
refine blsub_le_iff.2 fun i hi => ?_
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk yl yr yL yR)
⊢ birthday (mk xl xr xL xR) ♯ i <
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
rcases lt_birthday_iff.1 hi with (⟨j, hj⟩ | ⟨j, hj⟩)
[GOAL]
case e_a.a.inl.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk xl xr xL xR)
j : LeftMoves (mk xl xr xL xR)
hj : i ≤ birthday (moveLeft (mk xl xr xL xR) j)
⊢ i ♯ birthday (mk yl yr yL yR) <
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
exact lt_max_of_lt_left ((nadd_le_nadd_right hj _).trans_lt (lt_lsub _ _))
[GOAL]
case e_a.a.inr.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk xl xr xL xR)
j : RightMoves (mk xl xr xL xR)
hj : i ≤ birthday (moveRight (mk xl xr xL xR) j)
⊢ i ♯ birthday (mk yl yr yL yR) <
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
exact lt_max_of_lt_right ((nadd_le_nadd_right hj _).trans_lt (lt_lsub _ _))
[GOAL]
case e_a.a.inl.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk yl yr yL yR)
j : LeftMoves (mk yl yr yL yR)
hj : i ≤ birthday (moveLeft (mk yl yr yL yR) j)
⊢ birthday (mk xl xr xL xR) ♯ i <
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
exact lt_max_of_lt_left ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
[GOAL]
case e_a.a.inr.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk yl yr yL yR)
j : RightMoves (mk yl yr yL yR)
hj : i ≤ birthday (moveRight (mk yl yr yL yR) j)
⊢ birthday (mk xl xr xL xR) ♯ i <
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
exact lt_max_of_lt_right ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
[GOAL]
a b x : PGame
⊢ birthday (a + 0) = birthday a
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
⊢ birthday (0 + a) = birthday a
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
⊢ birthday (a + 1) = Order.succ (birthday a)
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
⊢ birthday (1 + a) = Order.succ (birthday a)
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
n : ℕ
⊢ birthday ↑(n + 1) = ↑(n + 1)
[PROOFSTEP]
simp [birthday_nat_cast]
[GOAL]
a b x : PGame
n : ℕ
⊢ birthday (a + ↑n) = birthday a + ↑n
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
n : ℕ
⊢ birthday (↑n + a) = birthday a + ↑n
[PROOFSTEP]
simp


[GOAL]
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ { val := b, property := hb } = default
[PROOFSTEP]
congr
[GOAL]
case e_val
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ b = a
[PROOFSTEP]
exact he b hb
[GOAL]
n : ℕ
⊢ 0 < 1 + n
[PROOFSTEP]
rw [Nat.add_comm]
[GOAL]
n : ℕ
⊢ 0 < n + 1
[PROOFSTEP]
exact Nat.zero_lt_succ _
[GOAL]
α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p x
[PROOFSTEP]
rwa [Unique.eq_default x]
[GOAL]
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ { toInhabited := { default := x }, uniq := h } = { toInhabited := { default := y }, uniq := uniq✝ }
[PROOFSTEP]
congr
[GOAL]
case e_toInhabited.e_default
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
[PROOFSTEP]
rw [h x, h y]
[GOAL]
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α
[PROOFSTEP]
constructor
[GOAL]
case left
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α
[PROOFSTEP]
exact inferInstance
[GOAL]
case right
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Nonempty α
[PROOFSTEP]
exact inferInstance
[GOAL]
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
⊢ Unique α
[PROOFSTEP]
inhabit α
[GOAL]
α : Sort u
x✝ : Subsingleton α ∧ Nonempty α
hs : Subsingleton α
hn : Nonempty α
inhabited_h : Inhabited α
⊢ Unique α
[PROOFSTEP]
exact Unique.mk' α
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
⊢ f = Function.const α (f default)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f x = Function.const α (f default) x
[PROOFSTEP]
rw [Subsingleton.elim x default]
[GOAL]
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f default = Function.const α (f default) default
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f i) (Function.const α (f default) x✝¹)
[PROOFSTEP]
rw [Subsingleton.elim i default]
[GOAL]
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f default) (Function.const α (f default) x✝¹)
[PROOFSTEP]
rfl
[GOAL]
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f
[PROOFSTEP]
rw [Function.bijective_iff_has_inverse]
[GOAL]
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
[PROOFSTEP]
refine' ⟨default, _, _⟩
[GOAL]
case refine'_1
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.LeftInverse default f
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.RightInverse default f
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : A
⊢ default (f x) = x
[PROOFSTEP]
simp
[GOAL]
case refine'_2
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
x : B
⊢ f (default x) = x
[PROOFSTEP]
simp
[GOAL]
α : Sort u
y : α
x✝ : { x // x = y }
x : α
hx : x = y
⊢ { val := x, property := hx } = default
[PROOFSTEP]
congr
[GOAL]
α : Sort u
y : α
x✝ : { x // y = x }
x : α
hx : y = x
⊢ { val := x, property := hx } = default
[PROOFSTEP]
subst hx
[GOAL]
α : Sort u
y : α
x✝ : { x // y = x }
⊢ { val := y, property := (_ : y = y) } = default
[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 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]