-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_add_div_mul {a c : Ordinal} (hc : c < a) (b d : Ordinal) :
    (a * b + c) / (a * d) = b / d

Proof state:
case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) = b / d

Tactic:
apply le_antisymm

Result:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) ≤ b / d

case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)

Proof state:
case inr.a.bc
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)

Tactic:
exact lt_mul_succ_div b hd

Result:
no goals

Proof state:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) ≤ b / d

Tactic:
rw [← lt_succ_iff, div_lt H, mul_assoc]

Result:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))

Proof state:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))

Tactic:
apply (add_lt_add_left hc _).trans_le

Result:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + a ≤ a * (d * succ (b / d))

Proof state:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))

Tactic:
apply mul_le_mul_left'

Result:
case inr.a.bc
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ succ b ≤ d * succ (b / d)

Proof state:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)

Tactic:
rw [le_div H, mul_assoc]

Result:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * (d * (b / d)) ≤ a * b + c

Proof state:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + a ≤ a * (d * succ (b / d))

Tactic:
rw [← mul_succ]

Result:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))

Proof state:
case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
ha : a ≠ 0
⊢ (a * b + c) / (a * 0) = b / 0

Tactic:
rw [mul_zero, div_zero, div_zero]

Result:
no goals

Proof state:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * (d * (b / d)) ≤ a * b + c

Tactic:
exact (mul_le_mul_left' (mul_div_le b d) a).trans (le_add_right _ c)

Result:
no goals

Proof state:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
⊢ (a * b + c) / (a * d) = b / d

Tactic:
have ha : a ≠ 0 := ((Ordinal.zero_le c).trans_lt hc).ne'

Result:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
⊢ (a * b + c) / (a * d) = b / d

Proof state:
case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
⊢ (a * b + c) / (a * d) = b / d

Tactic:
have H := mul_ne_zero ha hd

Result:
case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) = b / d

Proof state:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
⊢ (a * b + c) / (a * d) = b / d

Tactic:
obtain rfl | hd := eq_or_ne d 0

Result:
case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
ha : a ≠ 0
⊢ (a * b + c) / (a * 0) = b / 0

case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
⊢ (a * b + c) / (a * d) = b / d

Proof state:
case inr.a.bc
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ succ b ≤ d * succ (b / d)

Tactic:
rw [succ_le_iff]

Result:
case inr.a.bc
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
ha : a ≠ 0
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)