awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
order order₁ order₂ order₃ : ¬d < c → False
⊢ d < c
have order₄ : c ≤ d → False
Tactic: order
-- 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
H : c < d
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))
have simp : ∀ ⦃a : α⦄, x c < a → a < y (f (x c)) → ∀ ⦃b : α⦄, x d < b → b < y (f (x d)) → ¬a = b
Tactic: simp only [disjoint_iff_forall_ne, mem_Ioo, ne_eq, and_imp]
-- 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
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))
⊢ False
have ayc₁ : a < y c
Tactic: rw [hfx _ hc] at ayc
Cleared hypotheses: ayc, xda, ayd
-- 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
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))
⊢ False
have this : x d ≤ y c
Tactic: have : x d ≤ y c := (xda.trans ayc).le
-- 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
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
⊢ False
have this₁ : f (x d) ≤ f (y c)
Tactic: have : f (x d) ≤ f (y c) := hf (hxs _ hd) (hys _ hc) 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
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)
⊢ False
have this₁ : d ≤ c
Tactic: rw [hfx _ hd, hfy _ hc] 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 β
f : α → β
inst_4 : SecondCountableTopology α
hf : Monotone f
⊢ Set.Countable.{u_2} (α := β) {c : β | ∃ (x : α) (y : α), x < y ∧ f x = c ∧ f y = c}
have hf₁ : MonotoneOn f univ
Tactic: rw [← monotoneOn_univ] at hf
Cleared hypotheses: 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 α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}
have 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}
Tactic: apply (countable_image_lt_image_Ioi_within s f).mono
-- 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 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ¬ContinuousWithinAt f (s ∩ Ioi x) x
⊢ x ∈ s ∧ ∃ (z : β), f x < z ∧ ∀ y ∈ s, x < y → z ≤ f y
have contrapose! : ∀ (hx : ∀ (_ : x ∈ s) (z : β) (_ : f x < z), ∃ y ∈ s, x < y ∧ f y < z), ContinuousWithinAt f (s ∩ Ioi x) x
Tactic: contrapose! hx
Cleared hypotheses: 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 α
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
have refine_1 : ∀ (m : β) (hm : m < f x), ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, m < f b
Tactic: refine tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩
-- 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 : 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
⊢ ContinuousWithinAt f (s ∩ Ioi x) x
have refine_2 : ∀ (u : β) (hu : u > f x), ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
Tactic: refine tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩
-- 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 : 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
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, m < f b
have h : ∀ (y : α) (hy : y ∈ s ∩ Ioi x), m < f y
Tactic: filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy
-- 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 : 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
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
have refine_2 : ∀ (v : α) (vs : v ∈ s) (xv : x < v) (fvu : f v < u), ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
Tactic: rcases hx xs u hu with ⟨v, vs, xv, fvu⟩
-- 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 : 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
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
have this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
Tactic: have : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x := by simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]
-- 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 : 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
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
have h : ∀ (y : α) (hy : y ∈ s ∩ Ioo x v), f y < u
Tactic: filter_upwards [this] with y hy
-- 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 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}
have apply : Subset.{u_1} (α := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}
  ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})
Tactic: apply (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono
-- 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 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
⊢ Subset.{u_1} (α := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})
have refine : Subset.{u_1} (α := Set α)
  ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})ᶜ
  {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ
Tactic: refine compl_subset_compl.1 ?_
-- 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 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
⊢ Subset.{u_1} (α := Set α)
    ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x} ∪ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x})ᶜ
    {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ
have simp : Subset.{u_1} (α := Set α)
  ({x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}ᶜ ∩ {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}ᶜ)
  {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ
Tactic: simp only [compl_union]
-- 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 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : SecondCountableTopology β
hf : MonotoneOn f s
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}ᶜ x
h'x : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Iio x) x}ᶜ x
⊢ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}ᶜ x
have simp : ∀ (hx : x ∈ s → ContinuousWithinAt f (s ∩ Ioi x) x) (h'x : x ∈ s → ContinuousWithinAt f (s ∩ Iio x) x),
  x ∈ s → ContinuousWithinAt f s x
Tactic: simp only [mem_compl_iff, mem_setOf_eq, not_and, not_not] at hx h'x ⊢
Cleared hypotheses: hx, h'x
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
Tactic: rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
Tactic: rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
Tactic: rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
Tactic: rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₄ : Eq.{u_2 + 1} (α := β) (sSup (range fun (x : ι) ↦ f (g x))) (sSup (range fun (i : ι) ↦ f (g i)))
Tactic: rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
⊢ f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
Tactic: rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
⊢ f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
Tactic: rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
⊢ f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
Tactic: rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
⊢ f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₃ : sInf (range (f ∘ g)) = sInf (range fun (i : ι) ↦ f (g i))
Tactic: rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
rw₃ : sInf (range (f ∘ g)) = sInf (range fun (i : ι) ↦ f (g i))
⊢ f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₄ : Eq.{u_2 + 1} (α := β) (sInf (range fun (x : ι) ↦ f (g x))) (sInf (range fun (i : ι) ↦ f (g i)))
Tactic: rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
⊢ f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
Tactic: rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
⊢ f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
Tactic: rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
⊢ f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
Tactic: rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
⊢ f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
Tactic: rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]