[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : PartialOrder α
x y : α
⊢ x ≤ y → y = x ↔ ¬x < y
[PROOFSTEP]
rw [lt_iff_le_and_ne, not_and, Classical.not_not, eq_comm]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ min a b = if b ≤ a then b else a
[PROOFSTEP]
rw [min_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rcases lt_trichotomy a b with (lt | eq | gt)
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rw [if_pos lt.le, if_neg (not_le.mpr lt)]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rw [if_pos eq.le, if_pos eq.ge, eq]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
[PROOFSTEP]
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ max a b = if b ≤ a then a else b
[PROOFSTEP]
rw [max_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rcases lt_trichotomy a b with (lt | eq | gt)
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rw [if_pos lt.le, if_neg (not_le.mpr lt)]
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rw [if_pos eq.le, if_pos eq.ge, eq]
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
[PROOFSTEP]
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c
[PROOFSTEP]
rw [comm, comm b, comm _ c, comm a]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)
[PROOFSTEP]
exact assoc _ _ _
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝¹ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le✝ B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
h : toLE = toLE
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
cases h
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
have : A_lt = B_lt := by
  funext a b
  show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
  rw [A_iff, B_iff]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
⊢ A_lt = B_lt
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
a b : α
⊢ A_lt a b = B_lt a b
[PROOFSTEP]
show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
a b : α
⊢ (a < b) = (a < b)
[PROOFSTEP]
rw [A_iff, B_iff]
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
this : A_lt = B_lt
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
cases this
[GOAL]
case refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
⊢ mk le_refl✝¹ le_trans✝¹ = mk le_refl✝ le_trans✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : PartialOrder α
h : toPreorder = toPreorder
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
B : PartialOrder α
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝ = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
toPreorder✝¹ : Preorder α
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
[PROOFSTEP]
cases h
[GOAL]
case mk.mk.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_le B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
B_decidableEq : DecidableEq α
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
h : toPartialOrder = toPartialOrder
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ B_decidableLE B_decidableEq B_decidableLT
[PROOFSTEP]
cases h
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
B_decidableEq : DecidableEq α
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ B_decidableLE B_decidableEq B_decidableLT
[PROOFSTEP]
obtain rfl : A_decidableLE = B_decidableLE := Subsingleton.elim _ _
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
B_decidableEq : DecidableEq α
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE B_decidableEq B_decidableLT
[PROOFSTEP]
obtain rfl : A_decidableEq = B_decidableEq := Subsingleton.elim _ _
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_decidableLT : DecidableRel fun x x_1 => x < x_1
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq B_decidableLT
[PROOFSTEP]
obtain rfl : A_decidableLT = B_decidableLT := Subsingleton.elim _ _
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
have : A_min = B_min := by
  funext a b
  exact (A_min_def _ _).trans (B_min_def _ _).symm
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
⊢ A_min = B_min
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
a b : α
⊢ A_min a b = B_min a b
[PROOFSTEP]
exact (A_min_def _ _).trans (B_min_def _ _).symm
[GOAL]
case refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
this : A_min = B_min
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
cases this
[GOAL]
case refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
have : A_max = B_max := by
  funext a b
  exact (A_max_def _ _).trans (B_max_def _ _).symm
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
⊢ A_max = B_max
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
a b : α
⊢ A_max a b = B_max a b
[PROOFSTEP]
exact (A_max_def _ _).trans (B_max_def _ _).symm
[GOAL]
case refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
this : A_max = B_max
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
cases this
[GOAL]
case refl.refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
have : A_compare = B_compare := by
  funext a b
  exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
⊢ A_compare = B_compare
[PROOFSTEP]
funext a b
[GOAL]
case h.h
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
a b : α
⊢ A_compare a b = B_compare a b
[PROOFSTEP]
exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
[GOAL]
case refl.refl.refl
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x x_1 => x < x_1
A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
this : A_compare = B_compare
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
ext x y
[GOAL]
case a.le.h.h.a
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
[PROOFSTEP]
exact H x y
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
ext x y
[GOAL]
case a.a.le.h.h.a
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
[PROOFSTEP]
exact H x y
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
ext x y
[GOAL]
case a.a.a.le.h.h.a
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y
[PROOFSTEP]
exact H x y
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ max a b = if a ≤ b then a else b
[PROOFSTEP]
rw [max_comm, max_def]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ (if b ≤ a then a else b) = if a ≤ b then a else b
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ min a b = if a ≤ b then b else a
[PROOFSTEP]
rw [min_comm, min_def]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type u_3
inst✝ : LinearOrder α
src✝ : PartialOrder αᵒᵈ := inferInstanceAs (PartialOrder αᵒᵈ)
a b : αᵒᵈ
⊢ (if b ≤ a then b else a) = if a ≤ b then b else a
[PROOFSTEP]
rfl
[GOAL]
ι✝ : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι✝ → Type u_2
r : α✝ → α✝ → Prop
ι : Type u
α : ι → Type v
inst✝ : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i
[PROOFSTEP]
simp (config := { contextual := true }) [lt_iff_le_not_le, Pi.le_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
⊢ a < b
[PROOFSTEP]
inhabit ι
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b
[PROOFSTEP]
exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
[PROOFSTEP]
simp (config := { contextual := true }) [update_le_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update x i b ↔ a ≤ b
[PROOFSTEP]
simp [update_le_update_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ x ≤ update x i a ↔ x i ≤ a
[PROOFSTEP]
simp [le_update_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ x ↔ a ≤ x i
[PROOFSTEP]
simp [update_le_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ x < update x i a ↔ x i < a
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a < x ↔ a < x i
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b
[PROOFSTEP]
simp [Pi.le_def]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b
[PROOFSTEP]
simpa [Pi.lt_def] using le_of_lt
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ min x y = if x < y then x else y
[PROOFSTEP]
rw [min_comm, min_def, ← ite_not]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ (if ¬y ≤ x then x else y) = if x < y then x else y
[PROOFSTEP]
simp only [not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ max x y = if x < y then y else x
[PROOFSTEP]
rw [max_comm, max_def, ← ite_not]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ (if ¬y ≤ x then y else x) = if x < y then y else x
[PROOFSTEP]
simp only [not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
[PROOFSTEP]
have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
[PROOFSTEP]
simp only [h, compareOfLessAndEq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
try
  (first
    | rfl
    | contradiction)
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
have : ¬f a = f b := by rename_i h; exact inj.ne h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ ¬f a = f b
[PROOFSTEP]
rename_i h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : ¬a < b
h : ¬a = b
⊢ ¬f a = f b
[PROOFSTEP]
exact inj.ne h
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
this : ¬f a = f b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
[PROOFSTEP]
have : f a = f b := by rename_i h; exact congrArg f h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ f a = f b
[PROOFSTEP]
rename_i h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : ¬a < b
h : a = b
⊢ f a = f b
[PROOFSTEP]
exact congrArg f h
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
this : f a = f b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), min a b = if a ≤ b then a else b
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ min x y = if x ≤ y then x else y
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = f (if x ≤ y then x else y)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = if x ≤ y then f x else f y
[PROOFSTEP]
exact (hinf _ _).trans (min_def _ _)
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), max a b = if a ≤ b then b else a
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ max x y = if x ≤ y then y else x
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = f (if x ≤ y then y else x)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.96324
β : Type ?u.96321
inst✝² : LinearOrder β
inst✝¹ : Sup α
inst✝ : Inf α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
instOrdα : Ord α := { compare := fun a b => compare (f a) (f b) }
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = if x ≤ y then f y else f x
[PROOFSTEP]
exact (hsup _ _).trans (max_def _ _)
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), min a b = if a ≤ b then a else b
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ min x y = if x ≤ y then x else y
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = f (if x ≤ y then x else y)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (min x y) = if x ≤ y then f x else f y
[PROOFSTEP]
exact (hinf _ _).trans (min_def _ _)
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
⊢ ∀ (a b : α), max a b = if a ≤ b then b else a
[PROOFSTEP]
intros x y
[GOAL]
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ max x y = if x ≤ y then y else x
[PROOFSTEP]
apply inj
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = f (if x ≤ y then y else x)
[PROOFSTEP]
rw [apply_ite f]
[GOAL]
case a
ι : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : Type ?u.97808
β : Type ?u.97805
inst✝³ : LinearOrder β
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : Ord α
f : α → β
inj : Injective f
hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)
compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)
decidableLE : (x y : α) → Decidable (f x ≤ f y) := fun x y => inferInstance
decidableLT : (x y : α) → Decidable (f x < f y) := fun x y => inferInstance
decidableEq : (x y : α) → Decidable (x = y) := fun x y => decidable_of_iff (f x = f y) (_ : f x = f y ↔ x = y)
src✝ : PartialOrder α := PartialOrder.lift f inj
x y : α
⊢ f (max x y) = if x ≤ y then f y else f x
[PROOFSTEP]
exact (hsup _ _).trans (max_def _ _)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
by_cases h₁ : y.1 ≤ x.1
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
exact Or.inr ⟨h.1.1, LE.le.lt_of_not_le h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
[PROOFSTEP]
exact Or.inl ⟨LE.le.lt_of_not_le h.1.1 h₁, h.1.2⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
[PROOFSTEP]
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
[GOAL]
case refine'_2.inl.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y
[PROOFSTEP]
exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_le h.1⟩
[GOAL]
case refine'_2.inr.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
[PROOFSTEP]
exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_le h.2⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LT α
⊢ DenselyOrdered αᵒᵈ → DenselyOrdered α
[PROOFSTEP]
convert @OrderDual.denselyOrdered αᵒᵈ _
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
[PROOFSTEP]
simp_rw [Prod.lt_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    ∃ a_2,
      (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
        (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)
[PROOFSTEP]
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
[GOAL]
case inl.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h₁
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
c : α
ha : a.fst < c
hb : c < b.fst
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
exact ⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩
[GOAL]
case inr.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h₂
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
c : β
ha : a.snd < c
hb : c < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
[PROOFSTEP]
exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
[PROOFSTEP]
classical
simp_rw [Pi.lt_def]
rintro ⟨hab, i, hi⟩
obtain ⟨c, ha, hb⟩ := exists_between hi
exact
  ⟨Function.update a i c, ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_same]⟩,
    update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_same]⟩
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
[PROOFSTEP]
simp_rw [Pi.lt_def]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
⊢ (a ≤ b ∧ ∃ i, a i < b i) → ∃ a_2, (a ≤ a_2 ∧ ∃ i, a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ i, a_2 i < b i
[PROOFSTEP]
rintro ⟨hab, i, hi⟩
[GOAL]
case intro.intro
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between hi
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
c : α i
ha : a i < c
hb : c < b i
⊢ ∃ a_1, (a ≤ a_1 ∧ ∃ i, a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ i, a_1 i < b i
[PROOFSTEP]
exact
  ⟨Function.update a i c, ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_same]⟩,
    update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_same]⟩
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
c : α i
ha : a i < c
hb : c < b i
⊢ a i < update a i c i
[PROOFSTEP]
rwa [update_same]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α✝ → α✝ → Prop
α : ι → Type u_3
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
a b : (i : ι) → α i
hab : a ≤ b
i : ι
hi : a i < b i
c : α i
ha : a i < c
hb : c < b i
⊢ update a i c i < b i
[PROOFSTEP]
rwa [update_same]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
⊢ x = y ∨ y = z ∨ x = z
[PROOFSTEP]
by_contra hne
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : ¬(x = y ∨ y = z ∨ x = z)
⊢ False
[PROOFSTEP]
simp only [not_or, ← Ne.def] at hne 
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
⊢ False
[PROOFSTEP]
cases' hne.1.lt_or_lt with h₁ h₁
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False
[PROOFSTEP]
cases' hne.2.1.lt_or_lt with h₂ h₂
[GOAL]
case inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False
[PROOFSTEP]
cases' hne.2.1.lt_or_lt with h₂ h₂
[GOAL]
case inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False
[PROOFSTEP]
cases' hne.2.2.lt_or_lt with h₃ h₃
[GOAL]
case inl.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : x < z
⊢ False
case inl.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : z < x
⊢ False
case inl.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : x < z
⊢ False
case inl.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : z < x
⊢ False
case inr.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : x < z
⊢ False
case inr.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : z < x
⊢ False
case inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : x < z
⊢ False
case inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : z < x
⊢ False
[PROOFSTEP]
exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a : PUnit), a ≤ a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝ : PUnit
⊢ a✝ ≤ a✝
[PROOFSTEP]
trivial
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b c : PUnit), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝² b✝ c✝ : PUnit
a✝¹ : a✝² ≤ b✝
a✝ : b✝ ≤ c✝
⊢ a✝² ≤ c✝
[PROOFSTEP]
trivial
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b : PUnit), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
simp only [not_true, and_false, forall_const]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b : PUnit), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝² b✝ : PUnit
a✝¹ : a✝² ≤ b✝
a✝ : b✝ ≤ a✝²
⊢ a✝² = b✝
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
⊢ ∀ (a b : PUnit), a ≤ b ∨ b ≤ a
[PROOFSTEP]
intros
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
π : ι → Type u_2
r : α → α → Prop
a b : PUnit
a✝ b✝ : PUnit
⊢ a✝ ≤ b✝ ∨ b✝ ≤ a✝
[PROOFSTEP]
exact Or.inl trivial
