awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
⊢ Membership.mem (γ := Filter α) atBot s
have refine_2 : ∀ (a : α) (ha : IsLeast t a), Membership.mem (γ := Filter α) atBot s
Tactic: obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : NoMinOrder α
inst_3 : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
a : α
ha : IsLeast t a
⊢ Membership.mem (γ := Filter α) atBot s
have refine_2 : ∀ (b : α) (hb : b < a), Membership.mem (γ := Filter α) atBot s
Tactic: obtain ⟨b, hb⟩ := exists_lt a
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
⊢ ∃ x ∈ s, IsMinOn f s x
have rcases : ∀ (x : β) (hxs : x ∈ s) (hx : f x ∈ lowerBounds (f '' s)), ∃ x ∈ s, IsMinOn f s x
Tactic: rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
⊢ ∃ x ∈ s, IsMinOn f s x
have refine : ∀ (x : β) (hb : Membership.mem (γ := Set β) ((fun (a : β) ↦ a) '' s) x), x ∈ s
Tactic: refine ⟨x, hxs, forall_mem_image.1 (fun _ hb => hx <| mem_image_of_mem f ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
have inl : ∀ (hs : IsCompact.{u_3} (X := β) ∅) (hf : ContinuousOn f ∅)
  (hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b),
  ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs')
Cleared hypotheses: s, hs, hf, hf'
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
inl :
  ∀ (hs : IsCompact.{u_3} (X := β) ∅) (hf : ContinuousOn f ∅)
    (hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b),
    ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
have inr : ∀ (hs' : s.Nonempty), ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs')
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
a : α
hs : IsCompact.{u_3} (X := β) ∅
hf : ContinuousOn f ∅
hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b
⊢ ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b
have inl : ∀ (a' : α) (ha' : a < a'), ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b
Tactic: obtain ⟨a', ha'⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
have inr : ∀ (x : β) (hx : x ∈ s) (hx' : IsMinOn f s x), ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
Tactic: obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
⊢ ∃ x ∈ s, IsMinOn f s x
have rcases : ∀ (K : Set β) (hK : IsCompact K) (hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x), ∃ x ∈ s, IsMinOn f s x
Tactic: rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
⊢ ∃ x ∈ s, IsMinOn f s x
have hsub : insert x₀ (K ∩ s) ⊆ s
Tactic: have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
⊢ ∃ x ∈ s, IsMinOn f s x
have obtain : ∀ (x : β) (hx : x ∈ insert x₀ (K ∩ s)) (hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y), ∃ x ∈ s, IsMinOn f s x
Tactic: obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y :=
    ((hK.inter_right hsc).insert x₀).exists_isMinOn (insert_nonempty _ _) (hf.mono hsub)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
⊢ ∃ x ∈ s, IsMinOn f s x
have refine : ∀ (y : β) (hy : y ∈ s), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
Tactic: refine ⟨x, hsub hx, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
⊢ Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
have pos : ∀ (hyK : y ∈ K), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
Tactic: by_cases hyK : y ∈ K
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
pos : ∀ (hyK : y ∈ K), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
⊢ Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
have neg : ∀ (hyK : y ∉ K), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
Tactic: by_cases hyK : y ∈ K
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
f : β → α
hf : Continuous[inst_2, inst_1] f
x₀ : β
h : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
⊢ ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 univ, f x₀ ≤ f x
have rwa : ∀ᶠ (x : β) in cocompact β ⊓ ⊤, f x₀ ≤ f x
Tactic: rwa [principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
f : β → α
hf : Continuous[inst_2, inst_1] f
hlim : Tendsto f (cocompact β) atTop
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y
have inhabit : ∀ (inhabited_h : Inhabited β), ∃ (x : β), ∀ (y : β), f x ≤ f y
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y
have obtain : ∀ (x : β) (hx : f x ∈ lowerBounds (range f)), ∃ (x : β), ∀ (y : β), f x ≤ f y
Tactic: obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y
have hx₁ : ∀ (i : β), f x ≤ f i
Tactic: rw [mem_lowerBounds, forall_mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
⊢ BddBelow s
have inl : ∀ (hs : IsCompact.{u_2} (X := α) ∅), BddBelow.{u_2} (α := α) ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
inl : ∀ (hs : IsCompact.{u_2} (X := α) ∅), BddBelow.{u_2} (α := α) ∅
⊢ BddBelow s
have inr : ∀ (hne : s.Nonempty), BddBelow s
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s
have inr : ∀ (a : α) (has : a ∈ lowerBounds s), BddBelow s
Tactic: obtain ⟨a, -, has⟩ := hs.exists_isLeast hne
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
⊢ sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y
have refine : ∀ (h : ∀ x ∈ K, f x < y), sSup (f '' K) < y
Tactic: refine ⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h,
    fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
⊢ sSup (f '' K) < y
have obtain : ∀ (x : β) (hx : x ∈ K) (h2x : IsMaxOn f K x), sSup (f '' K) < y
Tactic: obtain ⟨x, hx, h2x⟩ := hK.exists_isMaxOn h0K hf
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
⊢ sSup (f '' K) < y
have refine : ∀ b ∈ f '' K, b ≤ f x
Tactic: refine (csSup_le (h0K.image f) ?_).trans_lt (h x hx)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)
have inl : ∀ (hK : IsCompact.{u_3} (X := β) ∅), Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' ∅)
Tactic: rcases eq_empty_or_nonempty K with (rfl | h0K)
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
inl : ∀ (hK : IsCompact.{u_3} (X := β) ∅), Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' ∅)
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)
have inr : ∀ (h0K : K.Nonempty), Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)
Tactic: rcases eq_empty_or_nonempty K with (rfl | h0K)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
hK : IsCompact.{u_3} (X := β) ∅
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' ∅)
have inl : Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup ∅
Tactic: simp_rw [image_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)
have inr : ∀ (x : γ), ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
⊢ ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x
have inr : ∀ (y : β) (hyK : y ∈ K) (h2y : sSup (f x '' K) = f x y) (hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y),
  ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x
Tactic: obtain ⟨y, hyK, h2y, hy⟩ :=
    hK.exists_sSup_image_eq_and_ge h0K
      (show Continuous (f x) from hf.comp <| .prodMk_right x).continuousOn
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x
have inr : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
Tactic: rw [ContinuousAt, h2y, tendsto_order]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
have this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
Tactic: have := tendsto_order.mp ((show Continuous fun x => f x y
    from hf.comp <| .prodMk_left _).tendsto x)
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
have inr : ∀ (z : α) (hz : z < f x y), ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)
Tactic: refine ⟨fun z hz => ?_, fun z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
inr : ∀ (z : α) (hz : z < f x y), ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
have inr₁ : ∀ (z : α) (hz : z > f x y), ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
Tactic: refine ⟨fun z hz => ?_, fun z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z < f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)
have inr : ∀ (x' : γ) (hx' : z < f x' y), BddAbove (f x' '' K)
Tactic: refine (this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
have h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
Tactic: have h : ({x} : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z := by
      rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
      exact (hy y' hy').trans_lt hz
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
have inr : ∀ (u : Set γ) (v : Set β) (hu : IsOpen[inst_4] u),
  IsOpen[inst_3] v →
    ∀ (hxu : {x} ⊆ u) (hKv : K ⊆ v) (huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z), ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
Tactic: obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ :=
      generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
have inr : ∀ (x' : γ) (hx' : x' ∈ u), sSup (f x' '' K) < z
Tactic: refine eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ sSup (f x' '' K) < z
have inr : ∀ x ∈ K, f x' x < z
Tactic: rw [hK.sSup_lt_iff_of_continuous h0K
        (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
have refine : sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
Tactic: refine h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm