case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : b < c
a : α
⊢ b + ↑a < c + ↑a
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
ha : a ≠ ⊤
h : b < c
⊢ b + a < c + a
lift a to α using ha
case intro.intro.intro
α : Type u
β : Type v
inst✝² : Add α
c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < c
⊢ ↑b + ↑a < c + ↑a
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : b < c
a : α
⊢ b + ↑a < c + ↑a
rcases lt_iff_exists_coe.1 h with ⟨b, rfl, h'⟩
case intro.intro.intro.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < none
⊢ ↑b + ↑a < none + ↑a

case intro.intro.intro.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b val✝ : α
h' h : ↑b < Option.some val✝
⊢ ↑b + ↑a < Option.some val✝ + ↑a
case intro.intro.intro
α : Type u
β : Type v
inst✝² : Add α
c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < c
⊢ ↑b + ↑a < c + ↑a
cases c
no goals
case intro.intro.intro.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < none
⊢ ↑b + ↑a < none + ↑a
exact coe_lt_top _
no goals
case intro.intro.intro.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b val✝ : α
h' h : ↑b < Option.some val✝
⊢ ↑b + ↑a < Option.some val✝ + ↑a
exact coe_lt_coe.2 (add_lt_add_right (coe_lt_coe.1 h) _)