ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ f, StrictMono f
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ∃ f, StrictMono f
inhabit α
case intro.intro
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
⊢ ∃ f, StrictMono f
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ f, StrictMono f
rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
case intro.intro.intro.intro
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∃ f, StrictMono f
case intro.intro
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
⊢ ∃ f, StrictMono f
rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
case intro.intro.intro.intro
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∀ (n : ℤ), (Int.casesOn n f fun n => g (n + 1)) < Int.casesOn (n + 1) f fun n => g (n + 1)
case intro.intro.intro.intro
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∃ f, StrictMono f
refine' ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ _⟩
case intro.intro.intro.intro.ofNat
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn (ofNat n) f fun n => g (n + 1)) < Int.casesOn (ofNat n + 1) f fun n => g (n + 1)

case intro.intro.intro.intro.negSucc.zero
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (Int.casesOn -[Nat.zero+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.zero+1] + 1) f fun n => g (n + 1)

case intro.intro.intro.intro.negSucc.succ
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn -[Nat.succ n+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.succ n+1] + 1) f fun n => g (n + 1)
case intro.intro.intro.intro
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∀ (n : ℤ), (Int.casesOn n f fun n => g (n + 1)) < Int.casesOn (n + 1) f fun n => g (n + 1)
rintro (n | _ | n)
no goals
case intro.intro.intro.intro.ofNat
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn (ofNat n) f fun n => g (n + 1)) < Int.casesOn (ofNat n + 1) f fun n => g (n + 1)
exact hf n.lt_succ_self
case intro.intro.intro.intro.negSucc.zero
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < f 0
case intro.intro.intro.intro.negSucc.zero
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (Int.casesOn -[Nat.zero+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.zero+1] + 1) f fun n => g (n + 1)
show g 1 < f 0
case intro.intro.intro.intro.negSucc.zero
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < g 0
case intro.intro.intro.intro.negSucc.zero
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < f 0
rw [hf₀, ← hg₀]
no goals
case intro.intro.intro.intro.negSucc.zero
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < g 0
exact hg Nat.zero_lt_one
no goals
case intro.intro.intro.intro.negSucc.succ
ι : Type ?u.44185
α : Type u
β : Type v
γ : Type w
δ : Type ?u.44194
π : ι → Type ?u.44199
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn -[Nat.succ n+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.succ n+1] + 1) f fun n => g (n + 1)
exact hg (Nat.lt_succ_self _)