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
α : 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)
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr
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
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
exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)