α : 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
α : 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)
intro b hb b' hb' h₁ h₂
α : 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
α : 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
rw [Set.mem_image] at hb hb'
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
α : 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
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
no goals
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
exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)
no goals
α : 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'
rw [haa']