[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a b : α
⊢ a = b → r a b ∧ r b a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a : α
⊢ r a a ∧ r a a
[PROOFSTEP]
exact ⟨refl _, refl _⟩
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsTrichotomous α r
a b : α
⊢ Function.swap r a b ∨ a = b ∨ Function.swap r b a
[PROOFSTEP]
simpa [Function.swap, or_comm, or_left_comm] using trichotomous_of r a b
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝¹ : IsIrrefl α r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = EmptyRelation a b
[PROOFSTEP]
simpa using not_rel_of_subsingleton r
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
⊢ ¬r b a → r b c → r a c
[PROOFSTEP]
intro h₁ h₂
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
⊢ r a c
[PROOFSTEP]
rcases trichotomous_of r a b with (h₃ | rfl | h₃)
[GOAL]
case inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c
case inr.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c
case inr.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c
[PROOFSTEP]
exacts [_root_.trans h₃ h₂, h₂, absurd h₃ h₁]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
⊢ r a b → ¬r c b → r a c
[PROOFSTEP]
intro h₁ h₂
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c
[PROOFSTEP]
rcases trichotomous_of r b c with (h₃ | rfl | h₃)
[GOAL]
case inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c
case inr.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b
case inr.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c
[PROOFSTEP]
exacts [_root_.trans h₁ h₃, h₁, absurd h₃ h₂]
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : x < y
e : y = x
⊢ False
[PROOFSTEP]
rw [e] at h 
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : x < x
e : y = x
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.14854
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsTrichotomous α r
[PROOFSTEP]
infer_instance
  -- see Note [lower instance priority]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.14937
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsTrans α r
[PROOFSTEP]
infer_instance
  -- see Note [lower instance priority]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.15023
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsIrrefl α r
[PROOFSTEP]
infer_instance
  -- see Note [lower instance priority]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.15135
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsAsymm α r
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a b c : α × β
h₁ : Prod.Lex r s a b
h₂ : Prod.Lex r s b c
⊢ Prod.Lex r s a c
[PROOFSTEP]
cases' h₁ with a₁ a₂ b₁ b₂ ab a₁ b₁ b₂ ab
[GOAL]
case left
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
ab : r a₁ b₁
h₂ : Prod.Lex r s (b₁, b₂) c
⊢ Prod.Lex r s (a₁, a₂) c
[PROOFSTEP]
cases' h₂ with _ _ c₁ c₂ bc _ _ c₂ bc
[GOAL]
case right
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : α × β
a₁ : α
b₁ b₂ : β
ab : s b₁ b₂
h₂ : Prod.Lex r s (a₁, b₂) c
⊢ Prod.Lex r s (a₁, b₁) c
[PROOFSTEP]
cases' h₂ with _ _ c₁ c₂ bc _ _ c₂ bc
[GOAL]
case left.left
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
a₂ : β
b₁ : α
b₂ : β
ab : r a₁ b₁
c₁ : α
c₂ : β
bc : r b₁ c₁
⊢ Prod.Lex r s (a₁, a₂) (c₁, c₂)
case left.right
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
a₂ : β
b₁ : α
b₂ : β
ab : r a₁ b₁
c₂ : β
bc : s b₂ c₂
⊢ Prod.Lex r s (a₁, a₂) (b₁, c₂)
case right.left
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
b₁ b₂ : β
ab : s b₁ b₂
c₁ : α
c₂ : β
bc : r a₁ c₁
⊢ Prod.Lex r s (a₁, b₁) (c₁, c₂)
case right.right
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
b₁ b₂ : β
ab : s b₁ b₂
c₂ : β
bc : s b₂ c₂
⊢ Prod.Lex r s (a₁, b₁) (a₁, c₂)
[PROOFSTEP]
exacts [.left _ _ (_root_.trans ab bc), .left _ _ ab, .left _ _ bc, .right _ (_root_.trans ab bc)]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
refine @Subrelation.wf (α × β) (Prod.Lex (· < ·) (· < ·)) (· < ·) ?_ IsWellFounded.wf
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ Subrelation (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ w
[GOAL]
case mk.mk
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : (a₁, b₁) < (a₂, b₂)
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
simp only [Prod.mk_lt_mk] at w 
[GOAL]
case mk.mk
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
rcases eq_or_ne a₁ a₂ with rfl | ha
[GOAL]
case mk.mk.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ b₂ : β
w : a₁ < a₁ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₁ ∧ b₁ < b₂
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₁, b₂)
[PROOFSTEP]
right
[GOAL]
case mk.mk.inl.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ b₂ : β
w : a₁ < a₁ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₁ ∧ b₁ < b₂
⊢ b₁ < b₂
[PROOFSTEP]
simpa using w
[GOAL]
case mk.mk.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
ha : a₁ ≠ a₂
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
left
[GOAL]
case mk.mk.inr.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
ha : a₁ ≠ a₂
⊢ a₁ < a₂
[PROOFSTEP]
rcases w with ⟨a_lt, _⟩ | ⟨a_le, _⟩
[GOAL]
case mk.mk.inr.h.inl.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : a₁ ≠ a₂
a_lt : a₁ < a₂
right✝ : b₁ ≤ b₂
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.inr.h.inr.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : a₁ ≠ a₂
a_le : a₁ ≤ a₂
right✝ : b₁ < b₂
⊢ a₁ < a₂
[PROOFSTEP]
exact Ne.lt_of_le ha a_le
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s✝ : β → β → Prop
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s
[PROOFSTEP]
simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop, not_and, not_not]
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s✝ : β → β → Prop
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s
[PROOFSTEP]
rw [not_iff_comm, not_bounded_iff]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSubset α
a b c : α
hab : a = b
hbc : b ⊆ c
⊢ a ⊆ c
[PROOFSTEP]
rwa [hab]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSubset α
a b c : α
hab : a ⊆ b
hbc : b = c
⊢ a ⊆ c
[PROOFSTEP]
rwa [← hbc]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSSubset α
a b c : α
hab : a = b
hbc : b ⊂ c
⊢ a ⊂ c
[PROOFSTEP]
rwa [hab]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSSubset α
a b c : α
hab : a ⊂ b
hbc : b = c
⊢ a ⊂ c
[PROOFSTEP]
rwa [← hbc]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ IsOrderConnected α fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ IsIncompTrans α fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ IsStrictWeakOrder α fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
