awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this_2 : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ x = y

Tactic:
exact antisymm (h _ _ h₂s₁) h₂s₂

Premises used: antisymm
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this_2 : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ x = y

Tactic:
apply antisymm h₂s₁ (h _ _ h₂s₂)

Premises used: antisymm
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
⊢ ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
have hS : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub := by
    rintro c hc₁ hc₂ s hs
    haveI := (hc₁ hs).1
    refine ⟨sSup c, ?_, fun z hz => le_sSup hz⟩
    refine
        { refl := ?_
          trans := ?_
          antisymm := ?_ } <;>
      simp_rw [binary_relation_sSup_iff]
    · intro x
      exact ⟨s, hs, refl x⟩
    · rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
      haveI : IsPartialOrder _ _ := hc₁ h₁s₁
      haveI : IsPartialOrder _ _ := hc₁ h₁s₂
      rcases hc₂.total h₁s₁ h₁s₂ with h | h
      · exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩
      · exact ⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩
    · rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
      haveI : IsPartialOrder _ _ := hc₁ h₁s₁
      haveI : IsPartialOrder _ _ := hc₁ h₁s₂
      rcases hc₂.total h₁s₁ h₁s₂ with h | h
      · exact antisymm (h _ _ h₂s₁) h₂s₂
      · apply antisymm h₂s₁ (h _ _ h₂s₂)
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
obtain :
  ∀ (s : α → α → Prop) (hrs : r ≤ s) (hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s),
    ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s

Tactic:
obtain ⟨s, hrs, hs⟩ := zorn_le_nonempty₀ S hS r ‹_›

Premises used: zorn_le_nonempty₀
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
⊢ IsPartialOrder α s

Tactic:
haveI : IsPartialOrder α s := hs.prop
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s

Tactic:
⟨s,
    { total := ?_, refl := hs.1.refl, trans := hs.1.trans, antisymm := hs.1.antisymm }, hrs⟩

Premises used: IsLinearOrder.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
refine : ∀ (a b : α), s a b ∨ s b a
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s

Tactic:
refine ⟨s,
    { total := ?_, refl := hs.1.refl, trans := hs.1.trans, antisymm := hs.1.antisymm }, hrs⟩
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
by_contra! : ∀ (h : ¬s x y ∧ ¬s y x), False
⊢ s x y ∨ s y x

Tactic:
by_contra! h
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
rw : ∀ (h : ¬s' x y ∧ ¬s' y x), False
rw₁ : s' ∈ S
⊢ False

Tactic:
rw [hs.eq_of_le (y := s') ?_ fun _ _ ↦ Or.inl] at h

Premises used: Maximal.eq_of_le, Or.inl
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

Tactic:
apply h.1 (Or.inr ⟨refl _, refl _⟩)

Premises used: And.left, And.intro, refl, Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S

Tactic:
{ refl := fun x ↦ Or.inl (refl _)
      trans := ?_
      antisymm := ?_ }

Premises used: Set.Mem, setOf, IsPartialOrder.mk
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
refine_1 : ∀ (a b c : α), s' a b → s' b c → s' a c
refine_2 : ∀ (a b : α), s' a b → s' b a → a = b
⊢ s' ∈ S

Tactic:
refine
    { refl := fun x ↦ Or.inl (refl _)
      trans := ?_
      antisymm := ?_ }
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bc : s b c
⊢ s' a c

Tactic:
Or.inl (_root_.trans ab bc)

Premises used: trans, Or.inl
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bc : s b c
⊢ s' a c

Tactic:
exact Or.inl (_root_.trans ab bc)

Premises used: trans, Or.inl
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
Or.inr ⟨_root_.trans ab bx, yc⟩

Premises used: trans, And.intro, Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
exact Or.inr ⟨_root_.trans ab bx, yc⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c

Tactic:
Or.inr ⟨ax, _root_.trans yb bc⟩

Premises used: trans, And.intro, Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c

Tactic:
exact Or.inr ⟨ax, _root_.trans yb bc⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
Or.inr ⟨ax, yc⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
exact Or.inr ⟨ax, yc⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b

Tactic:
antisymm ab ba

Premises used: antisymm
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b

Tactic:
exact antisymm ab ba

Premises used: antisymm
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
(h.2 (_root_.trans ya (_root_.trans ab bx))).elim

Premises used: trans, False.elim, And.right
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
exact (h.2 (_root_.trans ya (_root_.trans ab bx))).elim

Premises used: trans, False.elim, And.right
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

Tactic:
(h.2 (_root_.trans yb (_root_.trans ba ax))).elim

Premises used: trans, False.elim, And.right
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

Tactic:
exact (h.2 (_root_.trans yb (_root_.trans ba ax))).elim

Premises used: trans, False.elim, And.right
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
(h.2 (_root_.trans yb bx)).elim

Premises used: trans, False.elim, And.right
-- Module: Mathlib.Order.Extension.Linear
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b

Tactic:
exact (h.2 (_root_.trans yb bx)).elim

Premises used: trans, False.elim, And.right
-- Module: Mathlib.Order.Extension.Well
Goal:
α_1 : Type u
r_1 : α_1 → α_1 → Prop
α : Type u
r : α → α → Prop
inst : IsWellFounded α r
⊢ IsWellFounded α LT.lt

Tactic:
⟨InvImage.wf (fun a : α => (rank r a, embeddingToCardinal a)) <|
    Ordinal.lt_wf.prod_lex Cardinal.lt_wf⟩

Premises used: IsWellFounded.mk, embeddingToCardinal, Prod.mk, Cardinal.lt_wf, Ordinal.lt_wf, InvImage.wf, DFunLike.coe, WellFounded.prod_lex, IsWellFounded.rank
-- Module: Mathlib.Order.Extension.Well
Goal:
α : Type u
r : α → α → Prop
inst : IsWellFounded α r
⊢ ∃ (s : α → α → Prop), r ≤ s ∧ IsWellOrder α s

Tactic:
⟨(wellOrderExtension r).lt, fun _ _ h => Prod.Lex.left _ _ (rank_lt_of_rel h), ⟨⟩⟩

Premises used: IsWellOrder.mk, IsWellFounded.rank_lt_of_rel, embeddingToCardinal, And.intro, LT.lt, Exists.intro, Prod.Lex.left, DFunLike.coe
-- Module: Mathlib.Order.Extension.Well
Goal:
α : Type u
r : α → α → Prop
inst : LT α
inst_1 : WellFoundedLT α
⊢ WellFoundedLT.{u} (WellOrderExtension α)

Tactic:
IsWellFounded.wellOrderExtension.isWellFounded_lt (α := α) (· < ·)

Premises used: IsWellFounded.wellOrderExtension.isWellFounded_lt, LT.lt, WellOrderExtension
-- Module: Mathlib.Order.Extension.Well
Goal:
α : Type u
inst : Preorder α
inst_1 : WellFoundedLT α
⊢ StrictMono.{u, u} (α := α) (β := WellOrderExtension α) (⇑toWellOrderExtension : (a : α) → WellOrderExtension α)

Tactic:
fun _ _ h =>
  Prod.Lex.left _ _ <| IsWellFounded.rank_lt_of_rel h

Premises used: StrictMono, IsWellFounded.rank_lt_of_rel, embeddingToCardinal, toWellOrderExtension, Prod.Lex.left, DFunLike.coe
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
⊢ comap.{0, u_2} (β := R) Nat.cast atTop = atTop

Tactic:
comap_embedding_atTop (fun _ _ => Nat.cast_le) exists_nat_ge

Premises used: exists_nat_ge, Filter.comap_embedding_atTop, Nat.cast_le
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℕ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto f l atTop

Tactic:
tendsto_atTop_embedding (fun _ _ => Nat.cast_le) exists_nat_ge

Premises used: exists_nat_ge, Filter.tendsto_atTop_embedding, Nat.cast_le
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
β : Type u_3
f : ℕ → β
l : Filter β
⊢ Tendsto (fun (x : ℕ+) ↦ f (↑x : ℕ)) atTop l ↔ Tendsto f atTop l

Tactic:
tendsto_comp_val_Ioi_atTop

Premises used: PNat.val, Set.Ioi, Set.Mem, Filter.tendsto_comp_val_Ioi_atTop, Nat.lt, PNat
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
β : Type u_3
f : ℕ → β
l : Filter β
⊢ Tendsto (fun (x : ℕ+) ↦ f (↑x : ℕ)) atTop l ↔ Tendsto f atTop l

Tactic:
exact tendsto_comp_val_Ioi_atTop

Premises used: Filter.tendsto_comp_val_Ioi_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
⊢ Tendsto.{0, u_2} (β := R) Nat.cast atTop atTop

Tactic:
Nat.mono_cast.tendsto_atTop_atTop exists_nat_ge

Premises used: Nat.mono_cast, exists_nat_ge, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
⊢ Tendsto PNat.val atTop atTop

Tactic:
tendsto_atTop_atTop_of_monotone (fun _ _ h ↦ h) fun a ↦ ⟨Nat.succPNat a, Nat.le_succ a⟩

Premises used: Nat.le_succ, Filter.tendsto_atTop_atTop_of_monotone, Nat.succPNat, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℕ) in atTop, p (↑n : R)

Tactic:
tendsto_natCast_atTop_atTop.eventually h

Premises used: tendsto_natCast_atTop_atTop, Filter.Tendsto.eventually
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
⊢ comap.{0, u_2} (β := R) Int.cast atTop = atTop

Tactic:
comap_embedding_atTop (fun _ _ => Int.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge r; ⟨n, mod_cast hn⟩

Premises used: Int.cast, Int.cast_natCast, Int.cast_le, congrArg, cast, Exists, exists_nat_ge, _private.0.Int.comap_cast_atTop.match_1, LE.le, Nat.cast, Exists.intro, Filter.comap_embedding_atTop, Eq.symm
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
r : R
n : ℕ
hn : -r ≤ (↑n : R)
⊢ (↑(-(↑n : ℤ)) : R) ≤ r

Tactic:
simpa [neg_le] using hn

Premises used: neg_le
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℤ
l : Filter α
rw :
  Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto.{u_1, u_2} (β := R) (Int.cast ∘ f) l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]

Premises used: Int.comap_cast_atTop, Filter.tendsto_comap_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atTop ↔ Tendsto.{u_1, u_2} (β := R) (Int.cast ∘ f) l atTop

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℤ
l : Filter α
rw :
  Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto.{u_1, u_2} (β := R) (Int.cast ∘ f) l atBot
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto f l atBot

Tactic:
rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, Int.comap_cast_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ (↑(f n) : R)) l atBot ↔ Tendsto.{u_1, u_2} (β := R) (Int.cast ∘ f) l atBot

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
⊢ Tendsto.{0, u_2} (β := R) Int.cast atTop atTop

Tactic:
tendsto_intCast_atTop_iff.2 tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, tendsto_intCast_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
R : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
rw : ∀ᶠ (n : ℤ) in Filter.comap.{0, u_2} (β := R) Int.cast atTop, p (↑n : R)
⊢ ∀ᶠ (n : ℤ) in atTop, p (↑n : R)

Tactic:
rw [← Int.comap_cast_atTop (R := R)]

Premises used: Int.comap_cast_atTop