awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LocalExtr (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: rcases le_total x b
-- Lean 4 proof step from Mathlib.Topology.Order.LocalExtr (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have inr : b ≤ x → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: rcases le_total x b
-- Lean 4 proof step from Mathlib.Topology.Order.LocalExtr (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
have inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
Tactic: rcases le_total x b
-- Lean 4 proof step from Mathlib.Topology.Order.LocalExtr (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
have inr : b ≤ x → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
Tactic: rcases le_total x b
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
⊢ MonotoneOn f (insert x s)
have this : (𝓝[s] x).NeBot
Tactic: have : (𝓝[s] x).NeBot := hx
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
⊢ MonotoneOn f (insert x s)
have apply : ∀ (b : α) (hb : b ∈ s) (hbx : b ≤ x), f b ≤ f x
Tactic: apply monotoneOn_insert_iff.2 ⟨fun b hb hbx ↦ ?_, fun b hb hxb ↦ ?_, hf⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
apply : ∀ (b : α) (hb : b ∈ s) (hbx : b ≤ x), f b ≤ f x
⊢ MonotoneOn f (insert x s)
have apply₁ : ∀ (b : α) (hb : b ∈ s) (hxb : x ≤ b), f x ≤ f b
Tactic: apply monotoneOn_insert_iff.2 ⟨fun b hb hbx ↦ ?_, fun b hb hxb ↦ ?_, hf⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx : b ≤ x
⊢ f b ≤ f x
have inl : ∀ (hx : ClusterPt b (𝓟 s)) (h'x : ContinuousWithinAt f s b) (this : (𝓝[s] b).NeBot) (hbx : b ≤ b), f b ≤ f b
Tactic: rcases hbx.eq_or_lt with rfl | hbx
Cleared hypotheses: x, hx, h'x, this, hbx
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx : b ≤ x
inl : ∀ (hx : ClusterPt b (𝓟 s)) (h'x : ContinuousWithinAt f s b) (this : (𝓝[s] b).NeBot) (hbx : b ≤ b), f b ≤ f b
⊢ f b ≤ f x
have inr : ∀ (hbx : b < x), f b ≤ f x
Tactic: rcases hbx.eq_or_lt with rfl | hbx
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
⊢ f b ≤ f x
have inr : ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c
Tactic: apply ge_of_tendsto h'x
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c
have this₁ : s ∩ Ioi b ∈ 𝓝[s] x
Tactic: have : s ∩ Ioi b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Ioi_mem_nhds hbx)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
this : s ∩ Ioi b ∈ 𝓝[s] x
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α | x ∈ s ∩ Ioi b → Membership.mem (γ := Set α) {x : α | (fun (c : α) ↦ f b ≤ f c) x} x} a
Tactic: filter_upwards [this] with y hy using hf hb hy.1 (le_of_lt hy.2)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
this : s ∩ Ioi b ∈ 𝓝[s] x
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α | x ∈ s ∩ Ioi b → Membership.mem (γ := Set α) {x : α | (fun (c : α) ↦ f b ≤ f c) x} x} a
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c
have h₁ : ∀ a ∈ s ∩ Ioi b, f b ≤ f a
Tactic: filter_upwards [this] with y hy using hf hb hy.1 (le_of_lt hy.2)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
⊢ f x ≤ f b
have inl : ∀ (hb : x ∈ s) (hxb : x ≤ x), f x ≤ f x
Tactic: rcases hxb.eq_or_lt with rfl | hxb
Cleared hypotheses: b, hb, hxb
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
inl : ∀ (hb : x ∈ s) (hxb : x ≤ x), f x ≤ f x
⊢ f x ≤ f b
have inr : ∀ (hxb : x < b), f x ≤ f b
Tactic: rcases hxb.eq_or_lt with rfl | hxb
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
⊢ f x ≤ f b
have inr : ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b
Tactic: apply le_of_tendsto h'x
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b
have this₁ : s ∩ Iio b ∈ 𝓝[s] x
Tactic: have : s ∩ Iio b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Iio_mem_nhds hxb)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
this : s ∩ Iio b ∈ 𝓝[s] x
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b
have h : ∀ (y : α) (hy : y ∈ s ∩ Iio b), f y ≤ f b
Tactic: filter_upwards [this] with y hy
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
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
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
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}
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
have this : ∀ 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
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
have 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}
Tactic: choose! x y hxs hys hxy hfx hfy using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
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
⊢ c = d
have this : f (x c) = f (x d)
Tactic: have : f (x c) = f (x d) := by simp [hcd]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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)
⊢ c = d
have rwa : ∀ (this : c = f (x d)), c = d
Tactic: rwa [hfx _ hc, hfx _ hd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ c = d
have rwa₁ : ∀ (this : c = d), c = d
Tactic: rwa [hfx _ hc, hfx _ hd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
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
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
have suffices : (x '' t).Countable
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
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ (x '' t).Countable
have h : (x '' t).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y (f x))
Tactic: apply Set.PairwiseDisjoint.countable_of_Ioo (y := fun a ↦ y (f a))
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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))
⊢ (x '' t).Countable
have h' : ∀ x_1 ∈ x '' t, x_1 < y (f x_1)
Tactic: apply Set.PairwiseDisjoint.countable_of_Ioo (y := fun a ↦ y (f a))
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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 (f (x c))
have h' : x c < y c
Tactic: rw [hfx _ hc]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ (x '' t).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y (f x))
have 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))))
Tactic: simp only [PairwiseDisjoint, Set.Pairwise, mem_image, onFun, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
have 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))))
Tactic: wlog H : c < d generalizing c d with h
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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))))
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
have 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))))
Tactic: wlog H : c < d generalizing c d with h
Cleared hypotheses: c, hc, d, hd, hcd
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
have apply : d < c
Tactic: apply (h d hd c hc hcd.symm ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (hypothesis)
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
⊢ d < c
have this : c ≠ d
Tactic: have : c ≠ d := fun h ↦ hcd (congrArg x h)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
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
⊢ d < c
have order : ¬d < c → False
Tactic: order