awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
⊢ ∀ c ∈ t, ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c

Tactic:
have : ∀ c ∈ t, ∃ x, ∃ y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c := fun c hc ↦ hc
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
this : ∀ c ∈ t, ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c
choose! :
  ∀ (x y : (c : β) → α) (hxs : ∀ c ∈ t, x c ∈ s) (hys : ∀ c ∈ t, y c ∈ s) (hxy : ∀ c ∈ t, x c < y c)
    (hfx : ∀ c ∈ t, f (x c) = c) (hfy : ∀ c ∈ t, f (y c) = c),
    Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}

Tactic:
choose! x y hxs hys hxy hfx hfy using this
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
⊢ f (x c) = f (x d)

Tactic:
simp [hcd]
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
⊢ f (x c) = f (x d)

Tactic:
have : f (x c) = f (x d) := by simp [hcd]
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
this : f (x c) = f (x d)
rwa : ∀ (this : c = f (x d)), c = d
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : c = d), c = d
⊢ c = d

Tactic:
rwa [hfx _ hc, hfx _ hd] at this
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
⊢ InjOn x t

Tactic:
have : Set.InjOn x t := by
      intro c hc d hd hcd
      have : f (x c) = f (x d) := by simp [hcd]
      rwa [hfx _ hc, hfx _ hd] at this
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
this : InjOn x t
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}

Tactic:
countable_of_injective_of_countable_image this H

Premises used: Set.countable_of_injective_of_countable_image
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
this : InjOn x t
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}

Tactic:
exact countable_of_injective_of_countable_image this H

Premises used: Set.countable_of_injective_of_countable_image
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
suffices : (x '' t).Countable
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}

Tactic:
suffices H : Set.Countable (x '' t) by
    have : Set.InjOn x t := by
      intro c hc d hd hcd
      have : f (x c) = f (x d) := by simp [hcd]
      rwa [hfx _ hc, hfx _ hd] at this
    exact countable_of_injective_of_countable_image this H
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h_1 : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
h : (x '' t).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y (f x))
h' : ∀ x_1 ∈ x '' t, x_1 < y (f x_1)
⊢ (x '' t).Countable

Tactic:
apply Set.PairwiseDisjoint.countable_of_Ioo (y := fun a ↦ y (f a))

Premises used: Set.PairwiseDisjoint.countable_of_Ioo
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
h' : x c < y c
⊢ x c < y (f (x c))

Tactic:
rw [hfx _ hc]
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y c

Tactic:
hxy _ hc
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y c

Tactic:
exact hxy _ hc
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h_1 : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
h : ∀ a ∈ t, ∀ a_2 ∈ t, x a ≠ x a_2 → Disjoint (Ioo (x a) (y (f (x a)))) (Ioo (x a_2) (y (f (x a_2))))
⊢ (x '' t).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y (f x))

Tactic:
simp only [PairwiseDisjoint, Set.Pairwise, mem_image, onFun, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]

Premises used: Function.onFun, and_imp, Set.PairwiseDisjoint, Set.mem_image, forall_exists_index, Set.Pairwise, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h_1 : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
h :
  ∀
    (h :
      ∀ (c : β) (hc : c ∈ t) (d : β) (hd : d ∈ t) (hcd : x c ≠ x d) (H : c < d),
        Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d)))))
    (H : ¬c < d), Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
wlog :
  ∀ (c : β) (hc : c ∈ t) (d : β) (hd : d ∈ t) (hcd : x c ≠ x d) (H : c < d),
    Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))

Tactic:
wlog H : c < d generalizing c d with h
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h_1 : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
h :
  ∀ (c : β) (hc : c ∈ t) (d : β) (hd : d ∈ t) (hcd : x c ≠ x d) (H : c < d),
    Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
H : ¬c < d
apply : d < c
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))

Tactic:
apply (h d hd c hc hcd.symm ?_).symm

Premises used: Ne.symm, Disjoint.symm
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h_1 : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
h :
  ∀ (c : β) (hc : c ∈ t) (d : β) (hd : d ∈ t) (hcd : x c ≠ x d) (H : c < d),
    Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
H : ¬c < d
⊢ c ≠ d

Tactic:
have : c ≠ d := fun h ↦ hcd (congrArg x h)
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h_1 : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
h :
  ∀ (c : β) (hc : c ∈ t) (d : β) (hd : d ∈ t) (hcd : x c ≠ x d) (H : c < d),
    Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
H : ¬c < d
this : c ≠ d
order order₁ order₂ order₃ : ¬d < c → False
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : c ≤ d → False
⊢ d < c

Tactic:
order
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
simp : ∀ ⦃a : α⦄, x c < a → a < y (f (x c)) → ∀ ⦃b : α⦄, x d < b → b < y (f (x d)) → ¬a = b
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))

Tactic:
simp only [disjoint_iff_forall_ne, mem_Ioo, ne_eq, and_imp]

Premises used: Set.mem_Ioo, and_imp, ne_eq, Set.disjoint_iff_forall_ne
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y (f (x c))
xda : x d < a
ayd : a < y (f (x d))
⊢ a < y c

Tactic:
rw [hfx _ hc] at ayc
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y (f (x c))
xda : x d < a
ayd : a < y (f (x d))
ayc₁ : a < y c
⊢ x d < a

Tactic:
rw [hfx _ hc] at ayc
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y (f (x c))
xda : x d < a
ayd : a < y (f (x d))
ayc₁ : a < y c
xda₁ : x d < a
⊢ a < y (f (x d))

Tactic:
rw [hfx _ hc] at ayc
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
⊢ x d ≤ y c

Tactic:
have : x d ≤ y c := (xda.trans ayc).le
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
this : x d ≤ y c
⊢ f (x d) ≤ f (y c)

Tactic:
have : f (x d) ≤ f (y c) := hf (hxs _ hd) (hys _ hc) this
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
this_1 : x d ≤ y c
this : f (x d) ≤ f (y c)
⊢ d ≤ c

Tactic:
rw [hfx _ hd, hfy _ hc] at this
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
this_1 : x d ≤ y c
this : d ≤ c
⊢ False

Tactic:
not_le.2 H this

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
h : Nontrivial α
t : Set β := {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : (c : β) → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
this_1 : x d ≤ y c
this : d ≤ c
⊢ False

Tactic:
exact not_le.2 H this

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : α → β
inst_4 : SecondCountableTopology α
hf : Monotone f
⊢ MonotoneOn f univ

Tactic:
rw [← monotoneOn_univ] at hf

Premises used: monotoneOn_univ
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f univ
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x < y ∧ f x = c ∧ f y = c}

Tactic:
simpa using hf.countable_setOf_two_preimages

Premises used: MonotoneOn.countable_setOf_two_preimages
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : AntitoneOn f s
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}

Tactic:
(MonotoneOn.countable_setOf_two_preimages hf.dual_right :)

Premises used: setOf, AntitoneOn.dual_right, MonotoneOn.countable_setOf_two_preimages, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : α → β
inst_4 : SecondCountableTopology α
hf : Antitone f
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x < y ∧ f x = c ∧ f y = c}

Tactic:
(Monotone.countable_setOf_two_preimages hf.dual_right :)

Premises used: Antitone.dual_right, setOf, Monotone.countable_setOf_two_preimages, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
apply :
  Subset.{u_1} (α := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}
    {x : α | x ∈ s ∧ ∃ (z : β), f x < z ∧ ∀ y ∈ s, x < y → z ≤ f y}
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}

Tactic:
apply (countable_image_lt_image_Ioi_within s f).mono

Premises used: countable_image_lt_image_Ioi_within, Set.Countable.mono
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ¬ContinuousWithinAt f (s ∩ Ioi x) x
contrapose! : ∀ (hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z), ContinuousWithinAt f (s ∩ Ioi x) x
⊢ x ∈ s ∧ ∃ (z : β), f x < z ∧ ∀ y ∈ s, x < y → z ≤ f y

Tactic:
contrapose! hx
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
⊢ ContinuousWithinAt f (s ∩ Ioi x) x

Tactic:
tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩

Premises used: Iff.mpr, ContinuousWithinAt, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z
refine_1 : ∀ (m : β) (hm : m < f x), ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, m < f b
refine_2 : ∀ (u : β) (hu : u > f x), ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
⊢ ContinuousWithinAt f (s ∩ Ioi x) x

Tactic:
refine tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro