-- 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.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
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ 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 hbd | hdb := le_total b d

Result:
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)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.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
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ 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.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)

Tactic:
exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans <| hfdb.trans_lt hfba, hfba⟩⟩

Result:
no goals

Proof state:
case refine_2
α : 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)

Tactic:
rintro ⟨⟨a, b, hab, hfba⟩, c, d, hcd, hfcd⟩

Result:
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)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.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
had : a ≤ d
hac : a ≤ c
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)

Tactic:
obtain hfca | hfac := lt_or_le (f c) (f a)

Result:
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)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.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
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ 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.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
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ 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, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩

Result:
no goals

Proof state:
α : 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)

Tactic:
refine Iff.symm ⟨?_, ?_⟩

Result:
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

case refine_2
α : 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_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)

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

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.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
hfac : f a ≤ f c
hdb : d ≤ 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, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.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
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 ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.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
hfac : f a ≤ f c
⊢ ∃ 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 hbd | hdb := le_total b d

Result:
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)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.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
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)