α : Type ?u.5196
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type ?u.5320
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
⊢ False
α : Type ?u.5196
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type ?u.5320
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
⊢ ∀ (n : β), n ≤ f n
by_contra' h₁
α : Type ?u.5196
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type ?u.5320
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
h₂ : min h (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x
⊢ False
α : Type ?u.5196
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type ?u.5320
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
⊢ False
have h₂ := h.min_mem _ h₁
no goals
α : Type ?u.5196
β : Type u_1
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
γ : Type ?u.5320
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
h₂ : min h (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x
⊢ False
exact h.not_lt_min _ h₁ (hf h₂) h₂