<commit_before>/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
prelude
import init.logic
/- Make sure instances defined in this file have lower priority than the ones
   defined for concrete structures -/
set_option default_priority 100

universe variable u
variables {α : Type u}

class weak_order (α : Type u) extends has_le α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)

class linear_weak_order (α : Type u) extends weak_order α :=
(le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)

class strict_order (α : Type u) extends has_lt α :=
(lt_irrefl : ∀ a : α, ¬ a < a)
(lt_trans : ∀ a b c : α, a < b → b < c → a < c)

/- structures with a weak and a strict order -/
class order_pair (α : Type u) extends weak_order α, has_lt α :=
(le_of_lt : ∀ a b : α, a < b → a ≤ b)
(lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c)
(lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c)
(lt_irrefl : ∀ a : α, ¬ a < a)

class strong_order_pair (α : Type u) extends weak_order α, has_lt α :=
(le_iff_lt_or_eq : ∀ a b : α, a ≤ b ↔ a < b ∨ a = b)
(lt_irrefl : ∀ a : α, ¬ a < a)

class linear_order_pair (α : Type u) extends order_pair α, linear_weak_order α

class linear_strong_order_pair (α : Type u) extends strong_order_pair α, linear_weak_order α

class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
(decidable_lt : decidable_rel lt)

@[refl] lemma le_refl [weak_order α] : ∀ a : α, a ≤ a :=
weak_order.le_refl

def le.refl := @le_refl

@[trans] lemma le_trans [weak_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
weak_order.le_trans

def le.trans := @le_trans

lemma le_antisymm [weak_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
weak_order.le_antisymm

lemma le_of_eq [weak_order α] {a b : α} : a = b → a ≤ b :=
λ h, h ▸ le_refl a

@[trans] lemma ge_trans [weak_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
λ a b c h₁ h₂, le_trans h₂ h₁

def ge.trans := @ge_trans

lemma le_total [linear_weak_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
linear_weak_order.le_total

lemma le_of_not_ge [linear_weak_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
or.resolve_left (le_total b a)

lemma lt_irrefl [strict_order α] : ∀ a : α, ¬ a < a :=
strict_order.lt_irrefl<commit_msg>chore(library/init/algebra/order): remove unnecessary *.refl lemmas<commit_after>/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
prelude
import init.logic
/- Make sure instances defined in this file have lower priority than the ones
   defined for concrete structures -/
set_option default_priority 100

universe variable u
variables {α : Type u}

class weak_order (α : Type u) extends has_le α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)

class linear_weak_order (α : Type u) extends weak_order α :=
(le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)

class strict_order (α : Type u) extends has_lt α :=
(lt_irrefl : ∀ a : α, ¬ a < a)
(lt_trans : ∀ a b c : α, a < b → b < c → a < c)

/- structures with a weak and a strict order -/
class order_pair (α : Type u) extends weak_order α, has_lt α :=
(le_of_lt : ∀ a b : α, a < b → a ≤ b)
(lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c)
(lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c)
(lt_irrefl : ∀ a : α, ¬ a < a)

class strong_order_pair (α : Type u) extends weak_order α, has_lt α :=
(le_iff_lt_or_eq : ∀ a b : α, a ≤ b ↔ a < b ∨ a = b)
(lt_irrefl : ∀ a : α, ¬ a < a)

class linear_order_pair (α : Type u) extends order_pair α, linear_weak_order α

class linear_strong_order_pair (α : Type u) extends strong_order_pair α, linear_weak_order α

class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
(decidable_lt : decidable_rel lt)

@[refl] lemma le_refl [weak_order α] : ∀ a : α, a ≤ a :=
weak_order.le_refl

@[trans] lemma le_trans [weak_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
weak_order.le_trans

lemma le_antisymm [weak_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
weak_order.le_antisymm

lemma le_of_eq [weak_order α] {a b : α} : a = b → a ≤ b :=
λ h, h ▸ le_refl a

@[trans] lemma ge_trans [weak_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
λ a b c h₁ h₂, le_trans h₂ h₁

lemma le_total [linear_weak_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
linear_weak_order.le_total

lemma le_of_not_ge [linear_weak_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
or.resolve_left (le_total b a)

lemma lt_irrefl [strict_order α] : ∀ a : α, ¬ a < a :=
strict_order.lt_irrefl
{'fraction_non_alphanumeric': 0.133588598170602, 'fraction_numerical': 0.0038289725590299937, 'mean_word_length': 3.1573828470380194, 'pattern_counts': {'":': 0, '<': 31, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1055531', 'n_tokens_mistral': 2234, 'n_tokens_neox': 1980, 'n_words': 860}