awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
nhds_b : {0}ᶜ ∈ 𝓝 b
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
Tactic: apply tendsto_indicator_const_iff_forall_eventually' _ b
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    Tendsto.{u_3, u_1} (β := (x : α) → Prop) (fun (i : ι) (x : α) ↦ x ∈ As i) L
      (pi (α := fun (x : α) ↦ Prop) fun (x : α) ↦ pure (x ∈ A))
have rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))
Tactic: rw [tendsto_indicator_const_iff_forall_eventually' _ b nhds_b nhds_o, tendsto_pi]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))
have simp_rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)
Tactic: simp_rw [tendsto_pure]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    Tendsto.{u_3, u_1} (β := (x : α) → Prop) (fun (i : ι) (x : α) ↦ x ∈ As i) L
      (pi (α := fun (x : α) ↦ Prop) fun (x : α) ↦ pure (x ∈ A))
have rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))
Tactic: rw [tendsto_indicator_const_iff_forall_eventually _ b, tendsto_pi]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))
have simp_rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)
Tactic: simp_rw [tendsto_pure]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
Tactic: tfae_have 1 → 2 := (pure_le_nhds _).trans
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
Tactic: tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy)
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
Tactic: tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
Tactic: tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_6_iff_5 : Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
Tactic: tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
have rw : ClusterPt y (𝓟 {x}) ↔ ClusterPt y (pure x)
Tactic: rw [mem_closure_iff_clusterPt, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
rw : ClusterPt y (𝓟 {x}) ↔ ClusterPt y (pure x)
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
have rw₁ : ClusterPt y (pure x) ↔ ClusterPt y (pure x)
Tactic: rw [mem_closure_iff_clusterPt, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
Tactic: tfae_have 5 ↔ 7 := by
    rw [mem_closure_iff_clusterPt, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y
have refine : ∀ (h : Membership.mem (γ := Set X) (closure[inst] {x}) y) (i' : Set X), y ∈ i' ∧ IsOpen[inst] i' → i' ∈ 𝓝 x
Tactic: refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
h : Membership.mem (γ := Set X) (closure[inst] {x}) y
s : Set X
hy : y ∈ s
ho : IsOpen[inst] s
⊢ s ∈ 𝓝 x
have rcases : ∀ (z : X) (hxs : z ∈ s) (tfae_1_to_2 : ∀ (a : z ⤳ y), pure z ≤ 𝓝 y)
  (tfae_2_to_3 : ∀ (a : pure z ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s)
  (tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → z ∈ s) (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s)
  (tfae_4_to_5 :
    ∀ (a : ∀ (s : Set X), IsClosed[inst] s → z ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {z}) y)
  (tfae_6_iff_5 :
    Subset (α := Set X) (closure[inst] {y}) (closure[inst] {z}) ↔ Membership.mem (γ := Set X) (closure[inst] {z}) y)
  (tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {z}) y ↔ ClusterPt y (pure z))
  (h : Membership.mem (γ := Set X) (closure[inst] {z}) y), s ∈ 𝓝 z
Tactic: rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
Cleared hypotheses: x, tfae_1_to_2, tfae_2_to_3, tfae_3_to_4, tfae_4_to_5, tfae_6_iff_5, tfae_5_iff_7, h
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
tfae_2_to_3 : ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s
tfae_3_to_4 : ∀ (a : ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s
tfae_4_to_5 : ∀ (a : ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s), Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_6_iff_5 :
  Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}) ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y
tfae_5_iff_7 : Membership.mem (γ := Set X) (closure[inst] {x}) y ↔ ClusterPt y (pure x)
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s,
      Membership.mem (γ := Set X) (closure[inst] {x}) y, Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x}),
      ClusterPt y (pure x)].TFAE
have tfae_5_to_1 : ∀ (a : Membership.mem (γ := Set X) (closure[inst] {x}) y), x ⤳ y
Tactic: tfae_have 5 → 1 := by
    refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
    rintro s ⟨hy, ho⟩
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
    exact ho.mem_nhds hxs
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ (𝓝 x).ker = {y : X | y ⤳ x}
have h : ∀ (x_1 : X), x_1 ∈ (𝓝 x).ker ↔ Membership.mem (γ := Set X) {y : X | y ⤳ x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : Tendsto g l (𝓝 y)
hl : ∀ (x : X), f x ⤳ g x
⊢ Tendsto f l (𝓝 y)
have simp_all : ∀ (h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l)
  (hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s) (s : Set Y), IsOpen[inst] s → y ∈ s → f ⁻¹' s ∈ l
Tactic: simp_all only [specializes_iff_forall_open, tendsto_nhds]
Cleared hypotheses: h, hl
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → g ⁻¹' s ∈ l
hl : ∀ (x : X) (s : Set Y), IsOpen[inst] s → g x ∈ s → f x ∈ s
⊢ ∀ (s : Set Y), IsOpen[inst] s → y ∈ s → f ⁻¹' s ∈ l
have refine : ∀ (s : Set Y) (ho : IsOpen[inst] s) (hy : y ∈ s) (x : X) (hx : x ∈ g ⁻¹' s), x ∈ f ⁻¹' s
Tactic: refine fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : x ⤳ y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ f x ⤳ f y
have rw : ∀ (h : pure x ≤ 𝓝 y) (hf : ContinuousWithinAt f s y) (hx : x ∈ s), pure (f x) ≤ 𝓝 (f y)
Tactic: rw [specializes_iff_pure] at h ⊢
Cleared hypotheses: h, hf, hx
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S
have rw : (¬∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S
Tactic: rw [specializes_iff_forall_open]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S
have push : (∃ (s : Set X), IsOpen[inst] s ∧ y ∈ s ∧ x ∉ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S
Tactic: push Not
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S
have rw : (¬∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S
Tactic: rw [specializes_iff_forall_closed]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S
have push : (∃ (s : Set X), IsClosed[inst] s ∧ x ∈ s ∧ y ∉ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S
Tactic: push Not
-- Lean 4 proof step from Mathlib.Topology.Inseparable (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
⊢ Continuous[inst, inst_1] (s.piecewise (β := fun (a : X) ↦ Y) f g)
have this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
Tactic: have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ Continuous[inst, inst_1] (s.piecewise (β := fun (a : X) ↦ Y) f g)
have rw : ∀ (s_1 : Set Y), IsOpen[inst_1] s_1 → IsOpen[inst] (s.piecewise (β := fun (a : X) ↦ Y) f g ⁻¹' s_1)
Tactic: rw [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst_1] U
⊢ IsOpen[inst] (s.piecewise (β := fun (a : X) ↦ Y) f g ⁻¹' U)
have rw : IsOpen[inst] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)
Tactic: rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 t
⊢ ∃ x ∈ t, ClusterPt x f
have obtain : ∀ (x : X) (hxs : x ∈ s) (hxf : ClusterPt x f), ∃ x ∈ t, ClusterPt x f
Tactic: obtain ⟨x, hxs, hxf⟩ := hs <| hf.trans <| Filter.monotone_principal hts
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 t
x : X
hxs : x ∈ s
hxf : ClusterPt x f
⊢ ∃ x ∈ t, ClusterPt x f
have obtain : ∀ (y : X) (hyt : y ∈ t) (hxy : x ⤳ y), ∃ x ∈ t, ClusterPt x f
Tactic: obtain ⟨y, hyt, hxy⟩ := h x hxs
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = s
have refine_1 : ∀ (H : StableUnderSpecialization s) (s_1 : Set X),
  Membership.mem (γ := Set (Set X)) ((fun (x : X) ↦ closure[inst] {x}) '' s) s_1 → IsClosed[inst] s_1
Tactic: refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (H : StableUnderSpecialization s) (s_1 : Set X),
    Membership.mem (γ := Set (Set X)) ((fun (x : X) ↦ closure[inst] {x}) '' s) s_1 → IsClosed[inst] s_1
⊢ StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = s
have refine_2 : ∀ (H : StableUnderSpecialization s), ⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s) = s
Tactic: refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
| s
have rw : ⋃ x ∈ s, closure[inst] {x}
Tactic: rw [← H.Union_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s) = s
have refine_2 : Eq (α := Set X) (⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s)) (⋃ x ∈ s, closure[inst] {x})
Tactic: conv_rhs => rw [← H.Union_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s
have refine : StableUnderGeneralization s → ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s
Tactic: refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s → ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s
have rw : (∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = sᶜ) →
  ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s
Tactic: rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
have simp : (∀ ⦃a : X⦄ ⦃b : Y⦄,
    Membership.mem (γ := Set Y) (closure[inst_1] {f a}) b →
      ∃ (a' : X), Membership.mem (γ := Set X) (closure[inst] {a}) a' ∧ f a' = b) ↔
  ∀ (x : X), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
Tactic: simp only [SpecializingMap, Relation.Fibration, flip, specializes_iff_mem_closure]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ SpecializingMap f ↔ ∀ (x : X), IsClosed[inst_1] (f '' closure[inst] {x})
have refine : ∀ (h : SpecializingMap f) (x : X), IsClosed[inst_1] (f '' closure[inst] {x})
Tactic: refine ⟨fun h x ↦ ?_, fun h ↦ specializingMap_iff_stableUnderSpecialization_image_singleton.mpr
    (fun x ↦ (h x).stableUnderSpecialization)⟩
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst_1] (f '' closure[inst] {x})
have rw : IsClosed[inst_1] (closure[inst_1] {f x})
Tactic: rw [(specializingMap_iff_closure_singleton hf).mp h x]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : SpecializingMap f
hg : SpecializingMap g
⊢ SpecializingMap (g ∘ f)
have simp : ∀ (hf : ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s))
  (hg : ∀ (s : Set Y), StableUnderSpecialization s → StableUnderSpecialization (g '' s)) (s : Set X),
  StableUnderSpecialization s → StableUnderSpecialization (g '' f '' s)
Tactic: simp only [specializingMap_iff_stableUnderSpecialization_image, Set.image_comp] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x : X
y : Y
e : flip (fun (x1 x2 : Y) ↦ x1 ⤳ x2) y (f x)
⊢ ∃ (a' : X), flip (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have obtain : ∀ (y : X) (e : flip (fun (x1 x2 : Y) ↦ x1 ⤳ x2) (f y) (f x)),
  ∃ (a' : X), flip (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y
Tactic: obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩
Cleared hypotheses: y, e