awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : IsGLB 𝓕 s
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsGLB 𝓕' s
have simp_rw : ∀ (h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)),
  ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
Tactic: simp_rw [isGLB_pi] at *
Cleared hypotheses: h𝓕
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have rcases : ∀ (D : Set E) (D_count : D.Countable) (D_dense : Dense D),
  ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
Tactic: rcases exists_countable_dense E with ⟨D, D_count, D_dense⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (hypothesis)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
Tactic: have U_open {f} (hf : f ∈ 𝓕) (d : E) : IsOpen (U f d) := h𝓕_cont f hf |>.isOpen_preimage d
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
d : E
⊢ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
have h : ∀ (x : X),
  Membership.mem (γ := Set X) {x : X | s x < d} x ↔
    Membership.mem (γ := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (hypothesis)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
Tactic: have (d : E) : {x | s x < d} = ⋃ f : 𝓕, U f d := by
    ext x
    simp [U, isGLB_lt_iff (h𝓕 x)]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
⊢ ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A, U f d)
have simp_rw : ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)
Tactic: simp_rw [this d]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
⊢ ∃ A ⊆ 𝓕,
    A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)
have rcases : ∀ (t : Set (↑𝓕 : Type (max u_1 u_2))) (t_count : t.Countable)
  (ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)),
  ∃ A ⊆ 𝓕,
    A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)
Tactic: rcases eq_open_union_countable (fun f : 𝓕 ↦ U f d) (fun f ↦ U_open f.2 d) with ⟨t, t_count, ht⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
t : Set (↑𝓕 : Type (max u_1 u_2))
t_count : t.Countable
ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)
⊢ ∃ A ⊆ 𝓕,
    A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)
have right : Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
  (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
Tactic: use (↑) '' t, image_val_subset, t_count.image _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
t : Set (↑𝓕 : Type (max u_1 u_2))
t_count : t.Countable
ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
    (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
have right : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
Tactic: rw [← ht, biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
t : Set (↑𝓕 : Type (max u_1 u_2))
t_count : t.Countable
ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)
right :
  Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
    (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
have right₁ : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ y ∈ t, U (↑y : X → E) d)
Tactic: rw [← ht, biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (hypothesis)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have this₁ : ∀ (d : E), ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A, U f d)
Tactic: have (d : E) : ∃ A ⊆ 𝓕, A.Countable ∧ {x | s x < d} = ⋃ f ∈ A, U f d := by
    simp_rw [this d]
    rcases eq_open_union_countable (fun f : 𝓕 ↦ U f d) (fun f ↦ U_open f.2 d) with ⟨t, t_count, ht⟩
    use (↑) '' t, image_val_subset, t_count.image _
    rw [← ht, biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this_1 : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
this : ∀ (d : E), ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A, U f d)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have choose : ∀ (A : (d : E) → Set (X → E)) (A_sub : ∀ (d : E), A d ⊆ 𝓕) (A_count : ∀ (d : E), (A d).Countable)
  (hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)),
  ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
Tactic: choose A A_sub A_count hA using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (hypothesis)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have 𝓕'_sub : 𝓕' ⊆ 𝓕
Tactic: have 𝓕'_sub : 𝓕' ⊆ 𝓕 := iUnion₂_subset fun d _ ↦ A_sub d
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have right : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
Tactic: use 𝓕', 𝓕'_sub, D_count.biUnion fun d _ ↦ A_count d
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
⊢ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
have right : ∀ (x : X) (e : E) (he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')), e ≤ s x
Tactic: refine fun x ↦ ⟨lowerBounds_mono_set (image_mono 𝓕'_sub) (h𝓕 x).1, fun e he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
⊢ e ≤ s x
have right : ∀ (H : s x < e), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
⊢ False
have right : ∀ (d : E) (d_mem : d ∈ D) (hd : d ∈ Ioo (s x) e), False
Tactic: rcases D_dense.exists_between H with ⟨d, d_mem, hd⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (hypothesis)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
⊢ ∃ f ∈ A d, f x < d
have this₁ : Membership.mem (γ := Set X) {y : X | s y < d} x
Tactic: have : x ∈ {y | s y < d} := hd.1
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
⊢ False
have right : ∀ (f : X → E) (f_mem : f ∈ A d) (hf : f x < d), False
Tactic: obtain ⟨f, f_mem, hf⟩ : ∃ f ∈ A d, f x < d := by
    have : x ∈ {y | s y < d} := hd.1
    simpa only [hA d, mem_iUnion₂, exists_prop, U, mem_setOf_eq] using this
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Lindelof (goal)
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
f : X → E
f_mem : f ∈ A d
hf : f x < d
⊢ False
have right : e < e
Tactic: suffices e < e by simpa
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst : TopologicalSpace X₁
inst_1 : TopologicalSpace X₂
inst_2 : TopologicalSpace Z₁
inst_3 : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst, inst_1] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst_2, inst_3] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Function.mapPullback mapX mapY mapZ commX commZ)
have refine_1 : Continuous[instTopologicalSpaceSubtype, inst_1] fun (x : Function.Pullback f₁ g₁) ↦ mapX x.fst
Tactic: refine continuous_induced_rng.mpr (.prodMk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.SeparatedMap (goal)
Goal:
X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst : TopologicalSpace X₁
inst_1 : TopologicalSpace X₂
inst_2 : TopologicalSpace Z₁
inst_3 : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst, inst_1] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst_2, inst_3] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
refine_1 : Continuous[instTopologicalSpaceSubtype, inst_1] fun (x : Function.Pullback f₁ g₁) ↦ mapX x.fst
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Function.mapPullback mapX mapY mapZ commX commZ)
have refine_2 : Continuous[instTopologicalSpaceSubtype, inst_3] fun (x : Function.Pullback f₁ g₁) ↦ mapZ x.snd
Tactic: refine continuous_induced_rng.mpr (.prodMk ?_ ?_)