awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
x : X
⊢ Eq (α := X) ((↑((n.toSublocale.restrict : (a : X) → ↥n.toSublocale) x) : X) : X)
    ((↑(Subtype.mk (p := fun (x : X) ↦ x ∈ n.toSublocale) ((n : (a : X) → X) x) ⋯) : X) : X)

Tactic:
simpa [Sublocale.restrict, sInf_image, le_antisymm_iff (a := iInf _)] using
    ⟨iInf₂_le_of_le ⟨n x, x, rfl⟩ n.le_apply le_rfl, fun y hxy ↦ by simpa using n.monotone hxy⟩

Premises used: sInf_image, Sublocale.restrict, le_antisymm_iff
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
⊢ Function.LeftInverse (fun (s : Sublocale X) ↦ (OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus)
    fun (n : (Nucleus X)ᵒᵈ) ↦ Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n)

Tactic:
simp [Function.LeftInverse, Nucleus.ext_iff]

Premises used: Function.LeftInverse, Nucleus.ext_iff
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
h :
  ∀ (x : X),
    Membership.mem (γ := Sublocale X)
        ((fun (n : (Nucleus X)ᵒᵈ) ↦
            (Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n) : Sublocale X))
          ((fun (s : Sublocale X) ↦ ((OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus : (Nucleus X)ᵒᵈ))
            S))
        x ↔
      x ∈ S
⊢ (fun (n : (Nucleus X)ᵒᵈ) ↦
        (Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n) : Sublocale X))
      ((fun (s : Sublocale X) ↦ ((OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus : (Nucleus X)ᵒᵈ)) S) =
    S

Tactic:
ext x
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
⊢ (∃ (y : X), (↑((S.restrict : (a : X) → ↥S) y) : X) = x) → x ∈ S

Tactic:
simp +contextual [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
hx : x ∈ S
⊢ (↑((S.restrict : (a : X) → ↥S) x) : X) = x

Tactic:
simp [hx]
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
⊢ Membership.mem (γ := Sublocale X)
      ((fun (n : (Nucleus X)ᵒᵈ) ↦
          (Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n) : Sublocale X))
        ((fun (s : Sublocale X) ↦ ((OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus : (Nucleus X)ᵒᵈ))
          S))
      x ↔
    x ∈ S

Tactic:
simpa using ⟨by simp +contextual [eq_comm], fun hx ↦ ⟨x, by simp [hx]⟩⟩
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
⊢ ∀ {a b : (Nucleus X)ᵒᵈ},
    LE.le (α := Sublocale X)
        (({
                toFun := fun (n : (Nucleus X)ᵒᵈ) ↦
                  Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n),
                invFun := fun (s : Sublocale X) ↦ (OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (Nucleus X)ᵒᵈ) → Sublocale X)
            a :
          Sublocale X)
        (({
                toFun := fun (n : (Nucleus X)ᵒᵈ) ↦
                  Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n),
                invFun := fun (s : Sublocale X) ↦ (OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (Nucleus X)ᵒᵈ) → Sublocale X)
            b :
          Sublocale X) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
⊢ Eq.{u_1 + 1} (α := (n : Nucleus X) → Sublocale X) Nucleus.toSublocale
    (⇑nucleusIsoSublocale : (a : (Nucleus X)ᵒᵈ) → Sublocale X)

Tactic:
rfl

Premises used: Nucleus.toSublocale, OrderDual, rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
⊢ Eq.{u_1 + 1} (α := (S : Sublocale X) → Nucleus X) Sublocale.toNucleus
    (⇑(OrderIso.symm nucleusIsoSublocale) : (a : Sublocale X) → (Nucleus X)ᵒᵈ)

Tactic:
rfl

Premises used: Sublocale.toNucleus, rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
a : Sublocale X
s : Set (Sublocale X)
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
simp [← toNucleus_le_toNucleus,
    nucleusIsoSublocale.symm_eq_toNucleus, nucleusIsoSublocale.symm.map_sup,
    nucleusIsoSublocale.symm.map_sInf, sup_iInf_eq, nucleusIsoSublocale.symm.map_iInf]

Premises used: nucleusIsoSublocale, OrderIso.map_iInf, OrderIso.symm, Sublocale.toNucleus_le_toNucleus, OrderIso.map_sup, nucleusIsoSublocale.symm_eq_toNucleus, OrderIso.map_sInf, sup_iInf_eq
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ (n : ℕ),
    Eq (α := α) (succ^[n] ((OrderDual.ofDual : (a : αᵒᵈ) → α) b) : α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) a : α)

Tactic:
exists_succ_iterate_of_le h.ofDual

Premises used: LE.le.ofDual, IsSuccArchimedean.exists_succ_iterate_of_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
convert! exists_succ_iterate_of_le h.ofDual

Premises used: LE.le.ofDual, IsSuccArchimedean.exists_succ_iterate_of_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ (n : ℕ),
    Eq (α := α) (pred^[n] ((OrderDual.ofDual : (a : αᵒᵈ) → α) a) : α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
exists_pred_iterate_of_le h.ofDual

Premises used: IsPredArchimedean.exists_pred_iterate_of_le, LE.le.ofDual
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ (n : ℕ), succ^[n] a = b

Tactic:
convert! exists_pred_iterate_of_le h.ofDual

Premises used: IsPredArchimedean.exists_pred_iterate_of_le, LE.le.ofDual
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
h : a ≤ b
⊢ ∃ (n : ℕ), succ^[n] a = b

Tactic:
exists_succ_iterate_of_le h

Premises used: IsSuccArchimedean.exists_succ_iterate_of_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
⊢ (∃ (n : ℕ), succ^[n] a = b) ↔ a ≤ b

Tactic:
⟨?_, exists_succ_iterate_of_le⟩

Premises used: Iff.intro, IsSuccArchimedean.exists_succ_iterate_of_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
refine : (∃ (n : ℕ), succ^[n] a = b) → a ≤ b
⊢ (∃ (n : ℕ), succ^[n] a = b) ↔ a ≤ b

Tactic:
refine ⟨?_, exists_succ_iterate_of_le⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ succ^[n] a

Tactic:
id_le_iterate_of_id_le le_succ n a

Premises used: Order.le_succ, Function.id_le_iterate_of_id_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ succ^[n] a

Tactic:
exact id_le_iterate_of_id_le le_succ n a

Premises used: Order.le_succ, Function.id_le_iterate_of_id_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : α
hmn : m ≤ n
obtain : ∀ (n : ℕ) (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
⊢ P n hmn

Tactic:
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate

Premises used: LE.le.exists_succ_iterate
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
hmn : m ≤ Order.succ^[0] m
⊢ P (Order.succ^[0] m) hmn

Tactic:
rfl

Premises used: Nat.iterate
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
hmn : m ≤ Order.succ^[0] m
⊢ P (Order.succ^[0] m) hmn

Tactic:
exact rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
succ₁ : P (Order.succ (Order.succ^[n] m)) ⋯
⊢ P (Order.succ^[n + 1] m) hmn

Tactic:
simp_rw [Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ (Order.succ^[n] m)) ⋯

Tactic:
succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)

Premises used: Order.le_succ, Function.id_le_iterate_of_id_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ (Order.succ^[n] m)) ⋯

Tactic:
exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)

Premises used: Order.le_succ, Function.id_le_iterate_of_id_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
hmn : m ≤ Order.succ^[n] m
zero : ∀ (hmn : m ≤ Order.succ^[0] m), P (Order.succ^[0] m) hmn
succ₁ :
  ∀ (n : ℕ) (ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn) (hmn : m ≤ Order.succ^[n + 1] m),
    P (Order.succ^[n + 1] m) hmn
⊢ P (Order.succ^[n] m) hmn

Tactic:
induction n with
  | zero => exact rfl
  | succ n ih =>
    simp_rw [Function.iterate_succ_apply']
    exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
h : a ≤ b
obtain : ∀ (n : ℕ) (h : a ≤ succ^[n] a), p a ↔ p (succ^[n] a)
⊢ p a ↔ p b

Tactic:
obtain ⟨n, rfl⟩ := h.exists_succ_iterate

Premises used: LE.le.exists_succ_iterate, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)

Tactic:
Iterate.rec (fun b => p a ↔ p b) Iff.rfl (fun c hc => hc.trans (hsucc _)) n

Premises used: Iff.rfl, Iff, Iff.trans, Function.Iterate.rec
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)

Tactic:
exact Iterate.rec (fun b => p a ↔ p b) Iff.rfl (fun c hc => hc.trans (hsucc _)) n

Premises used: Iff.rfl, Iff, Iff.trans, Function.Iterate.rec
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
obtain : ∀ (n : ℕ) (h₁ : r ≤ succ^[n] r), succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r
⊢ v₁ ≤ v₂ ∨ v₂ ≤ v₁

Tactic:
obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate

Premises used: LE.le.exists_succ_iterate, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₂ : α
h₂ : r ≤ v₂
n : ℕ
h₁ : r ≤ succ^[n] r
obtain : ∀ (m : ℕ) (h₂ : r ≤ succ^[m] r), succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
⊢ succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r

Tactic:
obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate

Premises used: LE.le.exists_succ_iterate, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
        succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r)
    (h : ¬n ≤ m), succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
wlog :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
wlog h : n ≤ m
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
inr : succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
rw [Or.comm]

Premises used: Or.comm
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
inr : m ≤ n
⊢ succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r

Tactic:
apply this
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ m ≤ n

Tactic:
Nat.le_of_not_ge h

Premises used: Nat.le_of_not_ge
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ m ≤ n

Tactic:
exact Nat.le_of_not_ge h

Premises used: Nat.le_of_not_ge
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
h₁ : succ^[n] r ≤ succ^[m] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
left
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
h₁ : ∀ (k : ℕ) (h : n ≤ n + k), succ^[n] r ≤ succ^[n + k] r
⊢ succ^[n] r ≤ succ^[m] r

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
h₁ : succ^[n] r ≤ succ^[k] (succ^[n] r)
⊢ succ^[n] r ≤ succ^[n + k] r

Tactic:
rw [Nat.add_comm, Function.iterate_add, Function.comp_apply]

Premises used: Function.iterate_add, Function.comp_apply, Nat.add_comm
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[k] (succ^[n] r)

Tactic:
apply Order.le_succ_iterate

Premises used: Order.le_succ_iterate
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
rw : ¬v₂ ≤ v₁ → v₁ < v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
rw [Classical.or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
inl : ∀ (h : v₁ ≤ v₂), v₁ < v₂
inr : ∀ (h : v₂ ≤ v₁), v₁ < v₂
⊢ v₁ < v₂

Tactic:
rcases le_total_of_codirected h₁ h₂ with h | h

Premises used: le_total_of_codirected
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

Tactic:
apply lt_of_le_of_ne h (ne_of_not_le nh).symm

Premises used: Ne.symm, ne_of_not_le, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
contradiction
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
⊢ (∃ (n : ℕ), succ^[n] a = b) ∨ ∃ (n : ℕ), succ^[n] b = a

Tactic:
(le_total a b).imp exists_succ_iterate_of_le exists_succ_iterate_of_le

Premises used: le_total, IsSuccArchimedean.exists_succ_iterate_of_le, Or.imp
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
⊢ p a ↔ p b

Tactic:
(le_total a b).elim (Succ.rec_iff hsucc) fun h => (Succ.rec_iff hsucc h).symm

Premises used: le_total, Or.elim, Succ.rec_iff, Iff.symm
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
⊢ ∀ (a : α), f a ≤ m

Tactic:
have hm' : ∀ a, f a ≤ m := fun a ↦ hm <| Set.mem_range_self _
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
obtain : ∀ (a₀ : α), False
⊢ False

Tactic:
obtain ⟨a₀⟩ := ‹Nonempty α›

Premises used: Nonempty
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
⊢ ∃ (a : α), m < f a

Tactic:
this m (hm' a₀)
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
obtain : ∀ (a : α) (ha : m < f a), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
a : α
ha : m < f a
⊢ False

Tactic:
ha.not_ge (hm' a)

Premises used: LT.lt.not_ge
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
a : α
ha : m < f a
⊢ False

Tactic:
exact ha.not_ge (hm' a)

Premises used: LT.lt.not_ge
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
suffices : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
⊢ False

Tactic:
suffices ∀ b, f a₀ ≤ b → ∃ a, b < f a by
    obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
    exact ha.not_ge (hm' a)
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
⊢ ∀ (a : α), ∃ (a' : α), f a < f a'

Tactic:
have h : ∀ a, ∃ a', f a < f a' := fun a ↦ (exists_gt a).imp (fun a' h ↦ hf h)
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
rfl : ∃ (a : α), f a₀ < f a
succ : ∀ (n : β) (hmn : f a₀ ≤ n), (∃ (a : α), n < f a) → ∃ (a : α), Order.succ n < f a
⊢ ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a

Tactic:
apply Succ.rec
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
⊢ ∃ (a : α), f a₀ < f a

Tactic:
h a₀
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
⊢ ∃ (a : α), f a₀ < f a

Tactic:
exact h a₀
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
b : β
hmn : f a₀ ≤ b
a : α
hba : b < f a
⊢ ∃ (a : α), succ b < f a

Tactic:
(h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)

Premises used: Order.succ_le_of_lt, Exists.imp, LE.le.trans_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
b : β
hmn : f a₀ ≤ b
a : α
hba : b < f a
⊢ ∃ (a : α), succ b < f a

Tactic:
exact (h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)

Premises used: Order.succ_le_of_lt, Exists.imp, LE.le.trans_lt