-- Mathlib/Order/Monotone/Basic.lean
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
lemma not_monotone_not_antitone_iff_exists_le_le :
    ¬ Monotone f ∧ ¬ Antitone f ↔
      ∃ a b c, a ≤ b ∧ b ≤ c ∧ ((f a < f b ∧ f c < f b) ∨ (f b < f a ∧ f b < f c))

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans <| hfdb.trans_lt hfba, hfcd⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
obtain hda | had := le_total d a

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp_rw [Monotone, Antitone, not_forall, not_le]

Result:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) ↔
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1

Tactic:
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩

Result:
case refine_1.intro.intro.intro.intro.intro.inl.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1

case refine_1.intro.intro.intro.intro.intro.inr.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
obtain hac | hca := le_total a c

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
obtain hfdb | hfbd := le_or_lt (f d) (f b)

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfad : f a ≤ f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
obtain hfad | hfda := le_total (f a) (f d)

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfad : f a ≤ f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩

Result:
no goals