awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : ¬IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
(hn this).trans (hf _ hb' this hb)

Premises used: LE.le.trans
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : ¬IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
exact (hn this).trans (hf _ hb' this hb)

Premises used: LE.le.trans
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a ≤ f (Order.succ a)
a : α
ha : a ∈ s
n : ℕ
hb : Order.succ^[n] a ∈ s
zero : ∀ (hb : Order.succ^[0] a ∈ s), f a ≤ f (Order.succ^[0] a)
succ :
  ∀ (n : ℕ) (hn : ∀ (hb : Order.succ^[n] a ∈ s), f a ≤ f (Order.succ^[n] a)) (hb : Order.succ^[n + 1] a ∈ s),
    f a ≤ f (Order.succ^[n + 1] a)
⊢ f a ≤ f (Order.succ^[n] a)

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)

Premises used: Function.iterate_succ_apply', Order.succ, Nat.iterate, IsMax
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f (succ a) ≤ f a
⊢ AntitoneOn f s

Tactic:
monotoneOn_of_le_succ (β := βᵒᵈ) hs hf

Premises used: monotoneOn_of_le_succ, AntitoneOn
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
obtain : ∀ (n : ℕ) (hb : succ^[n] a ∈ s) (hab : a < succ^[n] a), f a < f (succ^[n] a)
⊢ f a < f b

Tactic:
obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le

Premises used: LT.lt.le, IsSuccArchimedean.exists_succ_iterate_of_le, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)
a : α
ha : a ∈ s
n : ℕ
hb : Order.succ^[n] a ∈ s
hab : a < Order.succ^[n] a
zero : ∀ (hb : Order.succ^[0] a ∈ s) (hab : a < Order.succ^[0] a), f a < f (Order.succ^[0] a)
succ : ∀ (n : ℕ) (hb : Order.succ^[n + 1] a ∈ s) (hab : a < Order.succ^[n + 1] a), f a < f (Order.succ^[n + 1] a)
⊢ f a < f (Order.succ^[n] a)

Tactic:
obtain _ | n := n
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hb : succ^[0] a ∈ s
hab : a < succ^[0] a
⊢ f a < f (succ^[0] a)

Tactic:
simp at hab
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : a < succ^[n + 1] a
⊢ ¬IsMax a

Tactic:
apply not_isMax_of_lt at hab

Premises used: not_isMax_of_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
hb : succ^[HAdd.hAdd (α := ℕ) 0 1] a ∈ s
⊢ f a < f (succ^[HAdd.hAdd (α := ℕ) 0 1] a)

Tactic:
simpa using hf _ hab ha hb
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : Order.succ^[n + 1] a ∈ s), f a < f (Order.succ^[n + 1] a)
hb : Order.succ^[n + 1 + 1] a ∈ s
succ : ∀ (hb : Order.succ (Order.succ^[n + 1] a) ∈ s), f a < f (Order.succ (Order.succ^[n + 1] a))
⊢ f a < f (Order.succ^[n + 1 + 1] a)

Tactic:
rw [Function.iterate_succ_apply'] at hb ⊢

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
⊢ succ^[n + 1] a ∈ s

Tactic:
have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
pos : ∀ (hb' : IsMax (succ^[n + 1] a)), f a < f (succ (succ^[n + 1] a))
neg : ∀ (hb' : ¬IsMax (succ^[n + 1] a)), f a < f (succ (succ^[n + 1] a))
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
by_cases hb' : IsMax (succ^[n + 1] a)

Premises used: Order.succ, Nat.iterate, HAdd.hAdd, OfNat.ofNat, IsMax
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
pos : f a < f (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
rw [succ_eq_iff_isMax.2 hb']

Premises used: Iff.mpr, Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ^[n + 1] a)

Tactic:
hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ^[n + 1] a)

Tactic:
exact hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : ¬IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
(hn this).trans (hf _ hb' this hb)

Premises used: LT.lt.trans
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : ¬IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
exact (hn this).trans (hf _ hb' this hb)

Premises used: LT.lt.trans
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)
a : α
ha : a ∈ s
n : ℕ
hb : Order.succ^[n + 1] a ∈ s
hab : ¬IsMax a
succ : ∀ (hb : Order.succ^[HAdd.hAdd (α := ℕ) 0 1] a ∈ s), f a < f (Order.succ^[HAdd.hAdd (α := ℕ) 0 1] a)
succ₁ :
  ∀ (n : ℕ) (hn : ∀ (hb : Order.succ^[n + 1] a ∈ s), f a < f (Order.succ^[n + 1] a))
    (hb : Order.succ^[n + 1 + 1] a ∈ s), f a < f (Order.succ^[n + 1 + 1] a)
⊢ f a < f (Order.succ^[n + 1] a)

Tactic:
induction n with
  | zero => simpa using hf _ hab ha hb
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n + 1] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)

Premises used: Function.iterate_succ_apply', Order.succ, Nat.iterate, HAdd.hAdd, OfNat.ofNat, IsMax
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f (succ a) < f a
⊢ StrictAntiOn f s

Tactic:
strictMonoOn_of_lt_succ (β := βᵒᵈ) hs hf

Premises used: StrictAntiOn, strictMonoOn_of_lt_succ
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ ∀ (a : α),
    ¬IsMax a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (succ a) → f a ≤ f (succ a)

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ Monotone f

Tactic:
simpa using monotoneOn_of_le_succ Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, monotoneOn_of_le_succ
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ ∀ (a : α),
    ¬IsMax a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (succ a) → f (succ a) ≤ f a

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ Antitone f

Tactic:
simpa using antitoneOn_of_succ_le Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, antitoneOn_of_succ_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ ∀ (a : α),
    ¬IsMax a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (succ a) → f a < f (succ a)

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ StrictMono f

Tactic:
simpa using strictMonoOn_of_lt_succ Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, strictMonoOn_of_lt_succ
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ ∀ (a : α),
    ¬IsMax a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (succ a) → f (succ a) < f a

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ StrictAnti f

Tactic:
simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, strictAntiOn_of_succ_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
obtain : ∀ (n : ℕ) (ha : pred^[n] b ∈ s) (hab : pred^[n] b ≤ b), f (pred^[n] b) ≤ f b
⊢ f a ≤ f b

Tactic:
obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab

Premises used: IsPredArchimedean.exists_pred_iterate_of_le, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
ha : pred^[0] b ∈ s
⊢ f (pred^[0] b) ≤ f b

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred^[n + 1] b ∈ s
succ : ∀ (ha : pred (pred^[n] b) ∈ s), f (pred (pred^[n] b)) ≤ f b
⊢ f (pred^[n + 1] b) ≤ f b

Tactic:
rw [Function.iterate_succ_apply'] at ha ⊢

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
⊢ pred^[n] b ∈ s

Tactic:
have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
pos : ∀ (ha' : IsMin (pred^[n] b)), f (pred (pred^[n] b)) ≤ f b
neg : ∀ (ha' : ¬IsMin (pred^[n] b)), f (pred (pred^[n] b)) ≤ f b
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
by_cases ha' : IsMin (pred^[n] b)

Premises used: Nat.iterate, Order.pred, IsMin
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
pos : f (pred^[n] b) ≤ f b
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
rw [pred_eq_iff_isMin.2 ha']

Premises used: Iff.mpr, Order.pred_eq_iff_isMin
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred^[n] b) ≤ f b

Tactic:
hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred^[n] b) ≤ f b

Tactic:
exact hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : ¬IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
(hn this).trans' (hf _ ha' this ha)

Premises used: LE.le.trans'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : ¬IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
exact (hn this).trans' (hf _ ha' this ha)

Premises used: LE.le.trans'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
zero : ∀ (ha : pred^[0] b ∈ s), f (pred^[0] b) ≤ f b
succ :
  ∀ (n : ℕ) (hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b) (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) ≤ f b
⊢ f (pred^[n] b) ≤ f b

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

Premises used: Function.iterate_succ_apply', Order.succ, Nat.iterate, Order.pred, IsMin
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f a ≤ f (pred a)
⊢ AntitoneOn f s

Tactic:
monotoneOn_of_pred_le (β := βᵒᵈ) hs hf

Premises used: monotoneOn_of_pred_le, AntitoneOn
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
obtain : ∀ (n : ℕ) (ha : pred^[n] b ∈ s) (hab : pred^[n] b < b), f (pred^[n] b) < f b
⊢ f a < f b

Tactic:
obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le

Premises used: IsPredArchimedean.exists_pred_iterate_of_le, LT.lt.le, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
hab : pred^[n] b < b
zero : ∀ (ha : pred^[0] b ∈ s) (hab : pred^[0] b < b), f (pred^[0] b) < f b
succ : ∀ (n : ℕ) (ha : pred^[n + 1] b ∈ s) (hab : pred^[n + 1] b < b), f (pred^[n + 1] b) < f b
⊢ f (pred^[n] b) < f b

Tactic:
obtain _ | n := n
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
ha : pred^[0] b ∈ s
hab : pred^[0] b < b
⊢ f (pred^[0] b) < f b

Tactic:
simp at hab
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : pred^[n + 1] b < b
⊢ ¬IsMin b

Tactic:
apply not_isMin_of_lt at hab

Premises used: not_isMin_of_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
ha : pred^[HAdd.hAdd (α := ℕ) 0 1] b ∈ s
⊢ f (pred^[HAdd.hAdd (α := ℕ) 0 1] b) < f b

Tactic:
simpa using hf _ hab hb ha
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred^[n + 1 + 1] b ∈ s
succ : ∀ (ha : pred (pred^[n + 1] b) ∈ s), f (pred (pred^[n + 1] b)) < f b
⊢ f (pred^[n + 1 + 1] b) < f b

Tactic:
rw [Function.iterate_succ_apply'] at ha ⊢

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
⊢ pred^[n + 1] b ∈ s

Tactic:
have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩