Theorem: C03S04.not_monotone_iff (LeanInRome/S3_Logic/S04_Conjunction_and_Iff.lean)

State before:
f : ℝ → ℝ
⊢ ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y
Tactic:
rw [Monotone]
State after:
f : ℝ → ℝ
⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y

State before:
f : ℝ → ℝ
⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y
Tactic:
push_neg
State after:
f : ℝ → ℝ
⊢ (∃ a b, a ≤ b ∧ f b < f a) ↔ ∃ x y, x ≤ y ∧ f x > f y

State before:
f : ℝ → ℝ
⊢ (∃ a b, a ≤ b ∧ f b < f a) ↔ ∃ x y, x ≤ y ∧ f x > f y
Tactic:
rfl
State after:
no goals