-- Mathlib/Order/SuccPred/Archimedean.lean
lemma strictMonoOn_of_pred_lt (hs : s.OrdConnected)
    (hf : ∀ a, ¬ IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a) : StrictMonoOn f s

Proof state:
case intro.succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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 : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b

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

Result:
case intro.succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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 : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b

Proof state:
case intro
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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
⊢ f (pred^[n] b) < f b

Tactic:
obtain _ | n := n

Result:
case intro.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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

case intro.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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
⊢ f (pred^[n + 1] b) < f b

Proof state:
case intro.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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
⊢ f (pred^[n + 1] b) < f b

Tactic:
apply not_isMin_of_lt at hab

Result:
case intro.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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 : ¬IsMin b
⊢ f (pred^[n + 1] b) < f b

Proof state:
case intro.succ.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : 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^[0 + 1] b ∈ s
⊢ f (pred^[0 + 1] b) < f b

Tactic:
simpa using hf _ hab hb ha

Result:
no goals