case inl
b : Ordinal
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) (0 * b)

case inr
a b : Ordinal
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)
a b : Ordinal
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) (a * b)
rcases eq_zero_or_pos a with (rfl | _)
case inl
b : Ordinal
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) 0
case inl
b : Ordinal
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) (0 * b)
rw [zero_mul]
no goals
case inl
b : Ordinal
hb₁ : b ≠ 1
hb : Principal (fun x x_1 => x + x_1) b
⊢ Principal (fun x x_1 => x + x_1) 0
exact principal_zero
case inr.inl
a : Ordinal
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)

case inr.inr
a b : Ordinal
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)
case inr
a b : Ordinal
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)
rcases eq_zero_or_pos b with (rfl | hb₁')
case inr.inl
a : Ordinal
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
case inr.inl
a : Ordinal
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)
rw [mul_zero]
no goals
case inr.inl
a : Ordinal
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
exact principal_zero
case inr.inr
a b : Ordinal
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)
case inr.inr
a b : Ordinal
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)
rw [← succ_le_iff, succ_zero] at hb₁'
case inr.inr
a b : Ordinal
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
hc : c < a * b
hd : d < a * b
⊢ (fun x x_1 => x + x_1) c d < a * b
case inr.inr
a b : Ordinal
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)
intro c d hc hd
case inr.inr
a b : Ordinal
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
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'
case inr.inr
a b : Ordinal
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
hc : c < a * b
hd : d < a * b
⊢ (fun x x_1 => x + x_1) c d < a * b
rw [lt_mul_of_limit (principal_add_isLimit (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
case inr.inr.intro.intro
a b : Ordinal
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
hd : ∃ c', c' < b ∧ d < a * c'
x : Ordinal
hx : x < b
hx' : c < a * x
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
case inr.inr
a b : Ordinal
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
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'
rcases hc with ⟨x, hx, hx'⟩
case inr.inr.intro.intro.intro.intro
a b : Ordinal
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
hx : x < b
hx' : c < a * x
y : Ordinal
hy : y < b
hy' : d < a * y
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
case inr.inr.intro.intro
a b : Ordinal
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
hd : ∃ c', c' < b ∧ d < a * c'
x : Ordinal
hx : x < b
hx' : c < a * x
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
rcases hd with ⟨y, hy, hy'⟩
case inr.inr.intro.intro.intro.intro
a b : Ordinal
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
hx : x < b
hx' : c < a * x
y : Ordinal
hy : y < b
hy' : d < a * y
⊢ (fun x x_1 => x + x_1) c d < a * (x + y)
case inr.inr.intro.intro.intro.intro
a b : Ordinal
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
hx : x < b
hx' : c < a * x
y : Ordinal
hy : y < b
hy' : d < a * y
⊢ ∃ c', c' < b ∧ (fun x x_1 => x + x_1) c d < a * c'
use x + y, hb hx hy
case inr.inr.intro.intro.intro.intro
a b : Ordinal
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
hx : x < b
hx' : c < a * x
y : Ordinal
hy : y < b
hy' : d < a * y
⊢ (fun x x_1 => x + x_1) c d < a * x + a * y
case inr.inr.intro.intro.intro.intro
a b : Ordinal
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
hx : x < b
hx' : c < a * x
y : Ordinal
hy : y < b
hy' : d < a * y
⊢ (fun x x_1 => x + x_1) c d < a * (x + y)
rw [mul_add]
no goals
case inr.inr.intro.intro.intro.intro
a b : Ordinal
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
hx : x < b
hx' : c < a * x
y : Ordinal
hy : y < b
hy' : d < a * y
⊢ (fun x x_1 => x + x_1) c d < a * x + a * y
exact Left.add_lt_add hx' hy'