[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a : WithTop α
⊢ a - ⊤ = 0
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
⊢ none - ⊤ = 0
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
val✝ : α
⊢ Option.some val✝ - ⊤ = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
induction a using recTopCoe
[GOAL]
case top
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
b : WithTop α
⊢ ⊤ - b = ⊤ ↔ ⊤ = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
induction b using recTopCoe
[GOAL]
case coe
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
b : WithTop α
a✝ : α
⊢ ↑a✝ - b = ⊤ ↔ ↑a✝ = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
induction b using recTopCoe
[GOAL]
case top.top
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∧ ⊤ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
case top.coe
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a✝ : α
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∧ ↑a✝ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
case coe.top
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Zero α
inst✝¹ : Sub β
inst✝ : Zero β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f 0 = 0
x✝ : WithTop α
⊢ map f (x✝ - ⊤) = map f x✝ - map f ⊤
[PROOFSTEP]
simp only [h₀, sub_top, WithTop.map_zero, coe_zero, map_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Zero α
inst✝¹ : Sub β
inst✝ : Zero β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f 0 = 0
x y : α
⊢ map f (↑x - ↑y) = map f ↑x - map f ↑y
[PROOFSTEP]
simp only [← coe_sub, map_coe, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ OrderedSub (WithTop α)
[PROOFSTEP]
constructor
[GOAL]
case tsub_le_iff_right
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ ∀ (a b c : WithTop α), a - b ≤ c ↔ a ≤ c + b
[PROOFSTEP]
rintro x y z
[GOAL]
case tsub_le_iff_right
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y z : WithTop α
⊢ x - y ≤ z ↔ x ≤ z + y
[PROOFSTEP]
induction y using WithTop.recTopCoe
[GOAL]
case tsub_le_iff_right.top
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
a✝ : α
⊢ x - ↑a✝ ≤ z ↔ x ≤ z + ↑a✝
[PROOFSTEP]
induction x using WithTop.recTopCoe
[GOAL]
case tsub_le_iff_right.coe.top
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝ : α
⊢ ⊤ - ↑a✝ ≤ z ↔ ⊤ ≤ z + ↑a✝
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.coe.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ z ↔ ↑a✝ ≤ z + ↑a✝¹
[PROOFSTEP]
induction z using WithTop.recTopCoe
[GOAL]
case tsub_le_iff_right.coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ ⊤ ↔ ↑a✝ ≤ ⊤ + ↑a✝¹
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝² a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝² ≤ ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ + ↑a✝²
[PROOFSTEP]
norm_cast
[GOAL]
case tsub_le_iff_right.coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝² a✝¹ a✝ : α
⊢ a✝¹ - a✝² ≤ a✝ ↔ a✝¹ ≤ a✝ + a✝²
[PROOFSTEP]
exact tsub_le_iff_right
