case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : b + ↑a ≤ c + ↑a
⊢ b ≤ c
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
ha : a ≠ ⊤
h : b + a ≤ c + a
⊢ b ≤ c
lift a to α using ha
case intro.none
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : b + ↑a ≤ none + ↑a
⊢ b ≤ none

case intro.some
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝ : α
h : b + ↑a ≤ Option.some val✝ + ↑a
⊢ b ≤ Option.some val✝
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : b + ↑a ≤ c + ↑a
⊢ b ≤ c
cases c
no goals
case intro.none
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : b + ↑a ≤ none + ↑a
⊢ b ≤ none
exact le_top
case intro.some.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝ : α
h : none + ↑a ≤ Option.some val✝ + ↑a
⊢ none ≤ Option.some val✝

case intro.some.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝¹ val✝ : α
h : Option.some val✝ + ↑a ≤ Option.some val✝¹ + ↑a
⊢ Option.some val✝ ≤ Option.some val✝¹
case intro.some
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝ : α
h : b + ↑a ≤ Option.some val✝ + ↑a
⊢ b ≤ Option.some val✝
cases b
no goals
case intro.some.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝ : α
h : none + ↑a ≤ Option.some val✝ + ↑a
⊢ none ≤ Option.some val✝
exact (not_top_le_coe _ h).elim
no goals
case intro.some.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a val✝¹ val✝ : α
h : Option.some val✝ + ↑a ≤ Option.some val✝¹ + ↑a
⊢ Option.some val✝ ≤ Option.some val✝¹
exact coe_le_coe.2 (le_of_add_le_add_right <| coe_le_coe.1 h)