awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : LE α
⊢ Minimal (Minimal P) x ↔ Minimal P x

Tactic:
⟨fun h ↦ h.prop, fun h ↦ ⟨h, fun _ hy hyx ↦ h.le_of_le hy.prop hyx⟩⟩

Premises used: Minimal.prop, Minimal.le_of_le, And.intro, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : LE α
hP : ∀ ⦃x y : α⦄, P y → x ≤ y → P x
⊢ Minimal P x ↔ P x ∧ IsMin x

Tactic:
⟨fun h ↦ ⟨h.prop, fun _ h' ↦ h.le_of_le (hP h.prop h') h'⟩, fun h ↦ ⟨h.1, fun _ _  h' ↦ h.2 h'⟩⟩

Premises used: Minimal.prop, Minimal.le_of_le, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
h : Minimal P x
hle : Q ≤ P
hQ : Q x
⊢ Minimal Q x

Tactic:
⟨hQ, fun y hQy ↦ h.le_of_le (hle y hQy)⟩

Premises used: Minimal.le_of_le, And.intro, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
h : Minimal P x
hQ : Q x
⊢ Minimal (fun (x : α) ↦ P x ∧ Q x) x

Tactic:
h.mono (fun _ ↦ And.left) ⟨h.prop, hQ⟩

Premises used: Minimal.prop, And.left, Minimal.mono, And.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
h : Minimal P x
hQ : Q x
⊢ Minimal (fun (x : α) ↦ Q x ∧ P x) x

Tactic:
h.mono (fun _ ↦ And.right) ⟨hQ, h.prop⟩

Premises used: Minimal.prop, And.right, Minimal.mono, And.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x y : α
inst : LE α
⊢ Minimal (fun (x : α) ↦ x = y) x ↔ x = y

Tactic:
simp +contextual [Minimal]

Premises used: Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : LE α
hx : P x
⊢ ¬Minimal P x ↔ ∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y

Tactic:
simp [Minimal, hx]

Premises used: Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
h : Minimal (fun (x : α) ↦ P x ∨ Q x) x
inl : ∀ (hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y) (h : P x), Minimal P x ∨ Minimal Q x
inr : ∀ (hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y) (h : Q x), Minimal P x ∨ Minimal Q x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
obtain ⟨h | h, hmin⟩ := h
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
.inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : Q x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
.inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : Q x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
exact .inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
simp_rw : Minimal (fun (x : α) ↦ P x) x → Q x
⊢ Minimal (fun (x : α) ↦ P x ∧ Q x) x ↔ Minimal P x ∧ Q x

Tactic:
simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]

Premises used: and_iff_left_of_imp, iff_self_and
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun (x : α) ↦ P x) x → Q x

Tactic:
fun h ↦ hPQ h.prop

Premises used: Minimal.prop
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun (x : α) ↦ P x) x → Q x

Tactic:
exact fun h ↦ hPQ h.prop
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
simp_rw : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ Q x ∧ P x) x
simp_rw₁ : Q x ∧ Minimal P x ↔ Minimal (fun (x : α) ↦ P x ∧ Q x) x
simp_rw₂ : Q x ∧ Minimal P x ↔ Minimal P x ∧ Q x
⊢ Minimal (fun (x : α) ↦ Q x ∧ P x) x ↔ Q x ∧ Minimal P x

Tactic:
simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]

Premises used: iff_comm, and_comm, minimal_and_iff_right_of_imp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : Preorder α
⊢ Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, y < x → ¬P y

Tactic:
simp [Minimal, lt_iff_le_not_ge, imp.swap]

Premises used: lt_iff_le_not_ge, Minimal, imp.swap
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
Q : ι → Prop
f : ι → α
i : ι
⊢ MinimalFor Q f i ↔ Q i ∧ ∀ ⦃j : ι⦄, f j < f i → ¬Q j

Tactic:
simp [MinimalFor, lt_iff_le_not_ge, imp.swap]

Premises used: lt_iff_le_not_ge, MinimalFor, imp.swap
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x y : α
inst : Preorder α
h : Minimal P x
hlt : y < x
⊢ ¬P y

Tactic:
(minimal_iff_forall_lt.1 h).2 hlt

Premises used: minimal_iff_forall_lt, And.right, Iff.mp
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
Q : ι → Prop
f : ι → α
i j : ι
h : MinimalFor Q f i
hlt : f j < f i
⊢ ¬Q j

Tactic:
(minimalFor_iff_forall_lt.1 h).2 hlt

Premises used: And.right, Iff.mp, minimalFor_iff_forall_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x y : α
inst : Preorder α
h : Minimal P x
hy : P y
⊢ ¬y < x

Tactic:
fun hlt ↦ h.not_prop_of_lt hlt hy

Premises used: Minimal.not_prop_of_lt, Not
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
Q : ι → Prop
f : ι → α
i j : ι
h : MinimalFor Q f i
hj : Q j
⊢ ¬f j < f i

Tactic:
fun hlt ↦ h.not_prop_of_lt hlt hj

Premises used: MinimalFor.not_prop_of_lt, Not
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x y : α
inst : Preorder α
⊢ Minimal (fun (x : α) ↦ x ≤ y) x ↔ x ≤ y ∧ IsMin x

Tactic:
minimal_iff_isMin (fun _ _ h h' ↦ h'.trans h)

Premises used: LE.le.trans, minimal_iff_isMin
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x y : α
inst : Preorder α
⊢ Minimal (fun (x : α) ↦ x < y) x ↔ x < y ∧ IsMin x

Tactic:
minimal_iff_isMin (fun _ _ h h' ↦ h'.trans_lt h)

Premises used: LE.le.trans_lt, minimal_iff_isMin
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : Preorder α
hx : P x
simp_rw : (∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ (y : α), y < x ∧ P y
simp_rw₁ : (∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ (y : α), (y ≤ x ∧ ¬x ≤ y) ∧ P y
⊢ ¬Minimal P x ↔ ∃ (y : α), y < x ∧ P y

Tactic:
simp_rw [not_minimal_iff hx, lt_iff_le_not_ge, and_comm]

Premises used: lt_iff_le_not_ge, not_minimal_iff, and_comm
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
⊢ MinimalFor Q f i

Tactic:
⟨h.prop, fun j hj hle ↦ ?_⟩

Premises used: MinimalFor.prop, And.intro, MinimalFor
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
refine : ∀ (j : ι) (hj : Q j) (hle : f j ≤ f i), f i ≤ f j
⊢ MinimalFor Q f i

Tactic:
refine ⟨h.prop, fun j hj hle ↦ ?_⟩
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
by_contra : ∀ (this : ¬f i ≤ f j), False
⊢ f i ≤ f j

Tactic:
by_contra
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
this : ¬f i ≤ f j
⊢ False

Tactic:
h.not_lt hj <| hg ⟨j, hj, rfl⟩ ⟨i, h.prop, rfl⟩ <| lt_of_le_not_ge hle this

Premises used: MinimalFor.prop, lt_of_le_not_ge, And.intro, Exists.intro, rfl, MinimalFor.not_lt
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
this : ¬f i ≤ f j
⊢ False

Tactic:
exact h.not_lt hj <| hg ⟨j, hj, rfl⟩ ⟨i, h.prop, rfl⟩ <| lt_of_le_not_ge hle this

Premises used: MinimalFor.prop, lt_of_le_not_ge, And.intro, Exists.intro, rfl, MinimalFor.not_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
x : α
inst : Preorder α
inst_1 : Preorder β
g : α → β
hg : StrictMonoOn g (setOf P)
h : MinimalFor P g x
⊢ Minimal P x

Tactic:
minimalFor_id.mp <| .of_strictMonoOn_comp (Set.image_id _ ▸ hg) h

Premises used: MinimalFor.of_strictMonoOn_comp, minimalFor_id, Iff.mp
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
⊢ MaximalFor Q f i

Tactic:
⟨h.prop, fun j hj hle ↦ ?_⟩

Premises used: MaximalFor, MinimalFor.prop, And.intro
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
refine : ∀ (j : ι) (hj : Q j) (hle : f i ≤ f j), f j ≤ f i
⊢ MaximalFor Q f i

Tactic:
refine ⟨h.prop, fun j hj hle ↦ ?_⟩
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
by_contra : ∀ (this : ¬f j ≤ f i), False
⊢ f j ≤ f i

Tactic:
by_contra
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
this : ¬f j ≤ f i
⊢ False

Tactic:
h.not_lt hj <| hg ⟨i, h.prop, rfl⟩ ⟨j, hj, rfl⟩ <| lt_of_le_not_ge hle this

Premises used: MinimalFor.prop, lt_of_le_not_ge, And.intro, Exists.intro, rfl, MinimalFor.not_lt
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' setOf Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
this : ¬f j ≤ f i
⊢ False

Tactic:
exact h.not_lt hj <| hg ⟨i, h.prop, rfl⟩ ⟨j, hj, rfl⟩ <| lt_of_le_not_ge hle this

Premises used: MinimalFor.prop, lt_of_le_not_ge, And.intro, Exists.intro, rfl, MinimalFor.not_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
x : α
inst : Preorder α
inst_1 : Preorder β
g : α → β
hg : StrictAntiOn g (setOf P)
h : MinimalFor P g x
⊢ Maximal P x

Tactic:
maximalFor_id.mp <| MinimalFor.maximalFor_of_strictAntiOn_comp (Set.image_id _ ▸ hg) h

Premises used: MinimalFor.maximalFor_of_strictAntiOn_comp, Iff.mp, maximalFor_id
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : WellFoundedLT α
P : ι → Prop
f : ι → α
hP : ∃ (i : ι), P i
⊢ ∃ (i : ι), MinimalFor P f i

Tactic:
simpa [not_lt_iff_le_imp_ge, InvImage] using (instIsWellFoundedInvImage (· < ·) f).wf.has_min _ hP

Premises used: InvImage, IsWellFounded.wf, WellFounded.has_min, not_lt_iff_le_imp_ge
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
inst : Preorder α
inst_1 : WellFoundedLT α
P : α → Prop
hP : ∃ (a : α), P a
⊢ ∃ (a : α), Minimal P a

Tactic:
exists_minimalFor_of_wellFoundedLT P id hP

Premises used: exists_minimalFor_of_wellFoundedLT, id, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
inst : Preorder α
inst_1 : WellFoundedLT α
P : α → Prop
a : α
ha : P a
obtain :
  ∀ (b : α) (hbmin : ∀ ⦃y : α⦄, (fun (b : α) ↦ b ≤ a ∧ P b) y → y ≤ b → b ≤ y) (hba : b ≤ a) (hb : P b),
    ∃ (b : α), b ≤ a ∧ Minimal P b
⊢ ∃ (b : α), b ≤ a ∧ Minimal P b

Tactic:
obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
    exists_minimal_of_wellFoundedLT (fun b ↦ b ≤ a ∧ P b) ⟨a, le_rfl, ha⟩

Premises used: le_rfl, LE.le, exists_minimal_of_wellFoundedLT, And, And.intro, Exists.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
inst : Preorder α
inst_1 : WellFoundedLT α
P : α → Prop
a : α
ha : P a
b : α
hbmin : ∀ ⦃y : α⦄, (fun (b : α) ↦ b ≤ a ∧ P b) y → y ≤ b → b ≤ y
hba : b ≤ a
hb : P b
⊢ ∃ (b : α), b ≤ a ∧ Minimal P b

Tactic:
⟨b, hba, hb, fun c hc hcb ↦ hbmin ⟨hcb.trans hba, hc⟩ hcb⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
inst : Preorder α
inst_1 : WellFoundedLT α
P : α → Prop
a : α
ha : P a
b : α
hbmin : ∀ ⦃y : α⦄, (fun (b : α) ↦ b ≤ a ∧ P b) y → y ≤ b → b ≤ y
hba : b ≤ a
hb : P b
⊢ ∃ (b : α), b ≤ a ∧ Minimal P b

Tactic:
exact ⟨b, hba, hb, fun c hc hcb ↦ hbmin ⟨hcb.trans hba, hc⟩ hcb⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x y : α
inst : PartialOrder α
hx : Minimal P x
hy : P y
hge : y ≤ x
⊢ x = y

Tactic:
(hx.2 hy hge).antisymm hge

Premises used: LE.le.antisymm, And.right
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x y : α
inst : PartialOrder α
hx : Minimal P x
hy : P y
hle : y ≤ x
⊢ y = x

Tactic:
(hx.eq_of_ge hy hle).symm

Premises used: Minimal.eq_of_ge, Eq.symm
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : PartialOrder α
⊢ Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x = y

Tactic:
⟨fun h ↦ ⟨h.1, fun _ ↦ h.eq_of_ge⟩, fun h ↦ ⟨h.1, fun _ hy hle ↦ (h.2 hy hle).le⟩⟩

Premises used: Eq.le, Minimal.eq_of_ge, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
inst : PartialOrder α
s : Set α
⊢ Minimal (fun (x : α) ↦ x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → y ≤ x → x = y

Tactic:
minimal_iff

Premises used: minimal_iff
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x

Tactic:
⟨hy, fun z hz _ ↦ hP hz⟩

Premises used: And.intro, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x

Tactic:
exact ⟨hy, fun z hz _ ↦ hP hz⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x y : α
inst : PartialOrder α
⊢ Minimal (fun (x : α) ↦ y ≤ x) x ↔ x = y

Tactic:
minimal_iff_eq rfl.le fun _ ↦ id

Premises used: id, Eq.le, minimal_iff_eq, rfl
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩

Premises used: Minimal.prop, Minimal.le_of_le, And.intro, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
refine_1 : ∀ (h' : Minimal P x), Q x
refine_2 : ∀ (h' : Minimal Q x) (y : α) (hy : P y) (hyx : y ≤ x), x ≤ y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal P x
refine_1 : ∀ (y : α) (hyx : y ≤ x) (hy : Q y), Q x
⊢ Q x

Tactic:
obtain ⟨y, hyx, hy⟩ := h h'.prop

Premises used: Minimal.prop
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy refine_1 refine_1₁ refine_1₂ refine_1₃ : Q y
⊢ Q x

Tactic:
rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]

Premises used: LE.le.antisymm, Minimal.le_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
refine_2 : ∀ (z : α) (hzy : z ≤ y) (hz : Q z), x ≤ y
⊢ x ≤ y

Tactic:
obtain ⟨z, hzy, hz⟩ := h hy
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
z : α
hzy : z ≤ y
hz : Q z
⊢ x ≤ y

Tactic:
(h'.le_of_le hz (hzy.trans hyx)).trans hzy

Premises used: Minimal.le_of_le, LE.le.trans
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
x : α
inst : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ (y : α), y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
z : α
hzy : z ≤ y
hz : Q z
⊢ x ≤ y

Tactic:
exact (h'.le_of_le hz (hzy.trans hyx)).trans hzy

Premises used: Minimal.le_of_le, LE.le.trans
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x y : α
inst : LinearOrder α
h : Minimal P x
hy : P y
⊢ x ≤ y

Tactic:
le_of_not_gt (h.not_lt hy)

Premises used: Minimal.not_lt, le_of_not_gt
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : LinearOrder α
i j : ι
Q : ι → Prop
f : ι → α
h : MinimalFor Q f i
hj : Q j
⊢ f i ≤ f j

Tactic:
le_of_not_gt (h.not_lt hj)

Premises used: le_of_not_gt, MinimalFor.not_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Minimal P s
ht : P t
hts : t ⊆ s
⊢ s = t

Tactic:
h.eq_of_ge ht hts

Premises used: Minimal.eq_of_ge
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Maximal P s
ht : P t
hst : s ⊆ t
⊢ s = t

Tactic:
h.eq_of_le ht hst

Premises used: Maximal.eq_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Minimal P s
ht : P t
hts : t ⊆ s
⊢ t = s

Tactic:
h.eq_of_le ht hts

Premises used: Minimal.eq_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Maximal P s
ht : P t
hst : s ⊆ t
⊢ t = s

Tactic:
h.eq_of_ge ht hst

Premises used: Maximal.eq_of_ge
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
⊢ Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s = t

Tactic:
_root_.minimal_iff

Premises used: minimal_iff
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
⊢ Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → s = t

Tactic:
_root_.maximal_iff

Premises used: maximal_iff
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
⊢ Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s ⊆ t

Tactic:
Iff.rfl

Premises used: Iff.rfl, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
⊢ Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → t ⊆ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Maximal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hs : P s
⊢ ¬Minimal P s ↔ ∃ (t : Set α), t ⊂ s ∧ P t

Tactic:
not_minimal_iff_exists_lt hs

Premises used: not_minimal_iff_exists_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hs : P s
⊢ ¬Maximal P s ↔ ∃ (t : Set α), s ⊂ t ∧ P t

Tactic:
not_maximal_iff_exists_gt hs

Premises used: not_maximal_iff_exists_gt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
⊢ Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, t ⊂ s → ¬P t

Tactic:
minimal_iff_forall_lt

Premises used: minimal_iff_forall_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Minimal P s
ht : t ⊂ s
⊢ ¬P t

Tactic:
(minimal_iff_forall_lt.1 h).2 ht

Premises used: minimal_iff_forall_lt, And.right, Iff.mp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Minimal P s
ht : P t
⊢ ¬t ⊂ s

Tactic:
h.not_lt ht

Premises used: Minimal.not_lt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
P : Set α → Prop
s : Set α
h : Maximal P s
hx : P (insert x s)
⊢ x ∈ s

Tactic:
h.eq_of_subset hx (subset_insert _ _) ▸ mem_insert ..

Premises used: Eq.rec, Maximal.eq_of_subset, Set.mem_insert, Eq.symm, Set.subset_insert
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
P : Set α → Prop
s : Set α
h : Minimal P s
hx : P (s \ {x})
⊢ ¬x ∈ s

Tactic:
fun hxs ↦ ((h.eq_of_superset hx diff_subset).subset hxs).2 rfl

Premises used: Set.diff_subset, Eq.subset, And.right, Not, rfl, Minimal.eq_of_superset
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
⊢ Minimal P s ↔ P s ∧ ∀ (x : α), x ∈ s → ¬P (s \ {x})

Tactic:
⟨fun h ↦ ⟨h.1, fun _ hx hP ↦ h.notMem_of_prop_diff_singleton hP hx⟩,
    fun h ↦ ⟨h.1, fun _ ht hts x hxs ↦ by_contra fun hxt ↦
      h.2 x hxs (hP ht <| subset_diff_singleton hts hxt)⟩⟩

Premises used: Minimal.notMem_of_prop_diff_singleton, And.right, And.left, Set.subset_diff_singleton, And.intro, Iff.intro, by_contra
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
hs : P s
h : ¬Minimal P s
⊢ ∃ (x : α), x ∈ s ∧ P (s \ {x})

Tactic:
simpa [Set.minimal_iff_forall_diff_singleton hP, hs] using h

Premises used: Set.minimal_iff_forall_diff_singleton
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
⊢ Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, s ⊂ t → ¬P t

Tactic:
maximal_iff_forall_gt

Premises used: maximal_iff_forall_gt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Maximal P s
ht : s ⊂ t
⊢ ¬P t

Tactic:
(maximal_iff_forall_gt.1 h).2 ht

Premises used: maximal_iff_forall_gt, And.right, Iff.mp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s t : Set α
h : Maximal P s
ht : P t
⊢ ¬s ⊂ t

Tactic:
h.not_gt ht

Premises used: Maximal.not_gt
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
simp : Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), ¬x ∈ s → ¬P (insert x s)

Tactic:
simp only [not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s

Tactic:
⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
    fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩

Premises used: Maximal.mem_of_prop_insert, And.right, And.left, And.intro, Iff.intro, Set.insert_subset
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s

Tactic:
exact ⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
    fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
hs : P s
h : ¬Maximal P s
⊢ ∃ (x : α), ¬x ∈ s ∧ P (insert x s)

Tactic:
simpa [Set.maximal_iff_forall_insert hP, hs] using h

Premises used: Set.maximal_iff_forall_insert
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
inst : Preorder α
s : Set α
⊢ {x : α | Minimal (fun (x : α) ↦ x ∈ s) x} ⊆ s

Tactic:
sep_subset ..

Premises used: setOf, Set.sep_subset, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
s : Set α
inst : Preorder α
h : s.Subsingleton
inl :
  ∀ (h : Set.Subsingleton.{u_2} (α := α) ∅),
    Minimal (fun (x : α) ↦ Membership.mem (γ := Set α) ∅ x) x ↔ Membership.mem (γ := Set α) ∅ x
inr :
  ∀ (x_1 : α) (h : Set.Subsingleton (α := α) {x_1}),
    Minimal (fun (x : α) ↦ Membership.mem (γ := Set α) {x_1} x) x ↔ Membership.mem (γ := Set α) {x_1} x
⊢ Minimal (fun (x : α) ↦ x ∈ s) x ↔ x ∈ s

Tactic:
obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
inst : Preorder α
h : Set.Subsingleton.{u_2} (α := α) ∅
⊢ Minimal (fun (x : α) ↦ Membership.mem (γ := Set α) ∅ x) x ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simp