[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b c d : WithTop α
x y : α
a : WithTop α
⊢ a + ⊤ = ⊤
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y : α
⊢ none + ⊤ = ⊤
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y val✝ : α
⊢ Option.some val✝ + ⊤ = ⊤
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝ : Add α
b c d : WithTop α
x y : α
⊢ none + b = ⊤ ↔ none = ⊤ ∨ b = ⊤
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u
β : Type v
inst✝ : Add α
b c d : WithTop α
x y val✝ : α
⊢ Option.some val✝ + b = ⊤ ↔ Option.some val✝ = ⊤ ∨ b = ⊤
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y : α
⊢ none + none = ⊤ ↔ none = ⊤ ∨ none = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
case none.some
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y val✝ : α
⊢ none + Option.some val✝ = ⊤ ↔ none = ⊤ ∨ Option.some val✝ = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
case some.none
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y val✝ : α
⊢ Option.some val✝ + none = ⊤ ↔ Option.some val✝ = ⊤ ∨ none = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
case some.some
α : Type u
β : Type v
inst✝ : Add α
c d : WithTop α
x y val✝¹ val✝ : α
⊢ Option.some val✝¹ + Option.some val✝ = ⊤ ↔ Option.some val✝¹ = ⊤ ∨ Option.some val✝ = ⊤
[PROOFSTEP]
simp [none_eq_top, some_eq_coe, ← WithTop.coe_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Add α
a✝ b✝ c d : WithTop α
x y : α
inst✝ : LT α
a b : WithTop α
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
[PROOFSTEP]
simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b✝ c✝ d : WithTop α
x y : α
b : WithTop α
c : α
⊢ none + b = ↑c ↔ ∃ a' b', ↑a' = none ∧ ↑b' = b ∧ a' + b' = c
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b c✝ d : WithTop α
x y a c : α
⊢ Option.some a + none = ↑c ↔ ∃ a' b', ↑a' = Option.some a ∧ ↑b' = none ∧ a' + b' = c
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b✝ c✝ d : WithTop α
x y a b c : α
⊢ Option.some a + Option.some b = ↑c ↔ ∃ a' b', ↑a' = Option.some a ∧ ↑b' = Option.some b ∧ a' + b' = c
[PROOFSTEP]
simp only [some_eq_coe, ← coe_add, coe_eq_coe, exists_and_left, exists_eq_left]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x✝ y✝ : α
x : WithTop α
y : α
⊢ x + ↑y = ⊤ ↔ x = ⊤
[PROOFSTEP]
induction x using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y✝ y : α
⊢ ⊤ + ↑y = ⊤ ↔ ⊤ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
case coe
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y✝ y a✝ : α
⊢ ↑a✝ + ↑y = ⊤ ↔ ↑a✝ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y✝ : α
y : WithTop α
⊢ ↑x + y = ⊤ ↔ y = ⊤
[PROOFSTEP]
induction y using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y : α
⊢ ↑x + ⊤ = ⊤ ↔ ⊤ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
case coe
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithTop α
x y a✝ : α
⊢ ↑x + ↑a✝ = ⊤ ↔ ↑a✝ = ⊤
[PROOFSTEP]
simp [← coe_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Add α
a b c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
ha : a ≠ ⊤
⊢ b + a = c + a ↔ b = c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a : α
⊢ b + ↑a = c + ↑a ↔ b = c
[PROOFSTEP]
obtain rfl | hb := (eq_or_ne b ⊤)
[GOAL]
case intro.inl
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a : α
⊢ ⊤ + ↑a = c + ↑a ↔ ⊤ = c
[PROOFSTEP]
rw [top_add, eq_comm, WithTop.add_coe_eq_top_iff, eq_comm]
[GOAL]
case intro.inr
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a : α
hb : b ≠ ⊤
⊢ b + ↑a = c + ↑a ↔ b = c
[PROOFSTEP]
lift b to α using hb
[GOAL]
case intro.inr.intro
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsRightCancelAdd α
a b : α
⊢ ↑b + ↑a = c + ↑a ↔ ↑b = c
[PROOFSTEP]
simp_rw [← WithTop.coe_add, eq_comm, WithTop.add_eq_coe, coe_eq_coe, exists_and_left, exists_eq_left, add_left_inj,
  exists_eq_right, eq_comm]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Add α
a b c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
ha : a ≠ ⊤
⊢ a + b = a + c ↔ b = c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a : α
⊢ ↑a + b = ↑a + c ↔ b = c
[PROOFSTEP]
obtain rfl | hb := (eq_or_ne b ⊤)
[GOAL]
case intro.inl
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a : α
⊢ ↑a + ⊤ = ↑a + c ↔ ⊤ = c
[PROOFSTEP]
rw [add_top, eq_comm, WithTop.coe_add_eq_top_iff, eq_comm]
[GOAL]
case intro.inr
α : Type u
β : Type v
inst✝¹ : Add α
b c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a : α
hb : b ≠ ⊤
⊢ ↑a + b = ↑a + c ↔ b = c
[PROOFSTEP]
lift b to α using hb
[GOAL]
case intro.inr.intro
α : Type u
β : Type v
inst✝¹ : Add α
c d : WithTop α
x y : α
inst✝ : IsLeftCancelAdd α
a b : α
⊢ ↑a + ↑b = ↑a + c ↔ ↑b = c
[PROOFSTEP]
simp_rw [← WithTop.coe_add, eq_comm, WithTop.add_eq_coe, eq_comm, coe_eq_coe, exists_and_left, exists_eq_left',
  add_right_inj, exists_eq_right']
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : WithTop α
h : b ≤ c
⊢ a + b ≤ a + c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
⊢ none + b ≤ none + c
[PROOFSTEP]
cases c
[GOAL]
case some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
val✝ : α
⊢ Option.some val✝ + b ≤ Option.some val✝ + c
[PROOFSTEP]
cases c
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ none + b ≤ none + none
[PROOFSTEP]
try exact le_top
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ none + b ≤ none + none
[PROOFSTEP]
exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ none + b ≤ none + Option.some val✝
[PROOFSTEP]
try exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ none + b ≤ none + Option.some val✝
[PROOFSTEP]
exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ Option.some val✝ + b ≤ Option.some val✝ + none
[PROOFSTEP]
try exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ Option.some val✝ + b ≤ Option.some val✝ + none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ Option.some val✝¹ + b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
try exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ Option.some val✝¹ + b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ Option.some val✝¹ + b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
rcases le_coe_iff.1 h with ⟨b, rfl, _⟩
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
val✝¹ val✝ b : α
right✝ : b ≤ val✝
h : ↑b ≤ Option.some val✝
⊢ Option.some val✝¹ + ↑b ≤ Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
exact coe_le_coe.2 (add_le_add_left (coe_le_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : WithTop α
h : b ≤ c
⊢ swap (fun x x_1 => x + x_1) a b ≤ swap (fun x x_1 => x + x_1) a c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none c
[PROOFSTEP]
cases c
[GOAL]
case some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : WithTop α
h : b ≤ c
val✝ : α
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝) c
[PROOFSTEP]
cases c
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none none
[PROOFSTEP]
try exact le_top
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none none
[PROOFSTEP]
exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none (Option.some val✝)
[PROOFSTEP]
try exact le_top
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) none b ≤ swap (fun x x_1 => x + x_1) none (Option.some val✝)
[PROOFSTEP]
exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝) none
[PROOFSTEP]
try exact le_top
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝ : α
h : b ≤ none
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝) none
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
try exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
exact le_top
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b : WithTop α
val✝¹ val✝ : α
h : b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) b ≤ swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
rcases le_coe_iff.1 h with ⟨b, rfl, _⟩
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
val✝¹ val✝ b : α
right✝ : b ≤ val✝
h : ↑b ≤ Option.some val✝
⊢ swap (fun x x_1 => x + x_1) (Option.some val✝¹) ↑b ≤
    swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝)
[PROOFSTEP]
exact coe_le_coe.2 (add_le_add_right (coe_le_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b c : WithTop α
h : a + b < a + c
⊢ b < c
[PROOFSTEP]
induction a using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
h : ⊤ + b < ⊤ + c
⊢ b < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case coe
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
a✝ : α
h : ↑a✝ + b < ↑a✝ + c
⊢ b < c
[PROOFSTEP]
induction b using WithTop.recTopCoe
[GOAL]
case coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
a✝ : α
h : ↑a✝ + ⊤ < ↑a✝ + c
⊢ ⊤ < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
a✝¹ a✝ : α
h : ↑a✝¹ + ↑a✝ < ↑a✝¹ + c
⊢ ↑a✝ < c
[PROOFSTEP]
induction c using WithTop.recTopCoe
[GOAL]
case coe.coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a✝¹ a✝ : α
h : ↑a✝¹ + ↑a✝ < ↑a✝¹ + ⊤
⊢ ↑a✝ < ⊤
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a✝² a✝¹ a✝ : α
h : ↑a✝² + ↑a✝¹ < ↑a✝² + ↑a✝
⊢ ↑a✝¹ < ↑a✝
[PROOFSTEP]
exact coe_lt_coe.2 (lt_of_add_lt_add_left <| coe_lt_coe.1 h)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b c : WithTop α
h : swap (fun x x_1 => x + x_1) a b < swap (fun x x_1 => x + x_1) a c
⊢ b < c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
h : swap (fun x x_1 => x + x_1) none b < swap (fun x x_1 => x + x_1) none c
⊢ b < c
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u
β : Type v
inst✝² : Add α
a b✝ c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
b c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) (Option.some val✝) b < swap (fun x x_1 => x + x_1) (Option.some val✝) c
⊢ b < c
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
h : swap (fun x x_1 => x + x_1) none none < swap (fun x x_1 => x + x_1) none c
⊢ none < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case none.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
h : swap (fun x x_1 => x + x_1) none none < swap (fun x x_1 => x + x_1) none c
⊢ none < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) none (Option.some val✝) < swap (fun x x_1 => x + x_1) none c
⊢ Option.some val✝ < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case none.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) none (Option.some val✝) < swap (fun x x_1 => x + x_1) none c
⊢ Option.some val✝ < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) (Option.some val✝) none < swap (fun x x_1 => x + x_1) (Option.some val✝) c
⊢ none < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case some.none
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝ : α
h : swap (fun x x_1 => x + x_1) (Option.some val✝) none < swap (fun x x_1 => x + x_1) (Option.some val✝) c
⊢ none < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) < swap (fun x x_1 => x + x_1) (Option.some val✝¹) c
⊢ Option.some val✝ < c
[PROOFSTEP]
try exact (not_none_lt _ h).elim
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) < swap (fun x x_1 => x + x_1) (Option.some val✝¹) c
⊢ Option.some val✝ < c
[PROOFSTEP]
exact (not_none_lt _ h).elim
[GOAL]
case some.some
α : Type u
β : Type v
inst✝² : Add α
a b c✝ d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
c : WithTop α
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) < swap (fun x x_1 => x + x_1) (Option.some val✝¹) c
⊢ Option.some val✝ < c
[PROOFSTEP]
cases c
[GOAL]
case some.some.none
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝¹) (Option.some val✝) <
    swap (fun x x_1 => x + x_1) (Option.some val✝¹) none
⊢ Option.some val✝ < none
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case some.some.some
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
val✝² val✝¹ val✝ : α
h :
  swap (fun x x_1 => x + x_1) (Option.some val✝²) (Option.some val✝¹) <
    swap (fun x x_1 => x + x_1) (Option.some val✝²) (Option.some val✝)
⊢ Option.some val✝¹ < Option.some val✝
[PROOFSTEP]
exact coe_lt_coe.2 (lt_of_add_lt_add_right <| coe_lt_coe.1 h)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
ha : a ≠ ⊤
h : a + b ≤ a + c
⊢ b ≤ c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : ↑a + b ≤ ↑a + c
⊢ b ≤ c
[PROOFSTEP]
induction c using WithTop.recTopCoe
[GOAL]
case intro.top
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : α
h : ↑a + b ≤ ↑a + ⊤
⊢ b ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case intro.coe
α : Type u
β : Type v
inst✝² : Add α
b d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝ : α
h : ↑a + b ≤ ↑a + ↑a✝
⊢ b ≤ ↑a✝
[PROOFSTEP]
induction b using WithTop.recTopCoe
[GOAL]
case intro.coe.top
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝ : α
h : ↑a + ⊤ ≤ ↑a + ↑a✝
⊢ ⊤ ≤ ↑a✝
[PROOFSTEP]
exact (not_top_le_coe _ h).elim
[GOAL]
case intro.coe.coe
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝¹ a✝ : α
h : ↑a + ↑a✝ ≤ ↑a + ↑a✝¹
⊢ ↑a✝ ≤ ↑a✝¹
[PROOFSTEP]
simp only [← coe_add, coe_le_coe] at h ⊢
[GOAL]
case intro.coe.coe
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a a✝¹ a✝ : α
h : a + a✝ ≤ a + a✝¹
⊢ a✝ ≤ a✝¹
[PROOFSTEP]
exact le_of_add_le_add_left h
[GOAL]
α : 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
[PROOFSTEP]
lift a to α using ha
[GOAL]
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
[PROOFSTEP]
cases c
[GOAL]
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
[PROOFSTEP]
exact le_top
[GOAL]
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✝
[PROOFSTEP]
cases b
[GOAL]
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✝
[PROOFSTEP]
exact (not_top_le_coe _ h).elim
[GOAL]
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✝¹
[PROOFSTEP]
exact coe_le_coe.2 (le_of_add_le_add_right <| coe_le_coe.1 h)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
ha : a ≠ ⊤
h : b < c
⊢ a + b < a + c
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : Add α
b c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : b < c
a : α
⊢ ↑a + b < ↑a + c
[PROOFSTEP]
rcases lt_iff_exists_coe.1 h with ⟨b, rfl, h'⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
inst✝² : Add α
c d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < c
⊢ ↑a + ↑b < ↑a + c
[PROOFSTEP]
cases c
[GOAL]
case intro.intro.intro.none
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : α
h' h : ↑b < none
⊢ ↑a + ↑b < ↑a + none
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
case intro.intro.intro.some
α : Type u
β : Type v
inst✝² : Add α
d : WithTop α
x y : α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b val✝ : α
h' h : ↑b < Option.some val✝
⊢ ↑a + ↑b < ↑a + Option.some val✝
[PROOFSTEP]
exact coe_lt_coe.2 (add_lt_add_left (coe_lt_coe.1 h) _)
[GOAL]
α : 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
[PROOFSTEP]
lift a to α using ha
[GOAL]
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
[PROOFSTEP]
rcases lt_iff_exists_coe.1 h with ⟨b, rfl, h'⟩
[GOAL]
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
[PROOFSTEP]
cases c
[GOAL]
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
[PROOFSTEP]
exact coe_lt_top _
[GOAL]
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
[PROOFSTEP]
exact coe_lt_coe.2 (add_lt_add_right (coe_lt_coe.1 h) _)
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a✝ b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (↑f) (a + b) = map (↑f) a + map (↑f) b
[PROOFSTEP]
induction a using WithTop.recTopCoe
[GOAL]
case top
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (↑f) (⊤ + b) = map ↑f ⊤ + map (↑f) b
[PROOFSTEP]
exact (top_add _).symm
[GOAL]
case coe
α : Type u
β : Type v
inst✝² : Add α
a b✝ c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (↑f) (↑a✝ + b) = map ↑f ↑a✝ + map (↑f) b
[PROOFSTEP]
induction b using WithTop.recTopCoe
[GOAL]
case coe.top
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (↑f) (↑a✝ + ⊤) = map ↑f ↑a✝ + map ↑f ⊤
[PROOFSTEP]
exact (add_top _).symm
[GOAL]
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (↑f) (↑a✝¹ + ↑a✝) = map ↑f ↑a✝¹ + map ↑f ↑a✝
[PROOFSTEP]
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
[GOAL]
case coe.coe
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithTop α
x y : α
F : Type u_1
inst✝¹ : Add β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ↑f ↑(a✝¹ + a✝) = ↑(↑f (a✝¹ + a✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp only
  -- Porting note: Had to add this...?
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
⊢ ↑↑0 = 0
[PROOFSTEP]
rw [Nat.cast_zero, WithTop.coe_zero]
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp only
  -- Porting note: Had to add this...?
[GOAL]
α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
src✝¹ : One (WithTop α) := one
src✝ : AddMonoid (WithTop α) := addMonoid
n : ℕ
⊢ ↑↑(n + 1) = ↑↑n + 1
[PROOFSTEP]
rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one]
[GOAL]
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
⊢ ∀ (a b : WithTop α), a ≤ b → ∀ (c : WithTop α), c + a ≤ c + b
[PROOFSTEP]
rintro a b h (_ | c)
[GOAL]
case none
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a b : WithTop α
h : a ≤ b
⊢ none + a ≤ none + b
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
case some
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a b : WithTop α
h : a ≤ b
c : α
⊢ Option.some c + a ≤ Option.some c + b
[PROOFSTEP]
rcases b with (_ | b)
[GOAL]
case some.none
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a : WithTop α
c : α
h : a ≤ none
⊢ Option.some c + a ≤ Option.some c + none
[PROOFSTEP]
simp [none_eq_top]
[GOAL]
case some.some
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
a : WithTop α
c b : α
h : a ≤ Option.some b
⊢ Option.some c + a ≤ Option.some c + Option.some b
[PROOFSTEP]
rcases le_coe_iff.1 h with ⟨a, rfl, _⟩
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
c b a : α
right✝ : a ≤ b
h : ↑a ≤ Option.some b
⊢ Option.some c + ↑a ≤ Option.some c + Option.some b
[PROOFSTEP]
simp only [some_eq_coe, ← coe_add, coe_le_coe] at h ⊢
[GOAL]
case some.some.intro.intro
α : Type u
β : Type v
inst✝ : OrderedAddCommMonoid α
src✝¹ : PartialOrder (WithTop α) := partialOrder
src✝ : AddCommMonoid (WithTop α) := addCommMonoid
c b a : α
right✝ h : a ≤ b
⊢ c + a ≤ c + b
[PROOFSTEP]
exact add_le_add_left h c
[GOAL]
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a b : WithTop α
⊢ ⊤ ≤ ⊤ → ∃ c, ⊤ = ⊤ + c
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b✝ : WithTop α
a b : α
h : ↑a ≤ ↑b
⊢ ∃ c, ↑b = ↑a + c
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)
[GOAL]
case intro
α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ b : WithTop α
a c : α
h : ↑a ≤ ↑(a + c)
⊢ ∃ c_1, ↑(a + c) = ↑a + c_1
[PROOFSTEP]
exact ⟨c, rfl⟩
[GOAL]
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (↑f) 1 = 1
[PROOFSTEP]
rw [WithTop.map_one, map_one, coe_one]
[GOAL]
α : Type u
β : Type v
inst✝ : Add α
a✝ b c d : WithBot α
x y : α
a : WithBot α
⊢ a + ⊥ = ⊥
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithBot α
x y : α
⊢ none + ⊥ = ⊥
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
β : Type v
inst✝ : Add α
a b c d : WithBot α
x y val✝ : α
⊢ Option.some val✝ + ⊥ = ⊥
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝² : Add α
a b c d : WithBot α
x y : α
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (↑f) 1 = 1
[PROOFSTEP]
rw [WithBot.map_one, map_one, coe_one]
