-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_mul_of_principal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b ≠ 1)
    (hb : Principal (· + ·) b) : Principal (· + ·) (a * b)

Proof state:
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) (a * 0)

Tactic:
rw [mul_zero]

Result:
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) 0

Proof state:
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) 0

Tactic:
exact principal_zero

Result:
no goals

Proof state:
case inr.inr.intro.intro
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hd : ∃ c' < b, d < a * c'
x : Ordinal.{u}
hx : x < b
hx' : c < a * x
⊢ ∃ c' < b, (fun x1 x2 => x1 + x2) c d < a * c'

Tactic:
rcases hd with ⟨y, hy, hy'⟩

Result:
case inr.inr.intro.intro.intro.intro
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
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' < b, (fun x1 x2 => x1 + x2) c d < a * c'

Proof state:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
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 x1 x2 => x1 + x2) c d < a * (x + y)

Tactic:
rw [mul_add]

Result:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
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 x1 x2 => x1 + x2) c d < a * x + a * y

Proof state:
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
⊢ Principal (fun x1 x2 => x1 + x2) (0 * b)

Tactic:
rw [zero_mul]

Result:
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
⊢ Principal (fun x1 x2 => x1 + x2) 0

Proof state:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
⊢ ∃ c' < b, (fun x1 x2 => x1 + x2) c d < a * c'

Tactic:
rcases hc with ⟨x, hx, hx'⟩

Result:
case inr.inr.intro.intro
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hd : ∃ c' < b, d < a * c'
x : Ordinal.{u}
hx : x < b
hx' : c < a * x
⊢ ∃ c' < b, (fun x1 x2 => x1 + x2) c d < a * c'

Proof state:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Tactic:
intro c d hc hd

Result:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : c < a * b
hd : d < a * b
⊢ (fun x1 x2 => x1 + x2) c d < a * b

Proof state:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
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 x1 x2 => x1 + x2) c d < a * x + a * y

Tactic:
exact Left.add_lt_add hx' hy'

Result:
no goals

Proof state:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 0 < b
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Tactic:
rw [← succ_le_iff, succ_zero] at hb₁'

Result:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Proof state:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : c < a * b
hd : d < a * b
⊢ (fun x1 x2 => x1 + x2) c d < a * b

Tactic:
rw [lt_mul_of_limit (isLimit_of_principal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *

Result:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
⊢ ∃ c' < b, (fun x1 x2 => x1 + x2) c d < a * c'

Proof state:
case inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Tactic:
rcases eq_zero_or_pos b with (rfl | hb₁')

Result:
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) 0
⊢ Principal (fun x1 x2 => x1 + x2) (a * 0)

case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
hb₁' : 0 < b
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Proof state:
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
⊢ Principal (fun x1 x2 => x1 + x2) 0

Tactic:
exact principal_zero

Result:
no goals

Proof state:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Tactic:
rcases eq_zero_or_pos a with (rfl | _)

Result:
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
⊢ Principal (fun x1 x2 => x1 + x2) (0 * b)

case inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
⊢ Principal (fun x1 x2 => x1 + x2) (a * b)

Proof state:
case inr.inr.intro.intro.intro.intro
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
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' < b, (fun x1 x2 => x1 + x2) c d < a * c'

Tactic:
use x + y, hb hx hy

Result:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : Principal (fun x1 x2 => x1 + x2) b
h✝ : 0 < a
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 x1 x2 => x1 + x2) c d < a * (x + y)