[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
⊢ ∀ ⦃b : α⦄, b ∈ {a} → r a b → r b a
[PROOFSTEP]
rintro b (rfl : b = a)
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
b✝ b : α
⊢ r b b → r b b
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
⊢ x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
[PROOFSTEP]
simp only [maximals, Set.mem_sep_iff, and_congr_right_iff]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
⊢ x ∈ s → ((∀ ⦃b : α⦄, b ∈ s → r x b → r b x) ↔ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y)
[PROOFSTEP]
refine' fun _ ↦ ⟨fun h y hys hxy ↦ antisymm hxy (h hys hxy), fun h y hys hxy ↦ _⟩
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
x✝ : x ∈ s
h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
y : α
hys : y ∈ s
hxy : r x y
⊢ r y x
[PROOFSTEP]
convert hxy
[GOAL]
case h.e'_1
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
x✝ : x ∈ s
h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
y : α
hys : y ∈ s
hxy : r x y
⊢ y = x
[PROOFSTEP]
rw [h hys hxy]
[GOAL]
case h.e'_2
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
x✝ : x ∈ s
h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
y : α
hys : y ∈ s
hxy : r x y
⊢ x = y
[PROOFSTEP]
rw [h hys hxy]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝¹ : IsAntisymm α r
x : α
rlt : α → α → Prop
inst✝ : IsNonstrictStrictOrder α r rlt
⊢ x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt y x → ¬y ∈ s
[PROOFSTEP]
simp [minimals, right_iff_left_not_left_of r rlt, not_imp_not, imp.swap (a := _ ∈ _)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝¹ : IsAntisymm α r
x : α
rlt : α → α → Prop
inst✝ : IsNonstrictStrictOrder α r rlt
⊢ x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt x y → ¬y ∈ s
[PROOFSTEP]
simp [maximals, right_iff_left_not_left_of r rlt, not_imp_not, imp.swap (a := _ ∈ _)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
⊢ minimals r s = minimals r t
[PROOFSTEP]
refine
  Set.ext fun a ↦ ⟨fun ⟨has, hmin⟩ ↦ ⟨?_, fun b hbt ↦ hmin (hts hbt)⟩, fun ⟨hat, hmin⟩ ↦ ⟨hts hat, fun b hbs hba ↦ ?_⟩⟩
[GOAL]
case refine_1
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r s
has : a ∈ s
hmin : ∀ ⦃b : α⦄, b ∈ s → r b a → r a b
⊢ a ∈ t
[PROOFSTEP]
obtain ⟨a', ha', haa'⟩ := h _ has
[GOAL]
case refine_1.intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r s
has : a ∈ s
hmin : ∀ ⦃b : α⦄, b ∈ s → r b a → r a b
a' : α
ha' : a' ∈ t
haa' : r a' a
⊢ a ∈ t
[PROOFSTEP]
rwa [antisymm (hmin (hts ha') haa') haa']
[GOAL]
case refine_2
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r t
hat : a ∈ t
hmin : ∀ ⦃b : α⦄, b ∈ t → r b a → r a b
b : α
hbs : b ∈ s
hba : r b a
⊢ r a b
[PROOFSTEP]
obtain ⟨b', hb't, hb'b⟩ := h b hbs
[GOAL]
case refine_2.intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r t
hat : a ∈ t
hmin : ∀ ⦃b : α⦄, b ∈ t → r b a → r a b
b : α
hbs : b ∈ s
hba : r b a
b' : α
hb't : b' ∈ t
hb'b : r b' b
⊢ r a b
[PROOFSTEP]
rwa [antisymm (hmin hb't (Trans.trans hb'b hba)) (Trans.trans hb'b hba)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsSymm α r
⊢ maximals r s = minimals r s
[PROOFSTEP]
rw [minimals_of_symm, maximals_of_symm]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
h : Set.Subsingleton s
⊢ maximals r s = s
[PROOFSTEP]
rcases h.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
[GOAL]
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
t : Set α
a b : α
h : Set.Subsingleton ∅
⊢ maximals r ∅ = ∅
case inr.intro α : Type u_1 r r₁ r₂ : α → α → Prop t : Set α a b x : α h : Set.Subsingleton {x} ⊢ maximals r {x} = {x}
[PROOFSTEP]
exacts [minimals_empty _, maximals_singleton _ _]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
⊢ r₁ b a
[PROOFSTEP]
have := eq_of_mem_maximals ha hb (h _ _ hab)
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
this : a = b
⊢ r₁ b a
[PROOFSTEP]
subst this
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
hb : a ∈ s
hab : r₁ a a
⊢ r₁ a a
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ minimals r₂ s
b : α
hb : b ∈ s
hab : r₁ b a
⊢ r₁ a b
[PROOFSTEP]
have := eq_of_mem_minimals ha hb (h _ _ hab)
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ minimals r₂ s
b : α
hb : b ∈ s
hab : r₁ b a
this : a = b
⊢ r₁ a b
[PROOFSTEP]
subst this
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ minimals r₂ s
hb : a ∈ s
hab : r₁ a a
⊢ r₁ a a
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
⊢ maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
⊢ a ∈ maximals r s ∪ maximals r t
[PROOFSTEP]
obtain h | h := ha.1
[GOAL]
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ s
⊢ a ∈ maximals r s ∪ maximals r t
[PROOFSTEP]
exact Or.inl ⟨h, fun b hb => ha.2 <| Or.inl hb⟩
[GOAL]
case inr
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ t
⊢ a ∈ maximals r s ∪ maximals r t
[PROOFSTEP]
exact Or.inr ⟨h, fun b hb => ha.2 <| Or.inr hb⟩
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ r b a
[PROOFSTEP]
obtain rfl := h.eq ha hb hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
h : IsAntichain r s
a : α
ha hb : a ∈ s
hab : r a a
⊢ r a a
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
⊢ maximals r s = t
[PROOFSTEP]
refine' h.antisymm fun a ha => _
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
⊢ a ∈ maximals r s
[PROOFSTEP]
obtain ⟨b, hb, hr⟩ := hs ha
[GOAL]
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
b : α
hb : b ∈ maximals r s
hr : r b a
⊢ a ∈ maximals r s
[PROOFSTEP]
rwa [of_not_not fun hab => ht (h hb) ha (Ne.symm hab) hr]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
⊢ minimals r s = t
[PROOFSTEP]
refine' h.antisymm fun a ha => _
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
⊢ a ∈ minimals r s
[PROOFSTEP]
obtain ⟨b, hb, hr⟩ := hs ha
[GOAL]
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
b : α
hb : b ∈ minimals r s
hr : r a b
⊢ a ∈ minimals r s
[PROOFSTEP]
rwa [of_not_not fun hab => ht ha (h hb) hab hr]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : PartialOrder α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
a : α
x✝ : a ∈ minimals (fun x x_1 => x ≤ x_1) ↑(upperClosure s)
b : α
hb : b ∈ s
hba : b ≤ a
right✝ : ∀ ⦃b : α⦄, b ∈ ↑(upperClosure s) → (fun x x_1 => x ≤ x_1) b a → (fun x x_1 => x ≤ x_1) a b
⊢ a ∈ s
[PROOFSTEP]
rwa [eq_of_mem_minimals ‹a ∈ _› (subset_upperClosure hb) hba]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : PartialOrder α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
a : α
ha : a ∈ s
b : α
x✝ : b ∈ ↑(upperClosure s)
hba : (fun x x_1 => x ≤ x_1) b a
c : α
hc : c ∈ s
hcb : c ≤ b
⊢ (fun x x_1 => x ≤ x_1) a b
[PROOFSTEP]
rwa [hs.eq' ha hc (hcb.trans hba)]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
⊢ minimals s (f '' x) = f '' minimals r x
[PROOFSTEP]
ext a
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ a ∈ minimals s (f '' x) ↔ a ∈ f '' minimals r x
[PROOFSTEP]
simp only [minimals, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_1 : α), a_1 ∈ x → s (f a_1) a → s a (f a_1)} ↔
    ∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_1 : α), a_1 ∈ x → s (f a_1) a → s a (f a_1)} →
    ∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = a
[PROOFSTEP]
rintro ⟨⟨a, ha, rfl⟩, h⟩
[GOAL]
case h.mp.intro.intro.intro
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : α
ha : a ∈ x
h : ∀ (a_1 : α), a_1 ∈ x → s (f a_1) (f a) → s (f a) (f a_1)
⊢ ∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = f a
[PROOFSTEP]
exact ⟨a, ⟨ha, fun y hy hya ↦ (hf ha hy).mpr (h _ hy ((hf hy ha).mp hya))⟩, rfl⟩
[GOAL]
case h.mpr
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ (∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = a) →
    a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_2 : α), a_2 ∈ x → s (f a_2) a → s a (f a_2)}
[PROOFSTEP]
rintro ⟨a, ⟨⟨ha, h⟩, rfl⟩⟩
[GOAL]
case h.mpr.intro.intro.intro
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : α
ha : a ∈ x
h : ∀ ⦃b : α⦄, b ∈ x → r b a → r a b
⊢ f a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_1 : α), a_1 ∈ x → s (f a_1) a → s a (f a_1)}
[PROOFSTEP]
exact ⟨⟨_, ha, rfl⟩, fun y hy hya ↦ (hf ha hy).mp (h hy ((hf hy ha).mpr hya))⟩
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
⊢ minimals s (↑f '' x) = ↑f '' minimals r x
[PROOFSTEP]
rw [minimals_image_of_rel_iff_rel]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
⊢ x ∩ f ⁻¹' minimals s (f '' x ∩ y) = minimals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
ext a
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
a : α
⊢ a ∈ x ∩ f ⁻¹' minimals s (f '' x ∩ y) ↔ a ∈ minimals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
simp only [minimals, mem_inter_iff, mem_image, and_imp, forall_exists_index, forall_apply_eq_imp_iff₂,
  preimage_setOf_eq, mem_setOf_eq, mem_preimage]
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
a : α
⊢ (a ∈ x ∧
      ((∃ x_1, x_1 ∈ x ∧ f x_1 = f a) ∧ f a ∈ y) ∧
        ∀ (a_1 : α), a_1 ∈ x → f a_1 ∈ y → s (f a_1) (f a) → s (f a) (f a_1)) ↔
    (a ∈ x ∧ f a ∈ y) ∧ ∀ ⦃b : α⦄, b ∈ x → f b ∈ y → r b a → r a b
[PROOFSTEP]
exact
  ⟨fun ⟨hax, ⟨_, hay⟩, h2⟩ ↦
    ⟨⟨hax, hay⟩, fun a₁ ha₁ ha₁y ha₁a ↦ (hf hax ha₁).mpr (h2 _ ha₁ ha₁y ((hf ha₁ hax).mp ha₁a))⟩, fun ⟨⟨hax, hay⟩, h⟩ ↦
    ⟨hax, ⟨⟨_, hax, rfl⟩, hay⟩, fun a' ha' ha'y hsa' ↦ (hf hax ha').mp (h ha' ha'y ((hf ha' hax).mpr hsa'))⟩⟩
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
y : Set β
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
hy : y ⊆ f '' x
⊢ x ∩ f ⁻¹' minimals s y = minimals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
rw [← inter_eq_self_of_subset_right hy, inter_minimals_preimage_inter_eq_of_rel_iff_rel_on hf, preimage_inter, ←
  inter_assoc, inter_eq_self_of_subset_left (subset_preimage_image f x)]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
y : Set β
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ x ∩ ↑f ⁻¹' minimals s y = minimals r (x ∩ ↑f ⁻¹' y)
[PROOFSTEP]
rw [inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset _ h]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ minimals r (↑f ⁻¹' y) = ↑f ⁻¹' minimals s (y ∩ range ↑f)
[PROOFSTEP]
convert (f.inter_preimage_minimals_eq univ y).symm
[GOAL]
case h.e'_2.h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' y = univ ∩ ↑f ⁻¹' y
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' minimals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' minimals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [univ_inter]
[GOAL]
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' minimals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' minimals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [inter_comm]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
⊢ x ∩ f ⁻¹' maximals s (f '' x ∩ y) = maximals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
apply inter_minimals_preimage_inter_eq_of_rel_iff_rel_on
[GOAL]
case hf
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
[PROOFSTEP]
exact fun _ _ a b ↦ hf b a
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
y : Set β
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
hy : y ⊆ f '' x
⊢ x ∩ f ⁻¹' maximals s y = maximals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
apply inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset _ hy
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
y : Set β
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
hy : y ⊆ f '' x
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
[PROOFSTEP]
exact fun _ _ a b ↦ hf b a
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
y : Set β
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (↑f a') (↑f a))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ x ∩ ↑f ⁻¹' maximals s y = maximals r (x ∩ ↑f ⁻¹' y)
[PROOFSTEP]
rw [inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset _ h]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ maximals r (↑f ⁻¹' y) = ↑f ⁻¹' maximals s (y ∩ range ↑f)
[PROOFSTEP]
convert (f.inter_preimage_maximals_eq univ y).symm
[GOAL]
case h.e'_2.h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' y = univ ∩ ↑f ⁻¹' y
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' maximals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' maximals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [univ_inter]
[GOAL]
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' maximals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' maximals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [inter_comm]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ minimals (fun x x_1 => x ≤ x_1) (Icc a b) = {a}
[PROOFSTEP]
simp_rw [Icc, and_comm (a := (a ≤ _))]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ minimals (fun x x_1 => x ≤ x_1) {x | x ≤ b ∧ a ≤ x} = {a}
[PROOFSTEP]
exact maximals_Icc (α := αᵒᵈ) hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ minimals (fun x x_1 => x ≤ x_1) (Ico a b) = {a}
[PROOFSTEP]
simp_rw [Ico, and_comm (a := _ ≤ _)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ minimals (fun x x_1 => x ≤ x_1) {x | x < b ∧ a ≤ x} = {a}
[PROOFSTEP]
exact maximals_Ioc (α := αᵒᵈ) hab
