awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
⊢ LT.lt.{u_1} (α := WithTop α) (⊤ : WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ) ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤ : WithBot αᵒᵈ)

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
⊢ LT.lt (α := WithTop α) (⊤ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
    (↑a : WithBot αᵒᵈ) < (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) ⊤

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
⊢ (↑a : WithTop α) < (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ ↔
    LT.lt (α := WithBot αᵒᵈ) (⊥ : WithBot αᵒᵈ)
      ((WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α) : WithBot αᵒᵈ)

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : α
a_1 : αᵒᵈ
⊢ (↑a : WithTop α) < (WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) ↔
    (↑a_1 : WithBot αᵒᵈ) < (WithTop.toDual : (a : WithTop α) → WithBot αᵒᵈ) (↑a : WithTop α)

Tactic:
simp [lt_toDual]

Premises used: OrderDual.lt_toDual
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
x y : WithBot αᵒᵈ
bot :
  LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < ⊥
coe :
  ∀ (a : αᵒᵈ),
    LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
      y < (↑a : WithBot αᵒᵈ)
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) x : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
y : WithBot αᵒᵈ
bot :
  LT.lt.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥
bot₁ :
  ∀ (a : αᵒᵈ),
    LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
      (↑a : WithBot αᵒᵈ) < ⊥
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < ⊥

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
y : WithBot αᵒᵈ
a : αᵒᵈ
coe :
  LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    ⊥ < (↑a : WithBot αᵒᵈ)
coe₁ :
  ∀ (a_1 : αᵒᵈ),
    LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
        ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) : WithTop α) ↔
      (↑a_1 : WithBot αᵒᵈ) < (↑a : WithBot αᵒᵈ)
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) y : WithTop α) ↔
    y < (↑a : WithBot αᵒᵈ)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
⊢ LT.lt.{u_1} (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    LT.lt.{u_1} (α := WithBot αᵒᵈ) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α) ↔
    (↑a : WithBot αᵒᵈ) < ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) ⊥ : WithTop α) ↔
    ⊥ < (↑a : WithBot αᵒᵈ)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : LT α
a a_1 : αᵒᵈ
⊢ LT.lt (α := WithTop α) ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a : WithBot αᵒᵈ) : WithTop α)
      ((WithBot.ofDual : (a : WithBot αᵒᵈ) → WithTop α) (↑a_1 : WithBot αᵒᵈ) : WithTop α) ↔
    (↑a_1 : WithBot αᵒᵈ) < (↑a : WithBot αᵒᵈ)

Tactic:
simp
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
a₁ : ι
⊢ a₁ = a₁

Tactic:
rfl
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
motive : WithBotTop ι → Sort u_2
bot : motive ⊥
coe : (a : ι) → motive (WithBotTop.coe a)
top : motive ⊤
⊢ WithBotTop.rec (motive := motive) bot coe top ⊥ = bot

Tactic:
rfl

Premises used: WithBotTop.rec, rfl
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
motive : WithBotTop ι → Sort u_2
bot : motive ⊥
coe : (a : ι) → motive (WithBotTop.coe a)
top : motive ⊤
a : ι
⊢ WithBotTop.rec (motive := motive) bot coe top (WithBotTop.coe a) = coe a

Tactic:
rfl

Premises used: WithBotTop.rec, rfl
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
motive : WithBotTop ι → Sort u_2
bot : motive ⊥
coe : (a : ι) → motive (WithBotTop.coe a)
top : motive ⊤
⊢ WithBotTop.rec (motive := motive) bot coe top ⊤ = top

Tactic:
rfl

Premises used: WithBotTop.rec, rfl
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : LE ι
a b : ι
rw : coe a ≤ coe b ↔ (↑a : WithTop ι) ≤ (↑b : WithTop ι)
⊢ coe a ≤ coe b ↔ a ≤ b

Tactic:
rw [← WithTop.coe_le_coe (α := ι)]

Premises used: WithTop.coe_le_coe
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : LE ι
a b : ι
⊢ coe a ≤ coe b ↔ (↑a : WithTop ι) ≤ (↑b : WithTop ι)

Tactic:
WithBot.coe_le_coe

Premises used: WithBotTop.coe, WithBot.coe_le_coe
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : LE ι
a b : ι
⊢ coe a ≤ coe b ↔ (↑a : WithTop ι) ≤ (↑b : WithTop ι)

Tactic:
exact WithBot.coe_le_coe

Premises used: WithBot.coe_le_coe
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : LT ι
a b : ι
rw : coe a < coe b ↔ (↑a : WithTop ι) < (↑b : WithTop ι)
⊢ coe a < coe b ↔ a < b

Tactic:
rw [← WithTop.coe_lt_coe (α := ι)]

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : LT ι
a b : ι
⊢ coe a < coe b ↔ (↑a : WithTop ι) < (↑b : WithTop ι)

Tactic:
WithBot.coe_lt_coe

Premises used: WithBotTop.coe, WithBot.coe_lt_coe
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : LT ι
a b : ι
⊢ coe a < coe b ↔ (↑a : WithTop ι) < (↑b : WithTop ι)

Tactic:
exact WithBot.coe_lt_coe

Premises used: WithBot.coe_lt_coe
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : Preorder ι
⊢ StrictMono.{u_1, u_1} (α := ι) coe

Tactic:
WithBot.coe_strictMono.comp WithTop.coe_strictMono

Premises used: WithBotTop.coe, WithTop.coe_strictMono, StrictMono.comp, WithBot.coe_strictMono
-- Module: Mathlib.Order.WithBotTop
Goal:
ι : Type u_1
inst : Preorder ι
x x_1 : ι
h : x ≤ x_1
⊢ coe x ≤ coe x_1

Tactic:
simpa
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ (ub : α), ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this_1 : ∃ (ub : α), ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
rw : a ∈ insert a (maxChain r)
⊢ a ∈ maxChain r

Tactic:
rw [maxChain_spec.right this (subset_insert _ _)]

Premises used: maxChain_spec, And.right, Set.subset_insert
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ (ub : α), ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this_1 : ∃ (ub : α), ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)

Tactic:
mem_insert _ _

Premises used: Set.mem_insert
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ (ub : α), ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this_1 : ∃ (ub : α), ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)

Tactic:
exact mem_insert _ _

Premises used: Set.mem_insert
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
inst : Nonempty α
h : ∀ (c : Set α), IsChain r c → c.Nonempty → ∃ (ub : α), ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
⊢ ∃ (m : α), ∀ (a : α), r m a → r a m

Tactic:
exists_maximal_of_chains_bounded
    (fun c hc =>
      (eq_empty_or_nonempty c).elim
        (fun h => ⟨Classical.arbitrary α, fun x hx => (h ▸ hx : x ∈ (∅ : Set α)).elim⟩) (h c hc))
    trans

Premises used: exists_maximal_of_chains_bounded, False.elim, Eq.rec, Set.eq_empty_or_nonempty, Exists.intro, Classical.arbitrary, Or.elim
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → BddAbove c
⊢ ∃ (m : α), IsMax m

Tactic:
exists_maximal_of_chains_bounded h le_trans

Premises used: exists_maximal_of_chains_bounded, IsMax, le_trans
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → c.Nonempty → BddAbove c
⊢ ∃ (m : α), IsMax m

Tactic:
exists_maximal_of_nonempty_chains_bounded h le_trans

Premises used: exists_maximal_of_nonempty_chains_bounded, IsMax, le_trans
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set (↑s : Type u_1)
hc : IsChain (fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2) c
p : { x : α // x ∈ s }
hpc : p ∈ c
q : { x : α // x ∈ s }
hqc : q ∈ c
hpq : (↑p : α) ≠ (↑q : α)
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑p : α) (↑q : α) ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑q : α) (↑p : α)

Tactic:
hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set (↑s : Type u_1)
hc : IsChain (fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2) c
p : { x : α // x ∈ s }
hpc : p ∈ c
q : { x : α // x ∈ s }
hqc : q ∈ c
hpq : (↑p : α) ≠ (↑q : α)
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑p : α) (↑q : α) ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑q : α) (↑p : α)

Tactic:
exact hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
refine_2 :
  ∀ (H : ∃ (m : α), Maximal (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) m),
    ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
refine_1 :
  ∀ (c : Set α) (hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c),
    ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m

Tactic:
have H := zorn_le₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ (m : α), Maximal (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) m
refine_2 :
  ∀ (m : α)
    (hm : ∀ ⦃y : α⦄, (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) y → m ≤ y → y ≤ m)
    (hms : m ∈ s) (hxm : x ≤ m), ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m

Tactic:
rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ ⦃y : α⦄, (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) y → m ≤ y → y ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m

Tactic:
⟨m, hxm, hms, fun z hzs hmz => @hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ ⦃y : α⦄, (fun (x_1 : α) ↦ Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} x_1) y → m ≤ y → y ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) ↦ x ∈ s) m

Tactic:
exact ⟨m, hxm, hms, fun z hzs hmz => @hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
refine_1 :
  ∀ (hcs : Subset.{u_1} (α := Set α) ∅ {y : α | y ∈ s ∧ x ≤ y}) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅),
    ∃ (ub : α),
      Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ (z : α), Membership.mem (γ := Set α) ∅ z → z ≤ ub
refine_1₁ : ∀ (y : α) (hy : y ∈ c), ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : Subset.{u_1} (α := Set α) ∅ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅
⊢ ∃ (ub : α),
    Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ (z : α), Membership.mem (γ := Set α) ∅ z → z ≤ ub

Tactic:
⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩

Premises used: le_rfl, False.elim, And.intro, Exists.intro
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : Subset.{u_1} (α := Set α) ∅ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅
⊢ ∃ (ub : α),
    Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ (z : α), Membership.mem (γ := Set α) ∅ z → z ≤ ub

Tactic:
exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
refine_1 :
  ∀ (z : α) (hzs : z ∈ s) (hz : ∀ z_1 ∈ c, z_1 ≤ z),
    ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩

Premises used: And.left
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ z_1 ∈ c, z_1 ≤ z
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩

Premises used: And.right, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y : α | y ∈ s ∧ x ≤ y}
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ z_1 ∈ c, z_1 ≤ z
⊢ ∃ (ub : α), Membership.mem (γ := Set α) {y : α | y ∈ s ∧ x ≤ y} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
refine_2 :
  ∀ (m : α) (hxm : x ≤ m) (ham : m ∈ Ici a) (hm : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ Ici a) y → m ≤ y → y ≤ m),
    ∃ (m : α), x ≤ m ∧ IsMax m
refine_1 :
  ∀ (c : Set α) (hca : c ⊆ Ici a) (hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c) (y : α) (hy : y ∈ c),
    ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
⊢ ∃ (m : α), x ≤ m ∧ IsMax m

Tactic:
let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun (x : α) ↦ x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ (m : α), x ≤ m ∧ IsMax m

Tactic:
⟨m, hxm, fun z hmz => hm (ham.trans hmz) hmz⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun (x : α) ↦ x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ (m : α), x ≤ m ∧ IsMax m

Tactic:
exact ⟨m, hxm, fun z hmz => hm (ham.trans hmz) hmz⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
refine_1 : ∀ (ub : α) (hub : ∀ z ∈ c, z ≤ ub), ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
have ⟨ub, hub⟩ := ih c hca hc y hy
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
ub : α
hub : ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
⟨ub, (hca hy).trans (hub y hy), hub⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
inst : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
ub : α
hub : ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨ub, (hca hy).trans (hub y hy), hub⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
S : Set (Set α)
h : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
⊢ ∃ (m : Set α), Maximal (fun (x : Set α) ↦ x ∈ S) m

Tactic:
zorn_le₀ S h

Premises used: zorn_le₀
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
S : Set (Set α)
H : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
x : Set α
hx : x ∈ S
⊢ ∃ (m : Set α), x ⊆ m ∧ Maximal (fun (x : Set α) ↦ x ∈ S) m

Tactic:
zorn_le_nonempty₀ _ (fun _ cS hc y yc => H _ cS hc ⟨y, yc⟩) _ hx

Premises used: zorn_le_nonempty₀, Exists.intro
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
S : Set (Set α)
h : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
⊢ ∃ (m : Set α), Minimal (fun (x : Set α) ↦ x ∈ S) m

Tactic:
(@zorn_le₀ (Set α)ᵒᵈ _ S) fun c cS hc => h c cS hc.symm

Premises used: IsChain.symm, Set.Mem, zorn_le₀, OrderDual, Minimal
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
S : Set (Set α)
H : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
x : Set α
hx : x ∈ S
⊢ ∃ m ⊆ x, Minimal (fun (x : Set α) ↦ x ∈ S) m

Tactic:
@zorn_le_nonempty₀ (Set α)ᵒᵈ _ S (fun _ cS hc y yc => H _ cS hc.symm ⟨y, yc⟩) _ hx

Premises used: IsChain.symm, Set.Mem, zorn_le_nonempty₀, Exists.intro, OrderDual, Minimal
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
refine_2 :
  ∀
    (H :
      ∃ (m : Set α),
        c ⊆ m ∧ Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) m),
    ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
refine_1 :
  ∀ c_1 ⊆ {s : Set α | c ⊆ s ∧ IsChain r s},
    IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c_1 →
      c_1.Nonempty →
        ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} ub ∧ ∀ s ∈ c_1, s ⊆ ub
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M

Tactic:
have H := zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } ?_ c ⟨Subset.rfl, hc⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
H :
  ∃ (m : Set α),
    c ⊆ m ∧ Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) m
refine_2 :
  ∀ (M : Set α) (hcM : c ⊆ M)
    (hM : Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) M),
    ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M

Tactic:
obtain ⟨M, hcM, hM⟩ := H
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
M : Set α
hcM : c ⊆ M
hM : Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) M
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M

Tactic:
⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩

Premises used: Maximal.prop, HasSubset.Subset.trans, And.right, Maximal.eq_of_subset, And.intro, Exists.intro
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
M : Set α
hcM : c ⊆ M
hM : Maximal (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} x) M
⊢ ∃ (M : Set α), IsMaxChain r M ∧ c ⊆ M

Tactic:
exact ⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} ub ∧ ∀ s ∈ cs, s ⊆ ub

Tactic:
⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ =>
      Set.subset_sUnion_of_mem⟩

Premises used: Set.sUnion, Set.mem_sUnion_of_mem, And.left, And.intro, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
refine_1 : IsChain r (⋃₀ cs)
⊢ ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | c ⊆ s ∧ IsChain r s} ub ∧ ∀ s ∈ cs, s ⊆ ub

Tactic:
refine
    ⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ =>
      Set.subset_sUnion_of_mem⟩
-- Module: Mathlib.Order.Zorn
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s : Set α | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
refine_1 : ∀ (hsz : sy ∈ cs) (hzsz : z ∈ sy), r y z ∨ r z y
refine_1₁ : ∀ (hsseq : sy ≠ sz), r y z ∨ r z y
⊢ r y z ∨ r z y

Tactic:
obtain rfl | hsseq := eq_or_ne sy sz

Premises used: eq_or_ne, rfl