[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
⊢ Set.Subsingleton s
[PROOFSTEP]
rintro a ha b hb
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
[PROOFSTEP]
obtain hab | hab | hab := trichotomous_of r a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b
[PROOFSTEP]
exact h.eq ha hb hab
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b
[PROOFSTEP]
exact hab
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
[PROOFSTEP]
exact h.eq' ha hb hab
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
⊢ IsAntichain r' (f '' s)
[PROOFSTEP]
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b✝ : α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False
[PROOFSTEP]
exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
hs : IsAntichain r s
φ : r ↪r r'
⊢ IsAntichain r' (↑φ '' s)
[PROOFSTEP]
intro b hb b' hb' h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b✝ : α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ↑φ '' s
b' : β
hb' : b' ∈ ↑φ '' s
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
[PROOFSTEP]
rw [Set.mem_image] at hb hb' 
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b✝ : α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x, x ∈ s ∧ ↑φ x = b
b' : β
hb' : ∃ x, x ∈ s ∧ ↑φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b : α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : ↑φ a ≠ ↑φ a'
h₂ : r' (↑φ a) (↑φ a')
⊢ False
[PROOFSTEP]
exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b : α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : ↑φ a ≠ ↑φ a'
h₂ : r' (↑φ a) (↑φ a')
haa' : a = a'
⊢ ↑φ a = ↑φ a'
[PROOFSTEP]
rw [haa']
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsLeast s a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
t : Set α
a b : α
inst✝ : Preorder α
⊢ IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsLeast {a} a
[PROOFSTEP]
exact ⟨isAntichain_singleton _ _, isLeast_singleton⟩
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsGreatest s a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
t : Set α
a b : α
inst✝ : Preorder α
⊢ IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsGreatest {a} a
[PROOFSTEP]
exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c
[PROOFSTEP]
obtain ⟨c, rfl⟩ := hf c
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)
[PROOFSTEP]
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)
