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
α : 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)
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
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)
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
obtain ⟨c, rfl⟩ := hf c
no goals
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)
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)