Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
Ported by: Jon Eugster
! This file was ported from Lean 3 source module algebra.order.monoid.with_top
! leanprover-community/mathlib commit 0111834459f5d7400215223ea95ae38a1265a907
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Group
import Mathlib.Algebra.Order.Monoid.OrderDual
import Mathlib.Algebra.Order.Monoid.WithZero.Basic
import Mathlib.Data.Nat.Cast.Defs
import Mathlib.Algebra.Order.ZeroLEOne
/-! # Adjoining top/bottom elements to ordered monoids.
-/
universe u v
variable { α : Type u } { β : Type v }
open Function
namespace WithTop
section One
variable [ One α ]
@[ to_additive ]
instance one : One ( WithTop α ) :=
⟨( 1 : α )⟩
#align with_top.has_one WithTop.one
#align with_top.has_zero WithTop.zero
@[ to_additive : ∀ {α : Type u} [inst : Zero α ↑0 = 0 to_additive ( attr := simp , norm_cast )]
theorem coe_one : ∀ {α : Type u} [inst : One α ↑1 = 1 coe_one : (( 1 : α ) : WithTop α ) = 1 :=
rfl : ∀ {α : Sort ?u.375} {a : α }, a = a
#align with_top.coe_one WithTop.coe_one : ∀ {α : Type u} [inst : One α ↑1 = 1
#align with_top.coe_zero WithTop.coe_zero : ∀ {α : Type u} [inst : Zero α ↑0 = 0
@[ to_additive : ∀ {α : Type u} [inst : Zero α a : α }, ↑a = 0 ↔ a = 0 to_additive ( attr := simp , norm_cast )]
theorem coe_eq_one : ∀ {α : Type u} [inst : One α a : α }, ↑a = 1 ↔ a = 1 coe_eq_one { a : α } : ( a : WithTop α ) = 1 ↔ a = 1 :=
coe_eq_coe : ∀ {α : Type ?u.663} {a b : α }, ↑a = ↑b ↔ a = b
#align with_top.coe_eq_one WithTop.coe_eq_one : ∀ {α : Type u} [inst : One α a : α }, ↑a = 1 ↔ a = 1
#align with_top.coe_eq_zero WithTop.coe_eq_zero : ∀ {α : Type u} [inst : Zero α a : α }, ↑a = 0 ↔ a = 0
@[ to_additive ( attr := simp )]
theorem untop_one : ( 1 : WithTop α ). untop coe_ne_top : ∀ {α : Type ?u.961} {a : α }, ↑a ≠ ⊤ = 1 :=
rfl : ∀ {α : Sort ?u.1004} {a : α }, a = a
#align with_top.untop_one WithTop.untop_one
#align with_top.untop_zero WithTop.untop_zero
@[ to_additive ( attr := simp )]
theorem untop_one' : ∀ (d : α ), untop' d 1 = 1 untop_one' ( d : α ) : ( 1 : WithTop α ). untop' d = 1 :=
rfl : ∀ {α : Sort ?u.1149} {a : α }, a = a
#align with_top.untop_one' WithTop.untop_one' : ∀ {α : Type u} [inst : One α d : α ), untop' d 1 = 1
#align with_top.untop_zero' WithTop.untop_zero' : ∀ {α : Type u} [inst : Zero α d : α ), untop' d 0 = 0
@[ to_additive ( attr := simp , norm_cast ) coe_nonneg : ∀ {α : Type u} [inst : Zero α inst_1 : LE α a : α }, 0 ≤ ↑a ↔ 0 ≤ a ]
theorem one_le_coe : ∀ [inst : LE α a : α }, 1 ≤ ↑a ↔ 1 ≤ a one_le_coe [ LE α ] { a : α } : 1 ≤ ( a : WithTop α ) ↔ 1 ≤ a :=
coe_le_coe : ∀ {α : Type ?u.1665} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b
#align with_top.one_le_coe WithTop.one_le_coe : ∀ {α : Type u} [inst : One α inst_1 : LE α a : α }, 1 ≤ ↑a ↔ 1 ≤ a
#align with_top.coe_nonneg WithTop.coe_nonneg : ∀ {α : Type u} [inst : Zero α inst_1 : LE α a : α }, 0 ≤ ↑a ↔ 0 ≤ a
@[ to_additive ( attr := simp , norm_cast ) coe_le_zero : ∀ {α : Type u} [inst : Zero α inst_1 : LE α a : α }, ↑a ≤ 0 ↔ a ≤ 0 ]
theorem coe_le_one : ∀ {α : Type u} [inst : One α inst_1 : LE α a : α }, ↑a ≤ 1 ↔ a ≤ 1 coe_le_one [ LE α ] { a : α } : ( a : WithTop α ) ≤ 1 ↔ a ≤ 1 :=
coe_le_coe : ∀ {α : Type ?u.2414} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b
#align with_top.coe_le_one WithTop.coe_le_one : ∀ {α : Type u} [inst : One α inst_1 : LE α a : α }, ↑a ≤ 1 ↔ a ≤ 1
#align with_top.coe_le_zero WithTop.coe_le_zero : ∀ {α : Type u} [inst : Zero α inst_1 : LE α a : α }, ↑a ≤ 0 ↔ a ≤ 0
@[ to_additive ( attr := simp , norm_cast ) coe_pos : ∀ {α : Type u} [inst : Zero α inst_1 : LT α a : α }, 0 < ↑a ↔ 0 < a ]
theorem one_lt_coe : ∀ {α : Type u} [inst : One α inst_1 : LT α a : α }, 1 < ↑a ↔ 1 < a one_lt_coe [ LT α ] { a : α } : 1 < ( a : WithTop α ) ↔ 1 < a :=
coe_lt_coe : ∀ {α : Type ?u.3167} [inst : LT α a b : α }, ↑a < ↑b ↔ a < b
#align with_top.one_lt_coe WithTop.one_lt_coe : ∀ {α : Type u} [inst : One α inst_1 : LT α a : α }, 1 < ↑a ↔ 1 < a
#align with_top.coe_pos WithTop.coe_pos : ∀ {α : Type u} [inst : Zero α inst_1 : LT α a : α }, 0 < ↑a ↔ 0 < a
@[ to_additive ( attr := simp , norm_cast ) coe_lt_zero : ∀ {α : Type u} [inst : Zero α inst_1 : LT α a : α }, ↑a < 0 ↔ a < 0 ]
theorem coe_lt_one : ∀ {α : Type u} [inst : One α inst_1 : LT α a : α }, ↑a < 1 ↔ a < 1 coe_lt_one [ LT α ] { a : α } : ( a : WithTop α ) < 1 ↔ a < 1 :=
coe_lt_coe : ∀ {α : Type ?u.3910} [inst : LT α a b : α }, ↑a < ↑b ↔ a < b
#align with_top.coe_lt_one WithTop.coe_lt_one : ∀ {α : Type u} [inst : One α inst_1 : LT α a : α }, ↑a < 1 ↔ a < 1
#align with_top.coe_lt_zero WithTop.coe_lt_zero : ∀ {α : Type u} [inst : Zero α inst_1 : LT α a : α }, ↑a < 0 ↔ a < 0
@[ to_additive : ∀ {α : Type u} [inst : Zero α β : Type u_1} (f : α → β map f 0 = ↑(f 0 to_additive ( attr := simp )]
protected theorem map_one : ∀ {β : Type u_1} (f : α → β map f 1 = ↑(f 1 map_one { β } ( f : α → β ) : ( 1 : WithTop α ). map f = ( f 1 : WithTop β ) :=
rfl : ∀ {α : Sort ?u.4380} {a : α }, a = a
#align with_top.map_one WithTop.map_one : ∀ {α : Type u} [inst : One α β : Type u_1} (f : α → β map f 1 = ↑(f 1
#align with_top.map_zero WithTop.map_zero : ∀ {α : Type u} [inst : Zero α β : Type u_1} (f : α → β map f 0 = ↑(f 0
@[ to_additive : ∀ {α : Type u} [inst : Zero α a : α }, 0 = ↑a ↔ a = 0 to_additive ( attr := simp , norm_cast )]
theorem one_eq_coe : ∀ {α : Type u} [inst : One α a : α }, 1 = ↑a ↔ a = 1 one_eq_coe { a : α } : 1 = ( a : WithTop α ) ↔ a = 1 :=
Trans.trans : ∀ {α : Sort ?u.4638} {β : Sort ?u.4637} {γ : Sort ?u.4636} {r : α → β → Sort ?u.4641s : β → γ → Sort ?u.4640t : outParam (α → γ → Sort ?u.4639self : Trans r s t a : α } {b : β } {c : γ }, r a b s b c t a c eq_comm : ∀ {α : Sort ?u.4692} {a b : α }, a = b ↔ b = a coe_eq_one : ∀ {α : Type ?u.4703} [inst : One α a : α }, ↑a = 1 ↔ a = 1
#align with_top.one_eq_coe WithTop.one_eq_coe : ∀ {α : Type u} [inst : One α a : α }, 1 = ↑a ↔ a = 1
#align with_top.zero_eq_coe WithTop.zero_eq_coe : ∀ {α : Type u} [inst : Zero α a : α }, 0 = ↑a ↔ a = 0
@[ to_additive : ∀ {α : Type u} [inst : Zero α ⊤ ≠ 0 to_additive ( attr := simp )]
theorem top_ne_one : ⊤ ≠ ( 1 : WithTop α ) :=
fun .
#align with_top.top_ne_one WithTop.top_ne_one : ∀ {α : Type u} [inst : One α ⊤ ≠ 1
#align with_top.top_ne_zero WithTop.top_ne_zero : ∀ {α : Type u} [inst : Zero α ⊤ ≠ 0
@[ to_additive : ∀ {α : Type u} [inst : Zero α 0 ≠ ⊤ to_additive ( attr := simp )]
theorem one_ne_top : ( 1 : WithTop α ) ≠ ⊤ :=
fun .
#align with_top.one_ne_top WithTop.one_ne_top : ∀ {α : Type u} [inst : One α 1 ≠ ⊤
#align with_top.zero_ne_top WithTop.zero_ne_top : ∀ {α : Type u} [inst : Zero α 0 ≠ ⊤
instance zeroLEOneClass [ Zero α ] [ LE α ] [ ZeroLEOneClass : (α : Type ?u.5510) → [inst : Zero α [inst : One α [inst : LE α Type α ] : ZeroLEOneClass : (α : Type ?u.5549) → [inst : Zero α [inst : One α [inst : LE α Type ( WithTop α ) :=
⟨ some_le_some . 2 : ∀ {a b : Prop }, (a ↔ b b → a zero_le_one ⟩
end One
section Add
variable [ Add α ] { a b c d : WithTop α } { x y : α }
instance add : Add ( WithTop α ) :=
⟨ Option.map₂ (· + ·) ⟩
#align with_top.has_add WithTop.add
@[ norm_cast ]
theorem coe_add : ∀ {α : Type u} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y coe_add : (( x + y : α ) : WithTop α ) = x + y :=
rfl : ∀ {α : Sort ?u.7072} {a : α }, a = a
#align with_top.coe_add WithTop.coe_add : ∀ {α : Type u} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y
section deprecated
set_option linter.deprecated false
@[ norm_cast , deprecated ]
theorem coe_bit0 : (( bit0 : {α : Type ?u.7224} → [inst : Add α α → α x : α ) : WithTop α ) = ( bit0 : {α : Type ?u.7324} → [inst : Add α α → α x : WithTop α ) :=
rfl : ∀ {α : Sort ?u.7406} {a : α }, a = a
#align with_top.coe_bit0 WithTop.coe_bit0
@[ norm_cast , deprecated ]
theorem coe_bit1 [ One α ] { a : α } : (( bit1 : {α : Type ?u.7527} → [inst : One α [inst : Add α α → α a : α ) : WithTop α ) = ( bit1 : {α : Type ?u.7667} → [inst : One α [inst : Add α α → α a : WithTop α ) :=
rfl : ∀ {α : Sort ?u.7802} {a : α }, a = a
#align with_top.coe_bit1 WithTop.coe_bit1
end deprecated
@[ simp ]
theorem top_add ( a : WithTop α ) : ⊤ + a = ⊤ :=
rfl : ∀ {α : Sort ?u.8065} {a : α }, a = a
#align with_top.top_add WithTop.top_add
@[ simp ]
theorem add_top ( a : WithTop α ) : a + ⊤ = ⊤ := by cases a <;> rfl
#align with_top.add_top WithTop.add_top
@[ simp ]
theorem add_eq_top : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := by
cases a <;> cases b <;> none.none none.some some.none some.some simp [ none_eq_top : ∀ {α : Type ?u.8691}, none = ⊤ , some_eq_coe , ← WithTop.coe_add : ∀ {α : Type ?u.8704} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y ]
#align with_top.add_eq_top WithTop.add_eq_top
theorem add_ne_top : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤ :=
add_eq_top . not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b . trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c not_or
#align with_top.add_ne_top WithTop.add_ne_top
theorem add_lt_top [ LT α ] { a b : WithTop α } : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := by
simp_rw [ WithTop.lt_top_iff_ne_top : ∀ {α : Type ?u.9964} [inst : LT α x : WithTop α x < ⊤ ↔ x ≠ ⊤ , add_ne_top ]
#align with_top.add_lt_top WithTop.add_lt_top
theorem add_eq_coe : ∀ {α : Type u} [inst : Add α a b : WithTop α c : α }, a + b = ↑c ↔ ∃ a' b' , ↑a' = a ∧ ↑b' = b ∧ a' + b' = c add_eq_coe :
∀ { a b : WithTop α } { c : α }, a + b = c ↔ ∃ a' b' : α , ↑ a' = a ∧ ↑ b' = b ∧ a' + b' = c
| none , b , c => by none + b = ↑c ↔ ∃ a' b' , ↑a' = none ∧ ↑b' = b ∧ a' + b' = c simp [ none_eq_top : ∀ {α : Type ?u.10872}, none = ⊤ ]
| Option.some a , none , c => by simp [ none_eq_top : ∀ {α : Type ?u.11890}, none = ⊤ ]
| Option.some a , Option.some b , c =>
by simp only [ some_eq_coe , ← coe_add : ∀ {α : Type ?u.12632} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y , coe_eq_coe : ∀ {α : Type ?u.12647} {a b : α }, ↑a = ↑b ↔ a = b , exists_and_left : ∀ {α : Sort ?u.12666} {p : α → Prop b : Prop }, (∃ x , b ∧ p x ) ↔ b ∧ ∃ x , p x , exists_eq_left : ∀ {α : Sort ?u.12684} {p : α → Prop a' : α }, (∃ a , a = a' ∧ p a ) ↔ p a' ]
#align with_top.add_eq_coe WithTop.add_eq_coe : ∀ {α : Type u} [inst : Add α a b : WithTop α c : α }, a + b = ↑c ↔ ∃ a' b' , ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
-- Porting note: simp can already prove this.
-- @[simp]
theorem add_coe_eq_top_iff { x : WithTop α } { y : α } : x + y = ⊤ ↔ x = ⊤ := by
induction x using WithTop.recTopCoe <;> simp [← coe_add : ∀ {α : Type ?u.13419} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y ]
#align with_top.add_coe_eq_top_iff WithTop.add_coe_eq_top_iff : ∀ {α : Type u} [inst : Add α x : WithTop α y : α }, x + ↑y = ⊤ ↔ x = ⊤
-- Porting note: simp can already prove this.
-- @[simp]
theorem coe_add_eq_top_iff { y : WithTop α } : ↑ x + y = ⊤ ↔ y = ⊤ := by
induction y using WithTop.recTopCoe <;> simp [← coe_add : ∀ {α : Type ?u.14020} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y ]
#align with_top.coe_add_eq_top_iff WithTop.coe_add_eq_top_iff : ∀ {α : Type u} [inst : Add α x : α } {y : WithTop α ↑x + y = ⊤ ↔ y = ⊤
instance covariantClass_add_le [ LE α ] [ CovariantClass : (M : Type ?u.14139) → (N : Type ?u.14138) → (M → N → N (N → N → Prop Prop α α (· + ·) (· ≤ ·) ] :
CovariantClass : (M : Type ?u.14207) → (N : Type ?u.14206) → (M → N → N (N → N → Prop Prop ( WithTop α ) ( WithTop α ) (· + ·) (· ≤ ·) :=
⟨ fun a b c h => by
cases a <;> cases c <;> none.none none.some some.none some.some try exact le_top : ∀ {α : Type ?u.14785} [inst : LE α inst_1 : OrderTop α a : α }, a ≤ ⊤
rcases le_coe_iff : ∀ {α : Type ?u.15326} {b : α } [inst : LE α x : WithTop α x ≤ ↑b ↔ ∃ a , x = ↑a ∧ a ≤ b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h with ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝ b ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝ rfl ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝ _ ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝
exact coe_le_coe : ∀ {α : Type ?u.15424} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( add_le_add_left : ∀ {α : Type ?u.15456} [inst : Add α inst_1 : LE α inst_2 : CovariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x ≤ x_1 b c : α }, b ≤ c ∀ (a : α ), a + b ≤ a + c ( coe_le_coe : ∀ {α : Type ?u.15463} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ) _ ) ⟩
#align with_top.covariant_class_add_le WithTop.covariantClass_add_le
instance covariantClass_swap_add_le [ LE α ] [ CovariantClass : (M : Type ?u.15662) → (N : Type ?u.15661) → (M → N → N (N → N → Prop Prop α α ( swap : {α : Sort ?u.15665} →
{β : Sort ?u.15664} → {φ : α → β → Sort ?u.15663((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· + ·) ) (· ≤ ·) ] :
CovariantClass : (M : Type ?u.15752) → (N : Type ?u.15751) → (M → N → N (N → N → Prop Prop ( WithTop α ) ( WithTop α ) ( swap : {α : Sort ?u.15757} →
{β : Sort ?u.15756} → {φ : α → β → Sort ?u.15755((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· + ·) ) (· ≤ ·) :=
⟨ fun a b c h => by
swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c cases a none swap (fun x x_1 => x + x_1 ) none b ≤ swap (fun x x_1 => x + x_1 ) none c some swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c <;> none swap (fun x x_1 => x + x_1 ) none b ≤ swap (fun x x_1 => x + x_1 ) none c some swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c cases c none.none swap (fun x x_1 => x + x_1 ) none b ≤ swap (fun x x_1 => x + x_1 ) none none none.some swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c <;> none.none swap (fun x x_1 => x + x_1 ) none b ≤ swap (fun x x_1 => x + x_1 ) none none none.some some.none some.some swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c try none.none swap (fun x x_1 => x + x_1 ) none b ≤ swap (fun x x_1 => x + x_1 ) none none exact le_top : ∀ {α : Type ?u.16337} [inst : LE α inst_1 : OrderTop α a : α }, a ≤ ⊤
swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c rcases le_coe_iff : ∀ {α : Type ?u.16883} {b : α } [inst : LE α x : WithTop α x ≤ ↑b ↔ ∃ a , x = ↑a ∧ a ≤ b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h with ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝ b ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝ rfl ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝ _ ⟨b, rfl, _⟩ : b✝ = ↑b ∧ b ≤ val✝
swap (fun x x_1 => x + x_1 ) a b ≤ swap (fun x x_1 => x + x_1 ) a c exact coe_le_coe : ∀ {α : Type ?u.16987} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( add_le_add_right : ∀ {α : Type ?u.17019} [inst : Add α inst_1 : LE α i : CovariantClass α α (swap fun x x_1 => x + x_1 fun x x_1 => x ≤ x_1 b c : α }, b ≤ c ∀ (a : α ), b + a ≤ c + a ( coe_le_coe : ∀ {α : Type ?u.17026} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ) _ ) ⟩
#align with_top.covariant_class_swap_add_le WithTop.covariantClass_swap_add_le
instance contravariantClass_add_lt [ LT α ] [ ContravariantClass : (M : Type ?u.17231) → (N : Type ?u.17230) → (M → N → N (N → N → Prop Prop α α (· + ·) (· < ·) ] :
ContravariantClass : (M : Type ?u.17299) → (N : Type ?u.17298) → (M → N → N (N → N → Prop Prop ( WithTop α ) ( WithTop α ) (· + ·) (· < ·) :=
⟨ fun a b c h => by
induction a using WithTop.recTopCoe ; · exact ( not_none_lt : ∀ {α : Type ?u.17732} [inst : LT α a : WithTop α ¬ none < a _ h ). elim
induction b using WithTop.recTopCoe ; · exact ( not_none_lt : ∀ {α : Type ?u.17796} [inst : LT α a : WithTop α ¬ none < a _ h ). elim
induction c using WithTop.recTopCoe
· exact coe_lt_top : ∀ {α : Type ?u.17858} [inst : LT α a : α ), ↑a < ⊤ _
· exact coe_lt_coe : ∀ {α : Type ?u.17877} [inst : LT α a b : α }, ↑a < ↑b ↔ a < b . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( lt_of_add_lt_add_left : ∀ {α : Type ?u.17895} [inst : Add α inst_1 : LT α inst_2 : ContravariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x < x_1 a b c : α }, a + b < a + c b < c <| coe_lt_coe : ∀ {α : Type ?u.17938} [inst : LT α a b : α }, ↑a < ↑b ↔ a < b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h : ↑a✝² + ↑a✝¹ < ↑a✝² + ↑a✝ h ) ⟩
#align with_top.contravariant_class_add_lt WithTop.contravariantClass_add_lt
instance contravariantClass_swap_add_lt [ LT α ] [ ContravariantClass : (M : Type ?u.18095) → (N : Type ?u.18094) → (M → N → N (N → N → Prop Prop α α ( swap : {α : Sort ?u.18098} →
{β : Sort ?u.18097} → {φ : α → β → Sort ?u.18096((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· + ·) ) (· < ·) ] :
ContravariantClass : (M : Type ?u.18185) → (N : Type ?u.18184) → (M → N → N (N → N → Prop Prop ( WithTop α ) ( WithTop α ) ( swap : {α : Sort ?u.18190} →
{β : Sort ?u.18189} → {φ : α → β → Sort ?u.18188((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· + ·) ) (· < ·) :=
⟨ fun a b c h => by
cases a <;> cases b <;> none.none none.some some.none some.some try exact ( not_none_lt : ∀ {α : Type ?u.18861} [inst : LT α a : WithTop α ¬ none < a _ h ). elim
cases c some.some.none some.some.some
· some.some.none some.some.some exact coe_lt_top : ∀ {α : Type ?u.19150} [inst : LT α a : α ), ↑a < ⊤ _
· exact coe_lt_coe : ∀ {α : Type ?u.19168} [inst : LT α a b : α }, ↑a < ↑b ↔ a < b . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( lt_of_add_lt_add_right : ∀ {α : Type ?u.19186} [inst : Add α inst_1 : LT α i : ContravariantClass α α (swap fun x x_1 => x + x_1 fun x x_1 => x < x_1 a b c : α }, b + a < c + a b < c <| coe_lt_coe : ∀ {α : Type ?u.19233} [inst : LT α a b : α }, ↑a < ↑b ↔ a < b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ) ⟩
#align with_top.contravariant_class_swap_add_lt WithTop.contravariantClass_swap_add_lt
protected theorem le_of_add_le_add_left [ LE α ] [ ContravariantClass : (M : Type ?u.19416) → (N : Type ?u.19415) → (M → N → N (N → N → Prop Prop α α (· + ·) (· ≤ ·) ] ( ha : a ≠ ⊤ )
( h : a + b ≤ a + c ) : b ≤ c := by
lift a to α using ha
induction c using WithTop.recTopCoe
· exact le_top : ∀ {α : Type ?u.19977} [inst : LE α inst_1 : OrderTop α a : α }, a ≤ ⊤
· induction b using WithTop.recTopCoe intro.coe.top intro.coe.coe
· intro.coe.top intro.coe.coe exact ( not_top_le_coe : ∀ {α : Type ?u.20294} [inst : LE α a : α ), ¬ ⊤ ≤ ↑a _ h ). elim
· simp only [← coe_add : ∀ {α : Type ?u.20362} [inst : Add α x y : α }, ↑(x + y = ↑x + ↑y , coe_le_coe : ∀ {α : Type ?u.20385} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b ] at h ⊢
exact le_of_add_le_add_left : ∀ {α : Type ?u.20570} [inst : Add α inst_1 : LE α inst_2 : ContravariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x ≤ x_1 a b c : α }, a + b ≤ a + c b ≤ c h
#align with_top.le_of_add_le_add_left WithTop.le_of_add_le_add_left
protected theorem le_of_add_le_add_right [ LE α ] [ ContravariantClass : (M : Type ?u.20702) → (N : Type ?u.20701) → (M → N → N (N → N → Prop Prop α α ( swap : {α : Sort ?u.20705} →
{β : Sort ?u.20704} → {φ : α → β → Sort ?u.20703((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y (· + ·) ) (· ≤ ·) ]
( ha : a ≠ ⊤ ) ( h : b + a ≤ c + a ) : b ≤ c := by
lift a to α using ha
cases c
· exact le_top : ∀ {α : Type ?u.21313} [inst : LE α inst_1 : OrderTop α a : α }, a ≤ ⊤
· cases b intro.some.none intro.some.some
· intro.some.none intro.some.some exact ( not_top_le_coe : ∀ {α : Type ?u.21653} [inst : LE α a : α ), ¬ ⊤ ≤ ↑a _ h ). elim
· exact coe_le_coe : ∀ {α : Type ?u.21706} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( le_of_add_le_add_right : ∀ {α : Type ?u.21730} [inst : Add α inst_1 : LE α i : ContravariantClass α α (swap fun x x_1 => x + x_1 fun x x_1 => x ≤ x_1 a b c : α }, b + a ≤ c + a b ≤ c <| coe_le_coe : ∀ {α : Type ?u.21781} {a b : α } [inst : LE α ↑a ≤ ↑b ↔ a ≤ b . 1 : ∀ {a b : Prop }, (a ↔ b a → b h )
#align with_top.le_of_add_le_add_right WithTop.le_of_add_le_add_right
protected theorem add_lt_add_left [ LT α ] [ CovariantClass : (M : Type ?u.21930) → (N : Type ?u.21929) → (M → N → N (N → N → Prop Prop α α (· + ·) (· < ·) ] ( ha : a ≠ ⊤ )
( h : b < c ) : a + b < a + c := by
lift a to α using ha