awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
by_contra! : ∀ (this : ∀ (n : ℕ), ¬IsMax (a n)), False
⊢ ∃ (n : ℕ), IsMax (a n)

Tactic:
by_contra!
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
this : ∀ (n : ℕ), ¬IsMax (a n)
⊢ False

Tactic:
(RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf

Premises used: RelEmbedding.natGT, IsWellFounded.wf, RelEmbedding.not_wellFounded
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
this : ∀ (n : ℕ), ¬IsMax (a n)
⊢ False

Tactic:
exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf

Premises used: RelEmbedding.natGT, IsWellFounded.wf, RelEmbedding.not_wellFounded
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
⊢ ∃ (n : ℕ), IsMax (a n)

Tactic:
have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
H : ∃ (n : ℕ), IsMax (a n)
⊢ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩

Premises used: WellFounded.min_mem, wellFounded_lt, And.intro, Exists.intro, WellFounded.not_lt_min
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
H : ∃ (n : ℕ), IsMax (a n)
⊢ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
let let₁ let₂ : ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
let₃ :
  let a : ℕ → α := fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t;
  ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
let₄ :
  let a : ℕ → α := fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t;
  ∀ (cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)), ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
let₅ :
  let a : ℕ → α := fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t;
  ∀ (cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)) (H : ∃ (n : ℕ), IsMax (a n)),
    ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
⊢ ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
obtain :
  ∀ (a : ℕ → (↑S : Type u_2)) (h₁ : IsMin (a 0)) (n : ℕ) (h₂ : IsMax (a n)) (e : ∀ i < n, a i ⋖ a (i + 1)),
    ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
⊢ ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
obtain ⟨a, h₁, n, h₂, e⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT S

Premises used: exists_covBy_seq_of_wellFoundedLT_wellFoundedGT, Set.Elem
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → (↑S : Type u_2)
h₁ : IsMin (a 0)
n : ℕ
h₂ : IsMax (a n)
e : ∀ i < n, a i ⋖ a (i + 1)
⊢ (↑(a 0) : α) = (↑⊥ : α)

Tactic:
simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂

Premises used: isMax_iff_eq_top, Subtype.ext_iff, isMin_iff_eq_bot
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → (↑S : Type u_2)
h₁ : IsMin (a 0)
n : ℕ
h₂ : IsMax (a n)
e : ∀ i < n, a i ⋖ a (i + 1)
h₃ : (↑(a 0) : α) = (↑⊥ : α)
⊢ (↑(a n) : α) = (↑⊤ : α)

Tactic:
simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂

Premises used: isMax_iff_eq_top, Subtype.ext_iff, isMin_iff_eq_bot
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → (↑S : Type u_2)
n : ℕ
e : ∀ i < n, a i ⋖ a (i + 1)
h₁ : (↑(a 0) : α) = (↑⊥ : α)
h₂ : (↑(a n) : α) = (↑⊤ : α)
⊢ ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
⟨Subtype.val ∘ a, h₁, n, h₂, fun i hi ↦ ⟨(e i hi).1, fun c hc h ↦ (e i hi).2
    (c := ⟨c, (a i).2.1.trans hc.le, h.le.trans (a _).2.2⟩) hc h⟩⟩

Premises used: Function.comp, And.right, And.left, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → (↑S : Type u_2)
n : ℕ
e : ∀ i < n, a i ⋖ a (i + 1)
h₁ : (↑(a 0) : α) = (↑⊥ : α)
h₂ : (↑(a n) : α) = (↑⊤ : α)
⊢ ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
exact ⟨Subtype.val ∘ a, h₁, n, h₂, fun i hi ↦ ⟨(e i hi).1, fun c hc h ↦ (e i hi).2
    (c := ⟨c, (a i).2.1.trans hc.le, h.le.trans (a _).2.2⟩) hc h⟩⟩
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
F : Set P
nonempty : F.Nonempty
directed : DirectedOn (fun (x1 x2 : P) ↦ x1 ≥ x2) F
mem_of_le : ∀ {x y : P}, x ≤ y → x ∈ F → y ∈ F
⊢ IsPFilter F

Tactic:
⟨fun _ _ _ _ => mem_of_le ‹_› ‹_›, nonempty, directed⟩

Premises used: Order.IsIdeal.mk, Order.IsPFilter
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
F : PFilter P
⊢ IsPFilter (↑F : Set P)

Tactic:
F.dual.isIdeal

Premises used: Set.Mem, Order.IsPFilter, setOf, Order.PFilter.dual, Set.preimage, Order.Ideal.isIdeal
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
F : PFilter P
⊢ (↑F : Set P).Nonempty

Tactic:
F.dual.nonempty

Premises used: Set.Mem, setOf, Order.PFilter.dual, Set.preimage, Order.Ideal.nonempty, OrderDual
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
F : PFilter P
⊢ DirectedOn (fun (x1 x2 : P) ↦ x1 ≥ x2) (↑F : Set P)

Tactic:
F.dual.directed

Premises used: Set.Mem, setOf, Order.PFilter.dual, Order.Ideal.directed, Set.preimage, OrderDual
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
x y : P
F : PFilter P
⊢ x ≤ y → x ∈ F → y ∈ F

Tactic:
fun h => F.dual.lower h

Premises used: Order.Ideal.lower, Set.Mem, setOf, Order.PFilter.dual, Set.preimage
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
s t : PFilter P
h : (↑s : Set P) = (↑t : Set P)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
x : P
F G : PFilter P
hx : x ∈ F
hle : F ≤ G
⊢ x ∈ G

Tactic:
hle hx
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
x : P
I : Ideal Pᵒᵈ
⊢ x ∈ { dual := I : PFilter P } ↔ Membership.mem (α := Pᵒᵈ) I ((toDual : (a : P) → Pᵒᵈ) x : Pᵒᵈ)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
x : P
F : PFilter P
⊢ principal x ≤ F ↔ x ∈ F

Tactic:
Ideal.principal_le_iff (x := toDual x)

Premises used: Set.Mem, setOf, Order.Ideal.principal_le_iff, Set.preimage, Set.Iic, OrderDual
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
x y : P
⊢ Membership.mem (γ := PFilter P) (principal y) x ↔ y ≤ x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.Iic
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
p q : P
⊢ LE.le (α := PFilter P) (principal q) (principal p) ↔ p ≤ q

Tactic:
simp
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
⊢ Antitone.{u_1, u_1} (α := P) (β := PFilter P) principal

Tactic:
fun _ _ =>
  principal_le_principal_iff.2

Premises used: Iff.mpr, Antitone, Order.PFilter.principal_le_principal_iff
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : Preorder P
inst_1 : OrderTop P
F : PFilter P
⊢ ⊤ ∈ F

Tactic:
Ideal.bot_mem _

Premises used: Set.Mem, setOf, Set.preimage, Order.Ideal.bot_mem
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : SemilatticeInf P
x y : P
F : PFilter P
hx : x ∈ F
hy : y ∈ F
⊢ x ⊓ y ∈ F

Tactic:
Ideal.sup_mem hx hy

Premises used: Set.Mem, setOf, Set.preimage, Order.Ideal.sup_mem
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : SemilatticeInf P
x y : P
F : PFilter P
⊢ x ⊓ y ∈ F ↔ x ∈ F ∧ y ∈ F

Tactic:
Ideal.sup_mem_iff

Premises used: Set.Mem, setOf, Set.preimage, Order.Ideal.sup_mem_iff
-- Module: Mathlib.Order.PFilter
Goal:
P : Type u_1
inst : CompleteSemilatticeInf P
x : P
F : (PFilter P)ᵒᵈ
⊢ (fun (x : P) ↦ ((toDual : (a : PFilter P) → (PFilter P)ᵒᵈ) (principal x) : (PFilter P)ᵒᵈ)) x ≤ F ↔
    x ≤ (fun (F : (PFilter P)ᵒᵈ) ↦ sInf (↑((ofDual : (a : (PFilter P)ᵒᵈ) → PFilter P) F : PFilter P) : Set P)) F

Tactic:
simp only [le_sInf_iff, SetLike.mem_coe, toDual_le, SetLike.le_def, mem_principal]

Premises used: le_sInf_iff, SetLike.le_def, OrderDual.toDual_le, SetLike.mem_coe, Order.PFilter.mem_principal
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
simp : ∀ (x_1 : β), x_1 ∈ f x → a ∈ g x x_1 → ∃ (a_3 : β), a_3 ∈ f y ∧ a ∈ g y a_3
⊢ Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) x) a →
    Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) y) a

Tactic:
simp only [and_imp, Part.mem_bind_iff, exists_imp]

Premises used: Part.mem_bind_iff, and_imp, exists_imp
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f x → a ∈ g x x_1 → ∃ (a_3 : β), a_3 ∈ f y ∧ a ∈ g y a_3

Tactic:
fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f x → a ∈ g x x_1 → ∃ (a_3 : β), a_3 ∈ f y ∧ a ∈ g y a_3

Tactic:
exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
simp : ∀ (x_1 : β), x_1 ∈ f y → a ∈ g y x_1 → ∃ (a_3 : β), a_3 ∈ f x ∧ a ∈ g x a_3
⊢ Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) y) a →
    Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) x) a

Tactic:
simp only [and_imp, Part.mem_bind_iff, exists_imp]

Premises used: Part.mem_bind_iff, and_imp, exists_imp
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f y → a ∈ g y x_1 → ∃ (a_3 : β), a_3 ∈ f x ∧ a ∈ g x a_3

Tactic:
fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f y → a ∈ g y x_1 → ∃ (a_3 : β), a_3 ∈ f x ∧ a ∈ g x a_3

Tactic:
exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : β → γ
g : α → Part β
hg : Monotone g
⊢ Monotone.{u_1, u_3} (β := Part γ) fun (x : α) ↦ map f (g x)

Tactic:
simpa only [← bind_some_eq_map] using hg.partBind monotone_const

Premises used: monotone_const, Part.bind_some_eq_map, Monotone.partBind
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : β → γ
g : α → Part β
hg : Antitone g
⊢ Antitone.{u_1, u_3} (β := Part γ) fun (x : α) ↦ map f (g x)

Tactic:
simpa only [← bind_some_eq_map] using hg.partBind antitone_const

Premises used: Part.bind_some_eq_map, antitone_const, Antitone.partBind
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
inst : Preorder α
β γ : Type u_4
f : α → Part (β → γ)
g : α → Part β
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u_1, u_4} (β := Part γ) fun (x : α) ↦ f x <*> g x

Tactic:
simpa only [seq_eq_bind_map] using hf.partBind <| Monotone.of_apply₂ fun _ ↦ hg.partMap

Premises used: Monotone.partMap, Monotone.partBind, Monotone.of_apply₂, seq_eq_bind_map
-- Module: Mathlib.Order.Part
Goal:
α : Type u_1
inst : Preorder α
β γ : Type u_4
f : α → Part (β → γ)
g : α → Part β
hf : Antitone f
hg : Antitone g
⊢ Antitone.{u_1, u_4} (β := Part γ) fun (x : α) ↦ f x <*> g x

Tactic:
simpa only [seq_eq_bind_map] using hf.partBind <| Antitone.of_apply₂ fun _ ↦ hg.partMap

Premises used: Antitone.partMap, Antitone.of_apply₂, Antitone.partBind, seq_eq_bind_map
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (partialSups f : (a : ι) → α) i = (Iic i).sup' ⋯ f

Tactic:
rfl

Premises used: WithBot.unbot, Finset.sup', rfl
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
rw : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
rw₁ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)

Tactic:
rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]

Premises used: partialSups_apply, Finset.comp_sup'_eq_sup'_comp, Finset.sup'_eq_sup
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).inf (p ∘ f) ↔ ∀ j ≤ i, p (f j)

Tactic:
simp [Finset.inf_eq_iInf]

Premises used: Finset.inf_eq_iInf
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
rw : (p x ∧ p y) = max (p x) (p y)
⊢ p (x ⊔ y) = max (p x) (p y)

Tactic:
rw [hp]
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ (p x ∧ p y) = max (p x) (p y)

Tactic:
rfl
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
rw : p ((Iic i).sup' ⋯ f) ↔ ∀ j ≤ i, p (f j)
rw₁ : (Iic i).sup' ⋯ (p ∘ f) ↔ ∀ j ≤ i, p (f j)
rw₂ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
rw₃ : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
rw₄ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
rw₅ : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
rw₆ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
rw₇ : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
rw₈ rw₉ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)

Tactic:
classical
  rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl

Premises used: partialSups_apply, Function.comp, Finset.comp_sup'_eq_sup'_comp, Finset.Iic, Finset.inf_eq_iInf, Finset.inf, Finset.sup'_eq_sup
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
a : α
⊢ (partialSups f : (a : ι) → α) i ≤ a ↔ ∀ j ≤ i, f j ≤ a

Tactic:
partialSups_iff_forall (· ≤ a) sup_le_iff

Premises used: LE.le, sup_le_iff, partialSups_iff_forall
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i j : ι
h : i ≤ j
⊢ f i ≤ (partialSups f : (a : ι) → α) j

Tactic:
partialSups_le_iff.1 le_rfl i h

Premises used: le_rfl, Iff.mp, partialSups_le_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ f ≤ (⇑(partialSups f) : (a : ι) → α)

Tactic:
fun _ => le_partialSups_of_le f le_rfl

Premises used: le_rfl, le_partialSups_of_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
a : α
w : ∀ j ≤ i, f j ≤ a
⊢ (partialSups f : (a : ι) → α) i ≤ a

Tactic:
partialSups_le_iff.2 w

Premises used: Iff.mpr, partialSups_le_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
h :
  ∀ (a : α),
    Membership.mem (γ := Set α) (upperBounds (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α))) a ↔
      a ∈ upperBounds (Set.range f)
⊢ upperBounds (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α)) = upperBounds (Set.range f)

Tactic:
ext a
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
a : α
h : (∀ (i j : ι), j ≤ i → f j ≤ a) ↔ ∀ (i : ι), f i ≤ a
⊢ Membership.mem (γ := Set α) (upperBounds (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α))) a ↔
    a ∈ upperBounds (Set.range f)

Tactic:
simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]

Premises used: Set.forall_mem_range, partialSups_le_iff, mem_upperBounds
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ (∀ (i j : ι), j ≤ i → f j ≤ a) ↔ ∀ (i : ι), f i ≤ a

Tactic:
⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩

Premises used: le_rfl, Iff.intro
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ (∀ (i j : ι), j ≤ i → f j ≤ a) ↔ ∀ (i : ι), f i ≤ a

Tactic:
exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ BddAbove.{u_1} (α := α) (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α)) ↔ BddAbove (Set.range f)

Tactic:
.of_eq <| congr_arg Set.Nonempty <| upperBounds_range_partialSups f

Premises used: Iff.of_eq, congr_arg, Set.Nonempty, upperBounds_range_partialSups
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
hf : Monotone f
⊢ (⇑(partialSups f) : (a : ι) → α) = f

Tactic:
funext fun i ↦ le_antisymm (partialSups_le _ _ _ (@hf · i)) (le_partialSups _ _)

Premises used: partialSups_le, funext, le_antisymm, le_partialSups
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
⊢ Monotone (α := ι → α) (β := ι →o α) partialSups

Tactic:
fun _ _ h _ ↦ partialSups_le_iff.2 fun j hj ↦ (h j).trans (le_partialSups_of_le _ hj)

Premises used: Iff.mpr, Monotone, le_partialSups_of_le, LE.le.trans, partialSups_le_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ Monotone.{u_3, u_1} (α := ι) (β := α) (⇑(partialSups f) : (a : ι) → α)

Tactic:
fun i _ hnm ↦ partialSups_le f i _ (fun _ hm'n ↦ le_partialSups_of_le _ (hm'n.trans hnm))

Premises used: Monotone, le_partialSups_of_le, partialSups, partialSups_le, LE.le.trans, DFunLike.coe