awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMinOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictAnti f
⊢ ¬BddAbove (Set.range f)

Tactic:
hf.dual_right.not_bddBelow_range_of_isPredArchimedean

Premises used: Set.Mem, setOf, StrictMono.not_bddBelow_range_of_isPredArchimedean, upperBounds, BddAbove, StrictAnti.dual_right, OrderDual
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b : α
⊢ ∀ (h : a ≤ b), ∃ (n : ℕ), pred^[n] b = a

Tactic:
WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a)
      h.wf ?_ b

Premises used: IsWellFounded.wf, WellFounded.fix
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b : α
refine :
  ∀ (x : α),
    (∀ y < x, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y) → (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) x
⊢ ∀ (h : a ≤ b), ∃ (n : ℕ), pred^[n] b = a

Tactic:
refine WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a)
      h.wf ?_ b

Premises used: IsWellFounded.wf, WellFounded.fix
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
hab : a ≤ b
⊢ a = b ∨ a < b

Tactic:
replace hab := eq_or_lt_of_le hab
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
hab : a = b ∨ a < b
inl : ∀ (ih : ∀ y < a, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y), ∃ (n : ℕ), pred^[n] a = a
inr : ∀ (hab : a < b), ∃ (n : ℕ), pred^[n] b = a
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
rcases hab with (rfl | hab)

Premises used: rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b : α
ih : ∀ y < a, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
⊢ ∃ (n : ℕ), pred^[n] a = a

Tactic:
⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b : α
ih : ∀ y < a, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
⊢ ∃ (n : ℕ), pred^[n] a = a

Tactic:
exact ⟨0, rfl⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
hab : a < b
inr : ∀ (hb : pred b = b), ∃ (n : ℕ), pred^[n] b = a
inr₁ : ∀ (hb : pred b < b), ∃ (n : ℕ), pred^[n] b = a
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
rcases eq_or_lt_of_le (pred_le b) with hb | hb

Premises used: eq_or_lt_of_le, Order.pred_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
hab : a < b
hb : pred b = b
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
cases (min_of_le_pred hb.ge).not_lt hab

Premises used: Eq.ge, Order.min_of_le_pred, IsMin.not_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
inr : ∀ (k : ℕ) (hk : pred^[k] (pred b) = a), ∃ (n : ℕ), pred^[n] b = a
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab)

Premises used: Order.le_pred_of_lt, Order.pred
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
⟨k + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
inr : pred^[k + 1] b = a
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
refine ⟨k + 1, ?_⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
inr : pred^[k] (pred^[1] b) = a
inr₁ : pred^[k] (pred b) = a
inr₂ inr₃ : a = a
⊢ pred^[k + 1] b = a

Tactic:
rw [iterate_add_apply, iterate_one, hk]

Premises used: Function.iterate_add_apply, Function.iterate_one
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedGT α
inst_1 : SuccOrder α
⊢ IsPredArchimedean.{u_1} αᵒᵈ

Tactic:
infer_instance
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
p : α → Prop
hbot : p ⊥
hsucc : ∀ (a : α), p a → p (succ a)
a : α
⊢ p a

Tactic:
Succ.rec hbot (fun x _ h => hsucc x h) (bot_le : ⊥ ≤ a)

Premises used: Succ.rec, bot_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)

Tactic:
⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩

Premises used: Order.succ_ne_bot, SuccOrder.succ, Iff.intro
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
refine : ∀ (h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)) (i : α) (hi : i ≠ ⊥), P i
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)

Tactic:
refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
i : α
hi : i ≠ ⊥
obtain : ∀ (j : ℕ) (hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥), P (Order.succ^[j] ⊥)
⊢ P i

Tactic:
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)

Premises used: IsSuccArchimedean.exists_succ_iterate_of_le, bot_le, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
a : j ≠ 0
⊢ 0 < j

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
a : ∀ (hi : j = 0), Eq.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
⊢ j ≠ 0

Tactic:
contrapose hi
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : j = 0
⊢ Eq.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥

Tactic:
simp [hi]
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
have : ∀ (hj : 0 < j), P (Order.succ^[j] ⊥)
⊢ P (Order.succ^[j] ⊥)

Tactic:
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi]
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
hj : 0 < j
rw : P (Order.succ^[j.pred.succ] ⊥)
⊢ P (Order.succ^[j] ⊥)

Tactic:
rw [← Nat.succ_pred_eq_of_pos hj]

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
hj : 0 < j
simp : P (Order.succ (Order.succ^[j.pred] ⊥))
⊢ P (Order.succ^[j.pred.succ] ⊥)

Tactic:
simp only [Function.iterate_succ', Function.comp_apply]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
hj : 0 < j
⊢ P (Order.succ (Order.succ^[j.pred] ⊥))

Tactic:
apply h
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
hS : BddAbove S
hS' : S.Nonempty
obtain : ∀ (m : X) (hm : m ∈ upperBounds S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x

Tactic:
obtain ⟨m, hm⟩ := hS
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
hS' : S.Nonempty
m : X
hm : m ∈ upperBounds S
obtain : ∀ (n : X) (hn : n ∈ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x

Tactic:
obtain ⟨n, hn⟩ := hS'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
pos : ∀ (hm' : m ∈ S), ∃ (x : X), IsGreatest S x
neg : ∀ (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x

Tactic:
by_cases hm' : m ∈ S
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ (x : X), IsGreatest S x

Tactic:
⟨_, hm', hm⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ (x : X), IsGreatest S x

Tactic:
exact ⟨_, hm', hm⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ n ≤ m

Tactic:
have hn' := hm hn
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
hn' : n ≤ m
neg : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x

Tactic:
revert hn hm hm'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x

Tactic:
Succ.rec ?_ ?_ hn'

Premises used: Succ.rec
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
neg : ∀ (hm : n ∈ upperBounds S) (hn : n ∈ S) (hm' : n ∉ S), ∃ (x : X), IsGreatest S x
neg₁ :
  ∀ (n_1 : X) (hmn : n ≤ n_1),
    (∀ (hm : n_1 ∈ upperBounds S) (hn : n ∈ S) (hm' : n_1 ∉ S), ∃ (x : X), IsGreatest S x) →
      ∀ (hm : succ n_1 ∈ upperBounds S) (hn : n ∈ S) (hm' : succ n_1 ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x

Tactic:
refine Succ.rec ?_ ?_ hn'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (hm : n ∈ upperBounds S) (hn : n ∈ S) (hm' : n ∉ S), ∃ (x : X), IsGreatest S x

Tactic:
simp +contextual
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
neg :
  n ≤ m →
    (∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x) →
      ∀ (hm : succ m ∈ upperBounds S) (hn : n ∈ S) (hm' : succ m ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∀ (hmn : n ≤ m),
    (∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x) →
      ∀ (hm : succ m ∈ upperBounds S) (hn : n ∈ S) (hm' : succ m ∉ S), ∃ (x : X), IsGreatest S x

Tactic:
_
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x

Tactic:
rw [mem_upperBounds] at IH hm

Premises used: mem_upperBounds
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
IH₁ : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∀ x ∈ S, x ≤ succ m

Tactic:
rw [mem_upperBounds] at IH hm

Premises used: mem_upperBounds
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
IH₁ : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm₁ : ∀ x ∈ S, x ≤ succ m
⊢ n ∈ S

Tactic:
rw [mem_upperBounds] at IH hm

Premises used: mem_upperBounds
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
IH₁ : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm₁ : ∀ x ∈ S, x ≤ succ m
hn₁ : n ∈ S
⊢ succ m ∉ S

Tactic:
rw [mem_upperBounds] at IH hm

Premises used: mem_upperBounds
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∀ x ∈ S, x = succ m ∨ x ≤ m

Tactic:
simp_rw [Order.le_succ_iff_eq_or_le] at hm

Premises used: Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ x ≤ m

Tactic:
(hm x hx).resolve_left ?_

Premises used: Or.resolve_left
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
refine : ¬x = succ m
⊢ x ≤ m

Tactic:
refine (hm x hx).resolve_left ?_

Premises used: Or.resolve_left
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
hx : succ m ∈ S
⊢ False

Tactic:
hm' hx
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
hx : succ m ∈ S
⊢ False

Tactic:
exact hm' hx
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∀ x ∈ S, x ≤ m

Tactic:
replace hm : ∀ x ∈ S, x ≤ m := by
    intro x hx
    refine (hm x hx).resolve_left ?_
    rintro rfl
    exact hm' hx
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
pos : ∀ (hmS : m ∈ S), ∃ (x : X), IsGreatest S x
neg : ∀ (hmS : m ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x

Tactic:
by_cases hmS : m ∈ S
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ (x : X), IsGreatest S x

Tactic:
⟨m, hmS, hm⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ (x : X), IsGreatest S x

Tactic:
exact ⟨m, hmS, hm⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ (x : X), IsGreatest S x

Tactic:
IH hm hn hmS
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ (x : X), IsGreatest S x

Tactic:
exact IH hm hn hmS
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ (n : ℕ), succ^[n] a = b

Tactic:
(exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_

Premises used: Iff.mpr, Exists.imp, IsSuccArchimedean.exists_succ_iterate_of_le, map_inv_le_map_inv_iff
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
refine : ∀ (a_1 : ℕ), succ^[a_1] (EquivLike.inv f a) = EquivLike.inv f b → succ^[a_1] a = b
⊢ ∃ (n : ℕ), succ^[n] a = b

Tactic:
refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_

Premises used: Iff.mpr, Exists.imp, IsSuccArchimedean.exists_succ_iterate_of_le, map_inv_le_map_inv_iff
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
rw : (f : (a : X) → Y) (succ^[n] (EquivLike.inv f a)) = b → succ^[n] a = b
⊢ succ^[n] (EquivLike.inv f a) = EquivLike.inv f b → succ^[n] a = b

Tactic:
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]

Premises used: OrderIso.apply_eq_iff_eq, EquivLike.apply_inv_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a : Y
⊢ succ^[0] a = (f : (a : X) → Y) (succ^[0] (EquivLike.inv f a))

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
n : ℕ
IH : ∀ {a : Y}, succ^[n] a = (f : (a : X) → Y) (succ^[n] (EquivLike.inv f a))
a : Y
⊢ succ^[n + 1] a = (f : (a : X) → Y) (succ^[n + 1] (EquivLike.inv f a))

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Premises used: Function.iterate_succ', OrderIso.map_succ, Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
zero : ∀ {a : Y}, Order.succ^[0] a = (f : (a : X) → Y) (Order.succ^[0] (EquivLike.inv f a))
succ :
  ∀ (n : ℕ) (IH : ∀ {a : Y}, Order.succ^[n] a = (f : (a : X) → Y) (Order.succ^[n] (EquivLike.inv f a))) {a : Y},
    Order.succ^[n + 1] a = (f : (a : X) → Y) (Order.succ^[n + 1] (EquivLike.inv f a))
⊢ Order.succ^[n] a = (f : (a : X) → Y) (Order.succ^[n] (EquivLike.inv f a))

Tactic:
induction n generalizing a with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Premises used: Order.succ, Function.iterate_succ', OrderIso.map_succ, Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PredOrder X
inst_3 : IsPredArchimedean X
inst_4 : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
(exists_pred_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_

Premises used: Iff.mpr, IsPredArchimedean.exists_pred_iterate_of_le, Exists.imp, map_inv_le_map_inv_iff