[GOAL]
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ Principal op o ↔ Principal (Function.swap op) o
[PROOFSTEP]
constructor
[GOAL]
case mp
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ Principal op o → Principal (Function.swap op) o
[PROOFSTEP]
exact fun h a b ha hb => h hb ha
[GOAL]
case mpr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ Principal (Function.swap op) o → Principal op o
[PROOFSTEP]
exact fun h a b ha hb => h hb ha
[GOAL]
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ Principal op 1 ↔ op 0 0 = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h a b ha hb => _⟩
[GOAL]
case refine'_1
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : Principal op 1
⊢ op 0 0 = 0
[PROOFSTEP]
rw [← lt_one_iff_zero]
[GOAL]
case refine'_1
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : Principal op 1
⊢ op 0 0 < 1
[PROOFSTEP]
exact h zero_lt_one zero_lt_one
[GOAL]
case refine'_2
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : op 0 0 = 0
a b : Ordinal.{u_1}
ha : a < 1
hb : b < 1
⊢ op a b < 1
[PROOFSTEP]
rwa [lt_one_iff_zero, ha, hb] at *
[GOAL]
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a o : Ordinal.{u_1}
hao : a < o
ho : Principal op o
n : ℕ
⊢ (op a)^[n] a < o
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a o : Ordinal.{u_1}
hao : a < o
ho : Principal op o
⊢ (op a)^[Nat.zero] a < o
[PROOFSTEP]
rwa [Function.iterate_zero]
[GOAL]
case succ
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a o : Ordinal.{u_1}
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a)^[Nat.succ n] a < o
[PROOFSTEP]
rw [Function.iterate_succ']
[GOAL]
case succ
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a o : Ordinal.{u_1}
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o
[PROOFSTEP]
exact ho hao hn
[GOAL]
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
a o : Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ op a o = o
[PROOFSTEP]
refine' le_antisymm _ (H.self_le _)
[GOAL]
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
a o : Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ op a o ≤ o
[PROOFSTEP]
rw [← IsNormal.bsup_eq.{u, u} H ho', bsup_le_iff]
[GOAL]
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
a o : Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ ∀ (i : Ordinal.{u}), i < o → op a i ≤ o
[PROOFSTEP]
exact fun b hbo => (ho hao hbo).le
[GOAL]
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
ha : a < nfp (fun o' => blsub₂ o' o' fun a x b x => op a b) o
hb : b < nfp (fun o' => blsub₂ o' o' fun a x b x => op a b) o
⊢ op a b < nfp (fun o' => blsub₂ o' o' fun a x b x => op a b) o
[PROOFSTEP]
rw [lt_nfp] at *
[GOAL]
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
ha : ∃ n, a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
hb : ∃ n, b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
[PROOFSTEP]
cases' ha with m hm
[GOAL]
case intro
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
hb : ∃ n, b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
⊢ ∃ n, op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
[PROOFSTEP]
cases' hb with n hn
[GOAL]
case intro.intro
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
[PROOFSTEP]
cases'
  le_total ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with
  h h
[GOAL]
case intro.intro.inl
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
h : (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o ≤ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
[PROOFSTEP]
use n + 1
[GOAL]
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
h : (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o ≤ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
⊢ op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n + 1] o
[PROOFSTEP]
rw [Function.iterate_succ']
[GOAL]
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
h : (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o ≤ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
⊢ op a b < ((fun o' => blsub₂ o' o' fun a x b x => op a b) ∘ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n]) o
[PROOFSTEP]
exact lt_blsub₂ (@fun a _ b _ => op a b) (hm.trans_le h) hn
[GOAL]
case intro.intro.inr
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
h : (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o ≤ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
⊢ ∃ n, op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
[PROOFSTEP]
use m + 1
[GOAL]
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
h : (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o ≤ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
⊢ op a b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m + 1] o
[PROOFSTEP]
rw [Function.iterate_succ']
[GOAL]
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o
h : (fun o' => blsub₂ o' o' fun a x b x => op a b)^[n] o ≤ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m] o
⊢ op a b < ((fun o' => blsub₂ o' o' fun a x b x => op a b) ∘ (fun o' => blsub₂ o' o' fun a x b x => op a b)^[m]) o
[PROOFSTEP]
exact lt_blsub₂ (@fun a _ b _ => op a b) hm (hn.trans_le h)
[GOAL]
o : Ordinal.{u_1}
ho : o ≤ 1
⊢ Principal (fun x x_1 => x + x_1) o
[PROOFSTEP]
rcases le_one_iff.1 ho with (rfl | rfl)
[GOAL]
case inl
ho : 0 ≤ 1
⊢ Principal (fun x x_1 => x + x_1) 0
[PROOFSTEP]
exact principal_zero
[GOAL]
case inr
ho : 1 ≤ 1
⊢ Principal (fun x x_1 => x + x_1) 1
[PROOFSTEP]
exact principal_add_one
[GOAL]
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
⊢ IsLimit o
[PROOFSTEP]
refine' ⟨fun ho₀ => _, fun a hao => _⟩
[GOAL]
case refine'_1
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
ho₀ : o = 0
⊢ False
[PROOFSTEP]
rw [ho₀] at ho₁
[GOAL]
case refine'_1
o : Ordinal.{u_1}
ho₁ : 1 < 0
ho : Principal (fun x x_1 => x + x_1) o
ho₀ : o = 0
⊢ False
[PROOFSTEP]
exact not_lt_of_gt zero_lt_one ho₁
[GOAL]
case refine'_2
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
⊢ succ a < o
[PROOFSTEP]
cases' eq_or_ne a 0 with ha ha
[GOAL]
case refine'_2.inl
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
ha : a = 0
⊢ succ a < o
[PROOFSTEP]
rw [ha, succ_zero]
[GOAL]
case refine'_2.inl
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
ha : a = 0
⊢ 1 < o
[PROOFSTEP]
exact ho₁
[GOAL]
case refine'_2.inr
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
ha : a ≠ 0
⊢ succ a < o
[PROOFSTEP]
refine' lt_of_le_of_lt _ (ho hao hao)
[GOAL]
case refine'_2.inr
o : Ordinal.{u_1}
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
ha : a ≠ 0
⊢ succ a ≤ (fun x x_1 => x + x_1) a a
[PROOFSTEP]
rwa [← add_one_eq_succ, add_le_add_iff_left, one_le_iff_ne_zero]
[GOAL]
o : Ordinal.{u_1}
⊢ Principal (fun x x_1 => x + x_1) o ↔ ∀ (a : Ordinal.{u_1}), a < o → a + o = o
[PROOFSTEP]
refine' ⟨fun ho a hao => _, fun h a b hao hbo => _⟩
[GOAL]
case refine'_1
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
⊢ a + o = o
[PROOFSTEP]
cases' lt_or_le 1 o with ho₁ ho₁
[GOAL]
case refine'_1.inl
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
ho₁ : 1 < o
⊢ a + o = o
[PROOFSTEP]
exact op_eq_self_of_principal hao (add_isNormal a) ho (principal_add_isLimit ho₁ ho)
[GOAL]
case refine'_1.inr
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal.{u_1}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o
[PROOFSTEP]
rcases le_one_iff.1 ho₁ with (rfl | rfl)
[GOAL]
case refine'_1.inr.inl
a : Ordinal.{u_1}
ho : Principal (fun x x_1 => x + x_1) 0
hao : a < 0
ho₁ : 0 ≤ 1
⊢ a + 0 = 0
[PROOFSTEP]
exact (Ordinal.not_lt_zero a hao).elim
[GOAL]
case refine'_1.inr.inr
a : Ordinal.{u_1}
ho : Principal (fun x x_1 => x + x_1) 1
hao : a < 1
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
[PROOFSTEP]
rw [lt_one_iff_zero] at hao
[GOAL]
case refine'_1.inr.inr
a : Ordinal.{u_1}
ho : Principal (fun x x_1 => x + x_1) 1
hao : a = 0
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
[PROOFSTEP]
rw [hao, zero_add]
[GOAL]
case refine'_2
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b < o
[PROOFSTEP]
rw [← h a hao]
[GOAL]
case refine'_2
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b < a + o
[PROOFSTEP]
exact (add_isNormal a).strictMono hbo
[GOAL]
a : Ordinal.{u_1}
ha : ¬Principal (fun x x_1 => x + x_1) a
⊢ ∃ b c x x, b + c = a
[PROOFSTEP]
unfold Principal at ha
[GOAL]
a : Ordinal.{u_1}
ha : ¬∀ ⦃a_1 b : Ordinal.{u_1}⦄, a_1 < a → b < a → (fun x x_1 => x + x_1) a_1 b < a
⊢ ∃ b c x x, b + c = a
[PROOFSTEP]
push_neg at ha
[GOAL]
a : Ordinal.{u_1}
ha : Exists fun ⦃a_1⦄ => Exists fun ⦃b⦄ => a_1 < a ∧ b < a ∧ a ≤ a_1 + b
⊢ ∃ b c x x, b + c = a
[PROOFSTEP]
rcases ha with ⟨b, c, hb, hc, H⟩
[GOAL]
case intro.intro.intro.intro
a b c : Ordinal.{u_1}
hb : b < a
hc : c < a
H : a ≤ b + c
⊢ ∃ b c x x, b + c = a
[PROOFSTEP]
refine' ⟨b, _, hb, lt_of_le_of_ne (sub_le_self a b) fun hab => _, Ordinal.add_sub_cancel_of_le hb.le⟩
[GOAL]
case intro.intro.intro.intro
a b c : Ordinal.{u_1}
hb : b < a
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False
[PROOFSTEP]
rw [← sub_le, hab] at H
[GOAL]
case intro.intro.intro.intro
a b c : Ordinal.{u_1}
hb : b < a
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False
[PROOFSTEP]
exact H.not_lt hc
[GOAL]
a : Ordinal.{u_1}
H : ∀ ⦃b c : Ordinal.{u_1}⦄, b < a → c < a → b + c ≠ a
⊢ Principal (fun x x_1 => x + x_1) a
[PROOFSTEP]
by_contra' ha
[GOAL]
a : Ordinal.{u_1}
H : ∀ ⦃b c : Ordinal.{u_1}⦄, b < a → c < a → b + c ≠ a
ha : ¬Principal (fun x x_1 => x + x_1) a
⊢ False
[PROOFSTEP]
rcases exists_lt_add_of_not_principal_add ha with ⟨b, c, hb, hc, rfl⟩
[GOAL]
case intro.intro.intro.intro
b c : Ordinal.{u_1}
H : ∀ ⦃b_1 c_1 : Ordinal.{u_1}⦄, b_1 < b + c → c_1 < b + c → b_1 + c_1 ≠ b + c
ha : ¬Principal (fun x x_1 => x + x_1) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False
[PROOFSTEP]
exact (H hb hc).irrefl
[GOAL]
a : Ordinal.{u_1}
h : a < ω
⊢ a + ω = ω
[PROOFSTEP]
rcases lt_omega.1 h with ⟨n, rfl⟩
[GOAL]
case intro
n : ℕ
h : ↑n < ω
⊢ ↑n + ω = ω
[PROOFSTEP]
clear h
[GOAL]
case intro
n : ℕ
⊢ ↑n + ω = ω
[PROOFSTEP]
induction' n with n IH
[GOAL]
case intro.zero
⊢ ↑Nat.zero + ω = ω
[PROOFSTEP]
rw [Nat.cast_zero, zero_add]
[GOAL]
case intro.succ
n : ℕ
IH : ↑n + ω = ω
⊢ ↑(Nat.succ n) + ω = ω
[PROOFSTEP]
rwa [Nat.cast_succ, add_assoc, one_add_of_omega_le (le_refl _)]
[GOAL]
a b : Ordinal.{u_1}
h : a < ω ^ b
⊢ a + ω ^ b = ω ^ b
[PROOFSTEP]
refine' le_antisymm _ (le_add_left _ _)
[GOAL]
a b : Ordinal.{u_1}
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b
[PROOFSTEP]
induction' b using limitRecOn with b _ b l IH
[GOAL]
case H₁
a b : Ordinal.{u_1}
h✝ : a < ω ^ b
h : a < ω ^ 0
⊢ a + ω ^ 0 ≤ ω ^ 0
[PROOFSTEP]
rw [opow_zero, ← succ_zero, lt_succ_iff, Ordinal.le_zero] at h
[GOAL]
case H₁
a b : Ordinal.{u_1}
h✝ : a < ω ^ b
h : a = 0
⊢ a + ω ^ 0 ≤ ω ^ 0
[PROOFSTEP]
rw [h, zero_add]
[GOAL]
case H₂
a b✝ : Ordinal.{u_1}
h✝ : a < ω ^ b✝
b : Ordinal.{u_1}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ succ b
⊢ a + ω ^ succ b ≤ ω ^ succ b
[PROOFSTEP]
rw [opow_succ] at h
[GOAL]
case H₂
a b✝ : Ordinal.{u_1}
h✝ : a < ω ^ b✝
b : Ordinal.{u_1}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
⊢ a + ω ^ succ b ≤ ω ^ succ b
[PROOFSTEP]
rcases(lt_mul_of_limit omega_isLimit).1 h with ⟨x, xo, ax⟩
[GOAL]
case H₂.intro.intro
a b✝ : Ordinal.{u_1}
h✝ : a < ω ^ b✝
b : Ordinal.{u_1}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal.{u_1}
xo : x < ω
ax : a < ω ^ b * x
⊢ a + ω ^ succ b ≤ ω ^ succ b
[PROOFSTEP]
refine' le_trans (add_le_add_right (le_of_lt ax) _) _
[GOAL]
case H₂.intro.intro
a b✝ : Ordinal.{u_1}
h✝ : a < ω ^ b✝
b : Ordinal.{u_1}
a✝ : a < ω ^ b → a + ω ^ b ≤ ω ^ b
h : a < ω ^ b * ω
x : Ordinal.{u_1}
xo : x < ω
ax : a < ω ^ b * x
⊢ ω ^ b * x + ω ^ succ b ≤ ω ^ succ b
[PROOFSTEP]
rw [opow_succ, ← mul_add, add_omega xo]
[GOAL]
case H₃
a b✝ : Ordinal.{u_1}
h✝ : a < ω ^ b✝
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
⊢ a + ω ^ b ≤ ω ^ b
[PROOFSTEP]
rcases(lt_opow_of_limit omega_ne_zero l).1 h with ⟨x, xb, ax⟩
[GOAL]
case H₃.intro.intro
a b✝ : Ordinal.{u_1}
h✝ : a < ω ^ b✝
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → a < ω ^ o' → a + ω ^ o' ≤ ω ^ o'
h : a < ω ^ b
x : Ordinal.{u_1}
xb : x < b
ax : a < ω ^ x
⊢ a + ω ^ b ≤ ω ^ b
[PROOFSTEP]
exact
  (((add_isNormal a).trans (opow_isNormal one_lt_omega)).limit_le l).2 fun y yb =>
    (add_le_add_left (opow_le_opow_right omega_pos (le_max_right _ _)) _).trans
      (le_trans (IH _ (max_lt xb yb) (ax.trans_le <| opow_le_opow_right omega_pos (le_max_left _ _)))
        (opow_le_opow_right omega_pos <| le_of_lt <| max_lt xb yb))
[GOAL]
o : Ordinal.{u_1}
⊢ Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
[PROOFSTEP]
rcases eq_or_ne o 0 with (rfl | ho)
[GOAL]
case inl
⊢ Principal (fun x x_1 => x + x_1) 0 ↔ 0 = 0 ∨ ∃ a, 0 = ω ^ a
[PROOFSTEP]
simp only [principal_zero, Or.inl]
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
[PROOFSTEP]
rw [principal_add_iff_add_left_eq_self]
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (∀ (a : Ordinal.{u_1}), a < o → a + o = o) ↔ o = 0 ∨ ∃ a, o = ω ^ a
[PROOFSTEP]
simp only [ho, false_or_iff]
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (∀ (a : Ordinal.{u_1}), a < o → a + o = o) ↔ ∃ a, o = ω ^ a
[PROOFSTEP]
refine'
  ⟨fun H => ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ ho)).resolve_left fun h => _).symm⟩, fun ⟨b, e⟩ =>
    e.symm ▸ fun a => add_omega_opow⟩
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
⊢ False
[PROOFSTEP]
have := H _ h
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ False
[PROOFSTEP]
have := lt_opow_succ_log_self one_lt_omega o
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : o < ω ^ succ (log ω o)
⊢ False
[PROOFSTEP]
rw [opow_succ, lt_mul_of_limit omega_isLimit] at this
[GOAL]
case inr
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this✝ : ω ^ log ω o + o = o
this : ∃ c', c' < ω ∧ o < ω ^ log ω o * c'
⊢ False
[PROOFSTEP]
rcases this with ⟨a, ao, h'⟩
[GOAL]
case inr.intro.intro
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
a : Ordinal.{u_1}
ao : a < ω
h' : o < ω ^ log ω o * a
⊢ False
[PROOFSTEP]
rcases lt_omega.1 ao with ⟨n, rfl⟩
[GOAL]
case inr.intro.intro.intro
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
ao : ↑n < ω
h' : o < ω ^ log ω o * ↑n
⊢ False
[PROOFSTEP]
clear ao
[GOAL]
case inr.intro.intro.intro
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
h' : o < ω ^ log ω o * ↑n
⊢ False
[PROOFSTEP]
revert h'
[GOAL]
case inr.intro.intro.intro
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ o < ω ^ log ω o * ↑n → False
[PROOFSTEP]
apply not_lt_of_le
[GOAL]
case inr.intro.intro.intro.h
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n ≤ o
[PROOFSTEP]
suffices e : (omega ^ log omega o) * ↑n + o = o
[GOAL]
case inr.intro.intro.intro.h
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
e : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑n ≤ o
[PROOFSTEP]
simpa only [e] using le_add_right ((omega ^ log omega o) * ↑n) o
[GOAL]
case e
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
⊢ ω ^ log ω o * ↑n + o = o
[PROOFSTEP]
induction' n with n IH
[GOAL]
case e.zero
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
⊢ ω ^ log ω o * ↑Nat.zero + o = o
[PROOFSTEP]
simp [Nat.cast_zero, mul_zero, zero_add]
[GOAL]
case e.succ
o : Ordinal.{u_1}
ho : o ≠ 0
H : ∀ (a : Ordinal.{u_1}), a < o → a + o = o
h : ω ^ log ω o < o
this : ω ^ log ω o + o = o
n : ℕ
IH : ω ^ log ω o * ↑n + o = o
⊢ ω ^ log ω o * ↑(Nat.succ n) + o = o
[PROOFSTEP]
simp only [Nat.cast_succ, mul_add_one, add_assoc, this, IH]
[GOAL]
a : Ordinal.{u_1}
ha : Principal (fun x x_1 => x + x_1) a
b : Ordinal.{u_1}
⊢ Principal (fun x x_1 => x + x_1) (a ^ b)
[PROOFSTEP]
rcases principal_add_iff_zero_or_omega_opow.1 ha with (rfl | ⟨c, rfl⟩)
[GOAL]
case inl
b : Ordinal.{u_1}
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ b)
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inl.inl
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ 0)
[PROOFSTEP]
rw [opow_zero]
[GOAL]
case inl.inl
ha : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) 1
[PROOFSTEP]
exact principal_add_one
[GOAL]
case inl.inr
b : Ordinal.{u_1}
ha : Principal (fun x x_1 => x + x_1) 0
hb : b ≠ 0
⊢ Principal (fun x x_1 => x + x_1) (0 ^ b)
[PROOFSTEP]
rwa [zero_opow hb]
[GOAL]
case inr.intro
b c : Ordinal.{u_1}
ha : Principal (fun x x_1 => x + x_1) (ω ^ c)
⊢ Principal (fun x x_1 => x + x_1) ((ω ^ c) ^ b)
[PROOFSTEP]
rw [← opow_mul]
[GOAL]
case inr.intro
b c : Ordinal.{u_1}
ha : Principal (fun x x_1 => x + x_1) (ω ^ c)
⊢ Principal (fun x x_1 => x + x_1) (ω ^ (c * b))
[PROOFSTEP]
exact principal_add_omega_opow _
[GOAL]
a b c : Ordinal.{u_1}
h₁ : a < ω ^ b
h₂ : ω ^ b ≤ c
⊢ a + c = c
[PROOFSTEP]
rw [← Ordinal.add_sub_cancel_of_le h₂, ← add_assoc, add_omega_opow h₁]
[GOAL]
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) (a * b)
[PROOFSTEP]
rcases eq_zero_or_pos a with (rfl | _)
[GOAL]
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) (0 * b)
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) 0
[PROOFSTEP]
exact principal_zero
[GOAL]
case inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
⊢ Principal (fun x x_1 => x + x_1) (a * b)
[PROOFSTEP]
rcases eq_zero_or_pos b with (rfl | hb₁')
[GOAL]
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) (a * 0)
[PROOFSTEP]
rw [mul_zero]
[GOAL]
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : Principal (fun x x_1 => x + x_1) 0
⊢ Principal (fun x x_1 => x + x_1) 0
[PROOFSTEP]
exact principal_zero
[GOAL]
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁' : 0 < b
⊢ Principal (fun x x_1 => x + x_1) (a * b)
[PROOFSTEP]
rw [← succ_le_iff, succ_zero] at hb₁'
[GOAL]
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
⊢ Principal (fun x x_1 => x + x_1) (a * b)
[PROOFSTEP]
intro c d hc hd
[GOAL]
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : c < a * b
hd : d < a * b
⊢ (fun x x_1 => x + x_1) c d < a * b
[PROOFSTEP]
rw [lt_mul_of_limit (principal_add_isLimit (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
[GOAL]
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c', c' < b ∧ c < a * c'
hd : ∃ c', c' < b ∧ d < a * c'
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
[PROOFSTEP]
rcases hc with ⟨x, hx, hx'⟩
[GOAL]
case inr.inr.intro.intro
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hd : ∃ c', c' < b ∧ d < a * c'
x : Ordinal.{u}
hx : x < b
hx' : c < a * x
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
[PROOFSTEP]
rcases hd with ⟨y, hy, hy'⟩
[GOAL]
case inr.inr.intro.intro.intro.intro
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
[PROOFSTEP]
use x + y, hb hx hy
[GOAL]
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x x_1 => x + x_1) c d < a * (x + y)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
h✝ : 0 < a
hb₁'✝ : 0 < b
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x x_1 => x + x_1) c d < a * x + a * y
[PROOFSTEP]
exact Left.add_lt_add hx' hy'
[GOAL]
⊢ Principal (fun x x_1 => x * x_1) 1
[PROOFSTEP]
rw [principal_one_iff]
[GOAL]
⊢ 0 * 0 = 0
[PROOFSTEP]
exact zero_mul _
[GOAL]
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ (fun x x_1 => x * x_1) a b < 2
[PROOFSTEP]
have h₂ : succ (1 : Ordinal) = 2 := by simp
[GOAL]
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ succ 1 = 2
[PROOFSTEP]
simp
[GOAL]
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
h₂ : succ 1 = 2
⊢ (fun x x_1 => x * x_1) a b < 2
[PROOFSTEP]
dsimp only
[GOAL]
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
h₂ : succ 1 = 2
⊢ a * b < 2
[PROOFSTEP]
rw [← h₂, lt_succ_iff] at ha hb ⊢
[GOAL]
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
h₂ : succ 1 = 2
⊢ a * b ≤ 1
[PROOFSTEP]
convert mul_le_mul' ha hb
[GOAL]
case h.e'_4
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
h₂ : succ 1 = 2
⊢ 1 = 1 * 1
[PROOFSTEP]
exact (mul_one 1).symm
[GOAL]
o : Ordinal.{u_1}
ho : o ≤ 2
⊢ Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
rcases lt_or_eq_of_le ho with (ho | rfl)
[GOAL]
case inl
o : Ordinal.{u_1}
ho✝ : o ≤ 2
ho : o < 2
⊢ Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
have h₂ : succ (1 : Ordinal) = 2 := by simp
[GOAL]
o : Ordinal.{u_1}
ho✝ : o ≤ 2
ho : o < 2
⊢ succ 1 = 2
[PROOFSTEP]
simp
[GOAL]
case inl
o : Ordinal.{u_1}
ho✝ : o ≤ 2
ho : o < 2
h₂ : succ 1 = 2
⊢ Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
rw [← h₂, lt_succ_iff] at ho
[GOAL]
case inl
o : Ordinal.{u_1}
ho✝ : o ≤ 2
ho : o ≤ 1
h₂ : succ 1 = 2
⊢ Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
rcases lt_or_eq_of_le ho with (ho | rfl)
[GOAL]
case inl.inl
o : Ordinal.{u_1}
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
h₂ : succ 1 = 2
ho : o < 1
⊢ Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
rw [lt_one_iff_zero.1 ho]
[GOAL]
case inl.inl
o : Ordinal.{u_1}
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
h₂ : succ 1 = 2
ho : o < 1
⊢ Principal (fun x x_1 => x * x_1) 0
[PROOFSTEP]
exact principal_zero
[GOAL]
case inl.inr
h₂ : succ 1 = 2
ho✝ : 1 ≤ 2
ho : 1 ≤ 1
⊢ Principal (fun x x_1 => x * x_1) 1
[PROOFSTEP]
exact principal_mul_one
[GOAL]
case inr
ho : 2 ≤ 2
⊢ Principal (fun x x_1 => x * x_1) 2
[PROOFSTEP]
exact principal_mul_two
[GOAL]
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
⊢ Principal (fun x x_1 => x + x_1) o
[PROOFSTEP]
cases' lt_or_gt_of_ne ho₂ with ho₁ ho₂
[GOAL]
case inl
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ Principal (fun x x_1 => x + x_1) o
[PROOFSTEP]
replace ho₁ : o < succ 1 := by simpa using ho₁
[GOAL]
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ o < succ 1
[PROOFSTEP]
simpa using ho₁
[GOAL]
case inl
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < succ 1
⊢ Principal (fun x x_1 => x + x_1) o
[PROOFSTEP]
rw [lt_succ_iff] at ho₁
[GOAL]
case inl
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o ≤ 1
⊢ Principal (fun x x_1 => x + x_1) o
[PROOFSTEP]
exact principal_add_of_le_one ho₁
[GOAL]
case inr
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
⊢ Principal (fun x x_1 => x + x_1) o
[PROOFSTEP]
refine' fun a b hao hbo => lt_of_le_of_lt _ (ho (max_lt hao hbo) ho₂)
[GOAL]
case inr
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b ≤ (fun x x_1 => x * x_1) (max a b) 2
[PROOFSTEP]
dsimp only
[GOAL]
case inr
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
⊢ a + b ≤ max a b * 2
[PROOFSTEP]
rw [← one_add_one_eq_two, mul_add, mul_one]
[GOAL]
case inr
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
⊢ a + b ≤ max a b + max a b
[PROOFSTEP]
exact add_le_add (le_max_left a b) (le_max_right a b)
[GOAL]
o : Ordinal.{u}
ho₂ : 2 < o
ho : Principal (fun x x_1 => x * x_1) o
⊢ succ 1 < o
[PROOFSTEP]
simpa using ho₂
[GOAL]
o : Ordinal.{u_1}
⊢ Principal (fun x x_1 => x * x_1) o ↔ ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
[PROOFSTEP]
refine' ⟨fun h a ha₀ hao => _, fun h a b hao hbo => _⟩
[GOAL]
case refine'_1
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o
[PROOFSTEP]
cases' le_or_gt o 2 with ho ho
[GOAL]
case refine'_1.inl
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o
[PROOFSTEP]
convert one_mul o
[GOAL]
case h.e'_2.h.e'_5
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case h.e'_2.h.e'_5.a
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1
[PROOFSTEP]
have : a < succ 1 := hao.trans_le (by simpa using ho)
[GOAL]
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ o ≤ succ 1
[PROOFSTEP]
simpa using ho
[GOAL]
case h.e'_2.h.e'_5.a
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
this : a < succ 1
⊢ a ≤ 1
[PROOFSTEP]
rwa [lt_succ_iff] at this
[GOAL]
case h.e'_2.h.e'_5.a
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a
[PROOFSTEP]
rwa [← succ_le_iff, succ_zero] at ha₀
[GOAL]
case refine'_1.inr
o : Ordinal.{u_1}
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal.{u_1}
ha₀ : 0 < a
hao : a < o
ho : o > 2
⊢ a * o = o
[PROOFSTEP]
exact op_eq_self_of_principal hao (mul_isNormal ha₀) h (principal_mul_isLimit ho h)
[GOAL]
case refine'_2
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x * x_1) a b < o
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case refine'_2.inl
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
b : Ordinal.{u_1}
hbo : b < o
hao : 0 < o
⊢ (fun x x_1 => x * x_1) 0 b < o
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2.inl
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
b : Ordinal.{u_1}
hbo : b < o
hao : 0 < o
⊢ 0 * b < o
[PROOFSTEP]
rwa [zero_mul]
[GOAL]
case refine'_2.inr
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ (fun x x_1 => x * x_1) a b < o
[PROOFSTEP]
rw [← Ordinal.pos_iff_ne_zero] at ha
[GOAL]
case refine'_2.inr
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a b < o
[PROOFSTEP]
rw [← h a ha hao]
[GOAL]
case refine'_2.inr
o : Ordinal.{u_1}
h : ∀ (a : Ordinal.{u_1}), 0 < a → a < o → a * o = o
a b : Ordinal.{u_1}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a b < a * o
[PROOFSTEP]
exact (mul_isNormal ha).strictMono hbo
[GOAL]
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x x_1 => x * x_1) ↑m ↑n < ω
[PROOFSTEP]
dsimp only
[GOAL]
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑m * ↑n < ω
[PROOFSTEP]
rw [← nat_cast_mul]
[GOAL]
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
[PROOFSTEP]
apply nat_lt_omega
[GOAL]
a b c : Ordinal.{u_1}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c
[PROOFSTEP]
rcases zero_or_succ_or_limit c with (rfl | ⟨c, rfl⟩ | l)
[GOAL]
case inl
a b : Ordinal.{u_1}
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0
[PROOFSTEP]
exact (lt_irrefl _).elim c0
[GOAL]
case inr.inl.intro
a b : Ordinal.{u_1}
hb : b < ω
c : Ordinal.{u_1}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c
[PROOFSTEP]
rw [opow_succ] at ha
[GOAL]
case inr.inl.intro
a b : Ordinal.{u_1}
hb : b < ω
c : Ordinal.{u_1}
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c
[PROOFSTEP]
rcases((mul_isNormal <| opow_pos _ omega_pos).limit_lt omega_isLimit).1 ha with ⟨n, hn, an⟩
[GOAL]
case inr.inl.intro.intro.intro
a b : Ordinal.{u_1}
hb : b < ω
c : Ordinal.{u_1}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u_1}
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ a * b < ω ^ succ c
[PROOFSTEP]
apply (mul_le_mul_right' (le_of_lt an) _).trans_lt
[GOAL]
case inr.inl.intro.intro.intro
a b : Ordinal.{u_1}
hb : b < ω
c : Ordinal.{u_1}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u_1}
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ (fun x x_1 => x * x_1) (ω ^ c) n * b < ω ^ succ c
[PROOFSTEP]
rw [opow_succ, mul_assoc, mul_lt_mul_iff_left (opow_pos _ omega_pos)]
[GOAL]
case inr.inl.intro.intro.intro
a b : Ordinal.{u_1}
hb : b < ω
c : Ordinal.{u_1}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u_1}
hn : n < ω
an : a < (fun x x_1 => x * x_1) (ω ^ c) n
⊢ n * b < ω
[PROOFSTEP]
exact principal_mul_omega hn hb
[GOAL]
case inr.inr
a b c : Ordinal.{u_1}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
⊢ a * b < ω ^ c
[PROOFSTEP]
rcases((opow_isNormal one_lt_omega).limit_lt l).1 ha with ⟨x, hx, ax⟩
[GOAL]
case inr.inr.intro.intro
a b c : Ordinal.{u_1}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal.{u_1}
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ a * b < ω ^ c
[PROOFSTEP]
refine' (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt _
[GOAL]
case inr.inr.intro.intro
a b c : Ordinal.{u_1}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal.{u_1}
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ (fun x x_1 => x ^ x_1) ω x * ω < ω ^ c
[PROOFSTEP]
rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega]
[GOAL]
case inr.inr.intro.intro
a b c : Ordinal.{u_1}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsLimit c
x : Ordinal.{u_1}
hx : x < c
ax : a < (fun x x_1 => x ^ x_1) ω x
⊢ succ x < c
[PROOFSTEP]
exact l.2 _ hx
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
[PROOFSTEP]
by_cases b0 : b = 0
[GOAL]
case pos
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b = 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
[PROOFSTEP]
rw [b0, opow_zero, opow_one] at h ⊢
[GOAL]
case pos
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω
b0 : b = 0
⊢ a * ω = ω
[PROOFSTEP]
exact mul_omega a0 h
[GOAL]
case neg
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
[PROOFSTEP]
refine' le_antisymm _ (by simpa only [one_mul] using mul_le_mul_right' (one_le_iff_pos.2 a0) (omega ^ omega ^ b))
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b
[PROOFSTEP]
simpa only [one_mul] using mul_le_mul_right' (one_le_iff_pos.2 a0) (omega ^ omega ^ b)
[GOAL]
case neg
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
[PROOFSTEP]
rcases(lt_opow_of_limit omega_ne_zero (opow_isLimit_left omega_isLimit b0)).1 h with ⟨x, xb, ax⟩
[GOAL]
case neg.intro.intro
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
x : Ordinal.{u_1}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b
[PROOFSTEP]
apply (mul_le_mul_right' (le_of_lt ax) _).trans
[GOAL]
case neg.intro.intro
a b : Ordinal.{u_1}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : ¬b = 0
x : Ordinal.{u_1}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
[PROOFSTEP]
rw [← opow_add, add_omega_opow xb]
[GOAL]
o b : Ordinal.{u_1}
hb : 1 < b
ho : Principal (fun x x_1 => x * x_1) (b ^ o)
x y : Ordinal.{u_1}
hx : x < o
hy : y < o
⊢ (fun x x_1 => x + x_1) x y < o
[PROOFSTEP]
have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)
[GOAL]
o b : Ordinal.{u_1}
hb : 1 < b
ho : Principal (fun x x_1 => x * x_1) (b ^ o)
x y : Ordinal.{u_1}
hx : x < o
hy : y < o
this : (fun x x_1 => x * x_1) (b ^ x) (b ^ y) < b ^ o
⊢ (fun x x_1 => x + x_1) x y < o
[PROOFSTEP]
dsimp only at *
[GOAL]
o b : Ordinal.{u_1}
hb : 1 < b
ho : Principal (fun x x_1 => x * x_1) (b ^ o)
x y : Ordinal.{u_1}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
⊢ x + y < o
[PROOFSTEP]
rwa [← opow_add, opow_lt_opow_iff_right hb] at this
[GOAL]
o : Ordinal.{u_1}
⊢ Principal (fun x x_1 => x * x_1) o ↔ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
[PROOFSTEP]
refine' ⟨fun ho => _, _⟩
[GOAL]
case refine'_1
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
[PROOFSTEP]
cases' le_or_lt o 2 with ho₂ ho₂
[GOAL]
case refine'_1.inl
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
[PROOFSTEP]
exact Or.inl ho₂
[GOAL]
case refine'_1.inr
o : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a
[PROOFSTEP]
rcases principal_add_iff_zero_or_omega_opow.1 (principal_add_of_principal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
[GOAL]
case refine'_1.inr.inl
ho : Principal (fun x x_1 => x * x_1) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ ∃ a, 0 = ω ^ ω ^ a
[PROOFSTEP]
exact (Ordinal.not_lt_zero 2 ho₂).elim
[GOAL]
case refine'_1.inr.inr.intro
a : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) (ω ^ a)
ho₂ : 2 < ω ^ a
⊢ ω ^ a ≤ 2 ∨ ∃ a_1, ω ^ a = ω ^ ω ^ a_1
[PROOFSTEP]
rcases principal_add_iff_zero_or_omega_opow.1 (principal_add_of_principal_mul_opow one_lt_omega ho) with
  (rfl | ⟨b, rfl⟩)
[GOAL]
case refine'_1.inr.inr.intro.inl
ho : Principal (fun x x_1 => x * x_1) (ω ^ 0)
ho₂ : 2 < ω ^ 0
⊢ ω ^ 0 ≤ 2 ∨ ∃ a, ω ^ 0 = ω ^ ω ^ a
[PROOFSTEP]
left
[GOAL]
case refine'_1.inr.inr.intro.inl.h
ho : Principal (fun x x_1 => x * x_1) (ω ^ 0)
ho₂ : 2 < ω ^ 0
⊢ ω ^ 0 ≤ 2
[PROOFSTEP]
simpa using one_le_two
[GOAL]
case refine'_1.inr.inr.intro.inr.intro
b : Ordinal.{u_1}
ho : Principal (fun x x_1 => x * x_1) (ω ^ ω ^ b)
ho₂ : 2 < ω ^ ω ^ b
⊢ ω ^ ω ^ b ≤ 2 ∨ ∃ a, ω ^ ω ^ b = ω ^ ω ^ a
[PROOFSTEP]
exact Or.inr ⟨b, rfl⟩
[GOAL]
case refine'_2
o : Ordinal.{u_1}
⊢ (o ≤ 2 ∨ ∃ a, o = ω ^ ω ^ a) → Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
rintro (ho₂ | ⟨a, rfl⟩)
[GOAL]
case refine'_2.inl
o : Ordinal.{u_1}
ho₂ : o ≤ 2
⊢ Principal (fun x x_1 => x * x_1) o
[PROOFSTEP]
exact principal_mul_of_le_two ho₂
[GOAL]
case refine'_2.inr.intro
a : Ordinal.{u_1}
⊢ Principal (fun x x_1 => x * x_1) (ω ^ ω ^ a)
[PROOFSTEP]
exact principal_mul_omega_opow_opow a
[GOAL]
a : Ordinal.{u_1}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u_1}
⊢ a * (ω * b) = ω * b
[PROOFSTEP]
rw [← mul_assoc, mul_omega a0 ha]
[GOAL]
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ a * b = b ^ succ (log b a)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)
[PROOFSTEP]
have hbl := principal_mul_isLimit hb₂ hb
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
⊢ a * b ≤ b ^ succ (log b a)
[PROOFSTEP]
have := IsNormal.bsup_eq.{u, u} (mul_isNormal (Ordinal.pos_iff_ne_zero.2 ha)) hbl
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => (fun x x_2 => x * x_2) a x) = (fun x x_1 => x * x_1) a b
⊢ a * b ≤ b ^ succ (log b a)
[PROOFSTEP]
dsimp at this
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
⊢ a * b ≤ b ^ succ (log b a)
[PROOFSTEP]
rw [← this, bsup_le_iff]
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
⊢ ∀ (i : Ordinal.{u}), i < b → a * i ≤ b ^ succ (log b a)
[PROOFSTEP]
intro c hcb
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
⊢ a * c ≤ b ^ succ (log b a)
[PROOFSTEP]
have hb₁ : 1 < b := (lt_succ 1).trans (by simpa using hb₂)
[GOAL]
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
⊢ succ 1 < b
[PROOFSTEP]
simpa using hb₂
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
⊢ a * c ≤ b ^ succ (log b a)
[PROOFSTEP]
have hbo₀ : (b ^ b.log a) ≠ 0 := Ordinal.pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * c ≤ b ^ succ (log b a)
[PROOFSTEP]
apply le_trans (mul_le_mul_right' (le_of_lt (lt_mul_succ_div a hbo₀)) c)
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
[PROOFSTEP]
rw [mul_assoc, opow_succ]
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
[PROOFSTEP]
refine' mul_le_mul_left' (le_of_lt (hb (hbl.2 _ _) hcb)) _
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b
[PROOFSTEP]
rw [div_lt hbo₀, ← opow_succ]
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
hbl : IsLimit b
this : (bsup b fun x x_1 => a * x) = a * b
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)
[PROOFSTEP]
exact lt_opow_succ_log_self hb₁ _
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b
[PROOFSTEP]
rw [opow_succ]
[GOAL]
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x x_1 => x * x_1) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b
[PROOFSTEP]
exact mul_le_mul_right' (opow_log_le_self b ha) b
[GOAL]
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x x_1 => x ^ x_1) ↑m ↑n < ω
[PROOFSTEP]
simp_rw [← nat_cast_opow]
[GOAL]
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m ^ n) < ω
[PROOFSTEP]
apply nat_lt_omega


[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : f ∈ skewAdjointSubmodule B
hg : g ∈ skewAdjointSubmodule B
⊢ ⁅f, g⁆ ∈ skewAdjointSubmodule B
[PROOFSTEP]
rw [mem_skewAdjointSubmodule] at *
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
⊢ IsSkewAdjoint B ⁅f, g⁆
[PROOFSTEP]
have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hf.mul hg
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
⊢ IsAdjointPair B B (f * g) (g * f)
[PROOFSTEP]
rw [← neg_mul_neg g f]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
⊢ IsAdjointPair B B (f * g) (-g * -f)
[PROOFSTEP]
exact hf.mul hg
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
⊢ IsSkewAdjoint B ⁅f, g⁆
[PROOFSTEP]
have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hg.mul hf
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
⊢ IsAdjointPair B B (g * f) (f * g)
[PROOFSTEP]
rw [← neg_mul_neg f g]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
⊢ IsAdjointPair B B (g * f) (-f * -g)
[PROOFSTEP]
exact hg.mul hf
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
hgf : IsAdjointPair B B (g * f) (f * g)
⊢ IsSkewAdjoint B ⁅f, g⁆
[PROOFSTEP]
change BilinForm.IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
hgf : IsAdjointPair B B (g * f) (f * g)
⊢ IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))
[PROOFSTEP]
rw [neg_sub]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
hgf : IsAdjointPair B B (g * f) (f * g)
⊢ IsAdjointPair B B (f * g - g * f) (g * f - f * g)
[PROOFSTEP]
exact hfg.sub hgf
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ { x // x ∈ skewAdjointLieSubalgebra (comp B ↑e ↑e) } ≃ₗ⁅R⁆ { x // x ∈ skewAdjointLieSubalgebra B }
[PROOFSTEP]
apply LieEquiv.ofSubalgebras _ _ e.lieConj
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ LieSubalgebra.map (LinearEquiv.lieConj e).toLieHom (skewAdjointLieSubalgebra (comp B ↑e ↑e)) =
    skewAdjointLieSubalgebra B
[PROOFSTEP]
ext f
[GOAL]
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ f ∈ LieSubalgebra.map (LinearEquiv.lieConj e).toLieHom (skewAdjointLieSubalgebra (comp B ↑e ↑e)) ↔
    f ∈ skewAdjointLieSubalgebra B
[PROOFSTEP]
simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule, LinearEquiv.coe_coe]
[GOAL]
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ ↑(LinearEquiv.symm (LieEquiv.toLinearEquiv (LinearEquiv.lieConj e))) f ∈
      (skewAdjointLieSubalgebra (comp B ↑e ↑e)).toSubmodule ↔
    f ∈ skewAdjointLieSubalgebra B
[PROOFSTEP]
exact (BilinForm.isPairSelfAdjoint_equiv (-B) B e f).symm
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : { x // x ∈ skewAdjointLieSubalgebra (comp B ↑e ↑e) }
⊢ ↑(↑(skewAdjointLieSubalgebraEquiv B e) f) = ↑(LinearEquiv.lieConj e) ↑f
[PROOFSTEP]
simp [skewAdjointLieSubalgebraEquiv]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : { x // x ∈ skewAdjointLieSubalgebra B }
⊢ ↑(↑(LieEquiv.symm (skewAdjointLieSubalgebraEquiv B e)) f) = ↑(LinearEquiv.lieConj (LinearEquiv.symm e)) ↑f
[PROOFSTEP]
simp [skewAdjointLieSubalgebraEquiv]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
⊢ (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ
[PROOFSTEP]
simp
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : A ∈ skewAdjointMatricesSubmodule J
hB : B ∈ skewAdjointMatricesSubmodule J
⊢ ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
[PROOFSTEP]
simp only [mem_skewAdjointMatricesSubmodule] at *
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ IsSkewAdjoint J ⁅A, B⁆
[PROOFSTEP]
change ⁅A, B⁆ᵀ * J = J * (-⁅A, B⁆)
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
[PROOFSTEP]
change Aᵀ * J = J * (-A) at hA
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hB : IsSkewAdjoint J B
hA : Aᵀ * J = J * -A
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
[PROOFSTEP]
change Bᵀ * J = J * (-B) at hB
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
[PROOFSTEP]
rw [Matrix.lie_transpose, LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket, sub_mul, mul_assoc,
  mul_assoc, hA, hB, ← mul_assoc, ← mul_assoc, hA, hB]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)
[PROOFSTEP]
noncomm_ring
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
⊢ LieSubalgebra.map (LieEquiv.symm (Matrix.lieConj P h)).toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
ext A
[GOAL]
case h
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ A ∈ LieSubalgebra.map (LieEquiv.symm (Matrix.lieConj P h)).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
suffices P.lieConj h A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
  by
  simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule, LinearEquiv.coe_coe]
  exact this
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : ↑(Matrix.lieConj P h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ A ∈ LieSubalgebra.map (LieEquiv.symm (Matrix.lieConj P h)).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule, LinearEquiv.coe_coe]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : ↑(Matrix.lieConj P h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ ↑(LinearEquiv.symm (LieEquiv.toLinearEquiv (LieEquiv.symm (Matrix.lieConj P h)))) A ∈
      (skewAdjointMatricesLieSubalgebra J).toSubmodule ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
exact this
[GOAL]
case h
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ ↑(Matrix.lieConj P h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
[PROOFSTEP]
simp [Matrix.IsSkewAdjoint, J.isAdjointPair_equiv' _ _ P (isUnit_of_invertible P)]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : { x // x ∈ skewAdjointMatricesLieSubalgebra J }
⊢ ↑(↑(skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P
[PROOFSTEP]
simp [skewAdjointMatricesLieSubalgebraEquiv]
[GOAL]
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
⊢ LieSubalgebra.map (AlgEquiv.toLieEquiv e).toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (↑e J)
[PROOFSTEP]
ext A
[GOAL]
case h
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
A : Matrix m m R
⊢ A ∈ LieSubalgebra.map (AlgEquiv.toLieEquiv e).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (↑e J)
[PROOFSTEP]
suffices J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A by
  -- Porting note: Originally `simpa [this]`simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
[GOAL]
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
A : Matrix m m R
this : Matrix.IsSkewAdjoint J (↑(AlgEquiv.symm e) A) ↔ Matrix.IsSkewAdjoint (↑e J) A
⊢ A ∈ LieSubalgebra.map (AlgEquiv.toLieEquiv e).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (↑e J)
[PROOFSTEP]
simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
[GOAL]
case h
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
A : Matrix m m R
⊢ Matrix.IsSkewAdjoint J (↑(AlgEquiv.symm e) A) ↔ Matrix.IsSkewAdjoint (↑e J) A
[PROOFSTEP]
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, ← h, ← Function.Injective.eq_iff e.injective, map_mul,
  AlgEquiv.apply_symm_apply, map_neg]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J
[PROOFSTEP]
change A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
[PROOFSTEP]
simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * J = J * -A → Aᵀ * u • J = u • J * -A
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ * u • J = u • J * -A
⊢ Aᵀ * J = J * -A
[PROOFSTEP]
simpa using congr_arg (fun B => u⁻¹ • B) h
[GOAL]
case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A
[PROOFSTEP]
simp [h]