awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x_1 : α
inst : Preorder α
x : α
h : Set.Subsingleton (α := α) {x}
⊢ Minimal (fun (x_2 : α) ↦ Membership.mem (γ := Set α) {x} x_2) x_1 ↔ Membership.mem (γ := Set α) {x} x_1

Tactic:
simp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
s : Set α
inst : Preorder α
h : IsLeast s x
⊢ Minimal (fun (x : α) ↦ x ∈ s) x

Tactic:
⟨h.1, fun _b hb _ ↦ h.2 hb⟩

Premises used: And.right, And.left, And.intro, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
a x : α
s : Set α
inst : PartialOrder α
h : IsLeast s a
⊢ Minimal (fun (x : α) ↦ x ∈ s) x ↔ x = a

Tactic:
⟨fun h' ↦ h'.eq_of_ge h.1 (h.2 h'.prop), fun h' ↦ h' ▸ h.minimal⟩

Premises used: Minimal.prop, IsLeast.minimal, Eq.rec, Minimal.eq_of_ge, And.right, And.left, Iff.intro, Eq.symm
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f x)

Tactic:
⟨mem_image_of_mem f hx.prop, ?_⟩

Premises used: Minimal.prop, Set.mem_image_of_mem, And.intro, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
refine : ∀ ⦃y : β⦄, (fun (x : β) ↦ x ∈ f '' s) y → y ≤ f x → f x ≤ y
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f x)

Tactic:
refine ⟨mem_image_of_mem f hx.prop, ?_⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
y : α
hy : y ∈ s
rw : y ≤ x → x ≤ y
⊢ f y ≤ f x → f x ≤ f y

Tactic:
rw [hf hx.prop hy, hf hy hx.prop]

Premises used: Minimal.prop
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ y ≤ x → x ≤ y

Tactic:
hx.le_of_le hy

Premises used: Minimal.le_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ y ≤ x → x ≤ y

Tactic:
exact hx.le_of_le hy

Premises used: Minimal.le_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f a) ↔ Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩

Premises used: minimal_mem_image_monotone, And.intro, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
refine : ∀ (h : Minimal (fun (x : β) ↦ x ∈ f '' s) (f a)) (y : α) (hys : (fun (x : α) ↦ x ∈ s) y), y ≤ a → a ≤ y
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f a) ↔ Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun (x : β) ↦ x ∈ f '' s) (f a)
y : α
hys : (fun (x : α) ↦ x ∈ s) y
rw : f y ≤ f a → f a ≤ f y
⊢ y ≤ a → a ≤ y

Tactic:
rw [← hf ha hys, ← hf hys ha]
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun (x : β) ↦ x ∈ f '' s) (f a)
y : α
hys : (fun (x : α) ↦ x ∈ s) y
⊢ f y ≤ f a → f a ≤ f y

Tactic:
h.le_of_le (mem_image_of_mem f hys)

Premises used: Minimal.le_of_le, Set.mem_image_of_mem
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun (x : β) ↦ x ∈ f '' s) (f a)
y : α
hys : (fun (x : α) ↦ x ∈ s) y
⊢ f y ≤ f a → f a ≤ f y

Tactic:
exact h.le_of_le (mem_image_of_mem f hys)

Premises used: Minimal.le_of_le, Set.mem_image_of_mem
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
⊢ Maximal (fun (x : β) ↦ x ∈ f '' s) (f x)

Tactic:
minimal_mem_image_monotone (β := βᵒᵈ) (fun _ _ h h' ↦ hf h' h) hx

Premises used: Set.Mem, minimal_mem_image_monotone, Maximal, OrderDual
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)
⊢ Minimal (fun (x : β) ↦ x ∈ f '' s) (f a) ↔ Maximal (fun (x : α) ↦ x ∈ s) a

Tactic:
maximal_mem_image_monotone_iff (β := βᵒᵈ) ha (fun _ _ h h' ↦ hf h' h)

Premises used: Set.Mem, maximal_mem_image_monotone_iff, OrderDual, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

Tactic:
Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
refine_1 :
  ∀ (x : β),
    x ∈ f '' {x : α | Minimal P x} →
      Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x
refine_2 :
  ∀ (x : β) (h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x),
    x ∈ f '' {x : α | Minimal P x}
⊢ f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

Tactic:
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : α
hx : Minimal P x
⊢ Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} (f x)

Tactic:
(minimal_mem_image_monotone_iff hx.prop hf).2 hx

Premises used: Iff.mpr, Set.Mem, setOf, Minimal.prop, minimal_mem_image_monotone_iff, Set.image, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : α
hx : Minimal P x
⊢ Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} (f x)

Tactic:
exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx

Premises used: Iff.mpr, Minimal.prop, minimal_mem_image_monotone_iff
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} x
refine_2 :
  ∀ (y : α) (hy : P y)
    (h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} (f y)),
    f y ∈ f '' {x : α | Minimal P x}
⊢ x ∈ f '' {x : α | Minimal P x}

Tactic:
obtain ⟨y, hy, rfl⟩ := (mem_setOf_eq ▸ h).prop

Premises used: rfl
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
y : α
hy : P y
h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} (f y)
⊢ f y ∈ f '' {x : α | Minimal P x}

Tactic:
mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := setOf P) hy hf).1 h

Premises used: minimal_mem_image_monotone_iff, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
y : α
hy : P y
h : Membership.mem (γ := Set β) {x : β | Minimal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x} (f y)
⊢ f y ∈ f '' {x : α | Minimal P x}

Tactic:
exact mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := setOf P) hy hf).1 h

Premises used: minimal_mem_image_monotone_iff, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
P : α → Prop
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)
⊢ f '' {x : α | Minimal P x} = {x : β | Maximal (fun (x : β) ↦ ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

Tactic:
image_monotone_setOf_minimal (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)

Premises used: image_monotone_setOf_minimal, setOf, Maximal, OrderDual
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x : α | Minimal (fun (x : α) ↦ x ∈ s) x} = {x : β | Minimal (fun (x : β) ↦ x ∈ f '' s) x}

Tactic:
image_monotone_setOf_minimal hf

Premises used: image_monotone_setOf_minimal, Set.Mem, setOf, Set.image
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)
⊢ f '' {x : α | Minimal (fun (x : α) ↦ x ∈ s) x} = {x : β | Maximal (fun (x : β) ↦ x ∈ f '' s) x}

Tactic:
image_antitone_setOf_minimal hf

Premises used: Set.Mem, setOf, image_antitone_setOf_minimal, Set.image
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
hx : Minimal (fun (x : α) ↦ x ∈ s) x
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
a : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
ha : a ∈ s
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x

Tactic:
⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩

Premises used: Set.mem_range_self, Minimal.prop, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
refine_1 :
  ∀
    (h :
      Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
        ((f : (a : α) → β) x : β))
    (y : α) (hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y), y ≤ x → x ≤ y
refine_2 :
  ∀ (h : Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x) ⦃y : β⦄,
    (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) y →
      y ≤ (f : (a : α) → β) x → (f : (a : α) → β) x ≤ y
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x

Tactic:
refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) x : β)
y : α
hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y
refine_1 :
  LE.le.{u_3} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) →
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ y ≤ x → x ≤ y

Tactic:
rw [← f.le_iff_le, ← f.le_iff_le]

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) x : β)
y : α
hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) →
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
h.le_of_le ⟨hy, mem_range_self y⟩

Premises used: Set.mem_range_self, Minimal.le_of_le, And.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) x : β)
y : α
hy : (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) y
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) →
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
exact h.le_of_le ⟨hy, mem_range_self y⟩

Premises used: Set.mem_range_self, Minimal.le_of_le, And.intro
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
y : α
hyt : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
refine_2 : y ≤ x → x ≤ y
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) →
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
simp_rw [f.le_iff_le]

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
y : α
hyt : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
⊢ y ≤ x → x ≤ y

Tactic:
h.le_of_le hyt

Premises used: Minimal.le_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
y : α
hyt : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
⊢ y ≤ x → x ≤ y

Tactic:
exact h.le_of_le hyt

Premises used: Minimal.le_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β)
rw :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t ∩ range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) x : β)
rw₁ rw₂ :
  Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β)
⊢ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x

Tactic:
rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]

Premises used: OrderEmbedding.minimal_apply_mem_inter_range_iff, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ (⇑f : (a : α) → β) '' s
simp_rw :
  x ∈ s ∧
      Membership.mem (γ := Set α)
        (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y}) x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₁ :
  x ∈ s ∧
      Membership.mem (γ := Set α) {a : α | Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) a : β)} x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₂ :
  x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' t) x) x
simp_rw₃ :
  x ∈ s ∧ Minimal.{u_3} (α := β) (fun (x : β) ↦ x ∈ t) ((f : (a : α) → β) x : β) ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
simp_rw₄ :
  x ∈ s ∧ Minimal (fun (x : α) ↦ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x ↔
    Minimal (fun (x : α) ↦ x ∈ s ∧ Membership.mem (α := β) t ((f : (a : α) → β) x : β)) x
⊢ x ∈ s ∩ preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) {y : β | Minimal (fun (x : β) ↦ x ∈ t) y} ↔
    Minimal (fun (x : α) ↦ x ∈ s ∩ (⇑f : (a : α) → β) ⁻¹' t) x

Tactic:
simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]

Premises used: Set.mem_inter_iff, RelEmbedding.injective, minimal_and_iff_left_of_imp, HasSubset.Subset.trans, Set.image_subset_range, Set.mem_setOf_eq, OrderEmbedding.minimal_apply_mem_iff, Set.preimage_setOf_eq, Iff.mp, Function.Injective.mem_set_image, Set.mem_preimage
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
P : α → Prop
⊢ ∀ ⦃x y : α⦄, P x → P y → (LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Premises used: OrderIso.le_iff_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
P : α → Prop
h : ∀ (x x : β), P ((f.symm : (a : β) → α) x) ↔ ∃ (x₀ : α), P x₀ ∧ (f : (a : α) → β) x₀ = x
⊢ Eq.{u_3 + 1} (α := Set β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) {x : α | Minimal P x})
    {x : β | Minimal (fun (x : β) ↦ P ((f.symm : (a : β) → α) x)) x}

Tactic:
convert! _root_.image_monotone_setOf_minimal (f := f) (by simp [f.le_iff_le])

Premises used: image_monotone_setOf_minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
P : α → Prop
x x_1 : β
⊢ P ((f.symm : (a : β) → α) x_1) ↔ ∃ (x₀ : α), P x₀ ∧ (f : (a : α) → β) x₀ = x_1

Tactic:
aesop
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
f : OrderIso.{u_2, u_3} (↑s : Type u_2) (↑t : Type u_3)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
⊢ t =
    range.{u_3, u_2 + 1} (ι := (↑s : Type u_2))
      (Function.comp (β := { x : β // x ∈ t }) (Subtype.val (p := fun (x : β) ↦ x ∈ t))
        (⇑f : (a : (↑s : Type u_2)) → (↑t : Type u_3)))

Tactic:
simp
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
β : Type u_3
x : α
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
f : OrderIso.{u_2, u_3} (↑s : Type u_2) (↑t : Type u_3)
hx : Minimal (fun (x : α) ↦ x ∈ s) x
⊢ Minimal (fun (x : β) ↦ x ∈ t)
    (↑((f : (a : (↑s : Type u_2)) → (↑t : Type u_3)) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯)) : β)

Tactic:
simpa only [show t = range (Subtype.val ∘ f) by simp, mem_univ, minimal_true_subtype, hx,
    true_imp_iff, image_univ] using OrderEmbedding.minimal_mem_image
    (f.toOrderEmbedding.trans (OrderEmbedding.subtype (· ∈ t))) (s := univ) (x := ⟨x, hx.prop⟩)

Premises used: Set.image_univ, OrderIso.toOrderEmbedding, OrderEmbedding.minimal_mem_image, Membership.mem, true_imp_iff, Set.mem_univ, OrderEmbedding.subtype, RelEmbedding.trans, minimal_true_subtype
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
inst : PartialOrder α
a b : α
hab : a ≤ b
⊢ Minimal (fun (x : α) ↦ x ∈ Icc a b) x ↔ x = a

Tactic:
minimal_iff_eq ⟨rfl.le, hab⟩ (fun _ ↦ And.left)

Premises used: Eq.le, minimal_iff_eq, And.left, And.intro, rfl
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
inst : PartialOrder α
a b : α
hab : a < b
⊢ Minimal (fun (x : α) ↦ x ∈ Ico a b) x ↔ x = a

Tactic:
minimal_iff_eq ⟨rfl.le, hab⟩ (fun _ ↦ And.left)

Premises used: Eq.le, minimal_iff_eq, And.left, And.intro, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsWeakUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b

Tactic:
IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy

Premises used: IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsWeakUpperModularLattice α
a b : α
rw : b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Tactic:
rw [inf_comm, sup_comm]

Premises used: inf_comm, sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a

Tactic:
fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

Premises used: covBy_sup_of_inf_covBy_of_inf_covBy_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a

Tactic:
exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

Premises used: covBy_sup_of_inf_covBy_of_inf_covBy_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsWeakUpperModularLattice α
a b : α
⊢ IsWeakLowerModularLattice.{u_1} αᵒᵈ

Tactic:
⟨fun ha hb => (ha.ofDual.sup_of_inf_of_inf_left hb.ofDual).toDual⟩

Premises used: CovBy.toDual, CovBy.sup_of_inf_of_inf_left, IsWeakLowerModularLattice.mk, CovBy.ofDual
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → b ⋖ a ⊔ b

Tactic:
IsUpperModularLattice.covBy_sup_of_inf_covBy

Premises used: IsUpperModularLattice.covBy_sup_of_inf_covBy
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
rw : b ⊓ a ⋖ b → a ⋖ b ⊔ a
⊢ a ⊓ b ⋖ b → a ⋖ a ⊔ b

Tactic:
rw [sup_comm, inf_comm]

Premises used: inf_comm, sup_comm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ b → a ⋖ b ⊔ a

Tactic:
covBy_sup_of_inf_covBy_left

Premises used: covBy_sup_of_inf_covBy_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ b → a ⋖ b ⊔ a

Tactic:
exact covBy_sup_of_inf_covBy_left

Premises used: covBy_sup_of_inf_covBy_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
⊢ IsWeakUpperModularLattice α

Tactic:
⟨fun _ => CovBy.sup_of_inf_right⟩

Premises used: IsWeakUpperModularLattice.mk, CovBy.sup_of_inf_right
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsUpperModularLattice α
a b : α
⊢ IsLowerModularLattice.{u_1} αᵒᵈ

Tactic:
⟨fun h => h.ofDual.sup_of_inf_left.toDual⟩

Premises used: CovBy.toDual, IsLowerModularLattice.mk, CovBy.ofDual, CovBy.sup_of_inf_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
x z y : α
⊢ x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z

Tactic:
IsModularLattice.sup_inf_le_assoc_of_le y

Premises used: IsModularLattice.sup_inf_le_assoc_of_le