awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
⊢ Membership.mem (γ := Set (Set X)) ((((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X) d) x ↔
    Membership.mem (γ := Set (Set X))
      (match (motive := DiscreteQuotient X → Set (Set X)) d with
        | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
        Set (Set X))
      x
have h : (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) ↔ ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
Tactic: simp only [Setoid.classes, Set.mem_setOf_eq, Function.comp_apply,
    finsetClopens, Set.coe_toFinset, Set.mem_image, Set.mem_range,
    exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
⊢ (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) ↔ ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
have h : (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) → ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h : (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) → ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
⊢ (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) ↔ ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
have h₁ : (∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}) → ∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
⊢ (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) → ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
have h : (∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x) →
  ∀ (y : Quotient d.toSetoid) (h : d.proj ⁻¹' {y} = x), x = {x : X | (d.toSetoid : X → X → Prop) x y.out}
Tactic: refine fun ⟨y, h⟩ ↦ ⟨Quotient.out (s := d.toSetoid) y, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h_1 : ∃ (a : Quotient d.toSetoid), d.proj ⁻¹' {a} = x
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x
⊢ x = {x : X | (d.toSetoid : X → X → Prop) x y.out}
have h₁ : ∀ (x_1 : X), x_1 ∈ x ↔ Membership.mem (γ := Set X) {x : X | (d.toSetoid : X → X → Prop) x y.out} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
d : DiscreteQuotient X
x : Set X
h_1 : ∃ (y : X), x = {x : X | (d.toSetoid : X → X → Prop) x y}
y : X
h : x = {x : X | (d.toSetoid : X → X → Prop) x y}
⊢ d.proj ⁻¹' {d.proj y} = x
have h₁ : ∀ (x_1 : X), x_1 ∈ d.proj ⁻¹' {d.proj y} ↔ x_1 ∈ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
⊢ Injective (α := DiscreteQuotient X) (finsetClopens X)
have apply : Injective (α := DiscreteQuotient X) (β := Set (Set X))
  (((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)
Tactic: apply Function.Injective.of_comp (f := Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ (↑))
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
⊢ Injective (α := DiscreteQuotient X) (β := Set (Set X))
    (((image fun (t : Clopens X) ↦ t.carrier) ∘ SetLike.coe) ∘ finsetClopens X)
have rw : Injective (β := Set (Set X)) fun (x : DiscreteQuotient X) ↦
  match (motive := DiscreteQuotient X → Set (Set X)) x with
  | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes
Tactic: rw [comp_finsetClopens]
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
⊢ ∀ ⦃a₂ : DiscreteQuotient X⦄,
    Eq.{u_2 + 1} (α := Set (Set X))
        ((fun (x : DiscreteQuotient X) ↦
            (match (motive := DiscreteQuotient X → Set (Set X)) x with
              | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
              Set (Set X)))
          { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
        ((fun (x : DiscreteQuotient X) ↦
            (match (motive := DiscreteQuotient X → Set (Set X)) x with
              | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
              Set (Set X)))
          a₂) →
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X } = a₂
have this : ∀ (toSetoid_1 : Setoid X) (isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))),
  Eq.{u_2 + 1} (α := Set (Set X))
      ((fun (x : DiscreteQuotient X) ↦
          (match (motive := DiscreteQuotient X → Set (Set X)) x with
            | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
            Set (Set X)))
        { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
      ((fun (x : DiscreteQuotient X) ↦
          (match (motive := DiscreteQuotient X → Set (Set X)) x with
            | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
            Set (Set X)))
        { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 }) →
    { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X } =
      { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 }
Tactic: ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteQuotient (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
toSetoid : Setoid X
isOpen_setOf_rel : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid : X → X → Prop) x))
toSetoid_1 : Setoid X
isOpen_setOf_rel_1 : ∀ (x : X), IsOpen[inst] (setOf ((toSetoid_1 : X → X → Prop) x))
h :
  Eq.{u_2 + 1} (α := Set (Set X))
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel })
    ((fun (x : DiscreteQuotient X) ↦
        (match (motive := DiscreteQuotient X → Set (Set X)) x with
          | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes :
          Set (Set X)))
      { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 })
⊢ { toSetoid := toSetoid, isOpen_setOf_rel := isOpen_setOf_rel : DiscreteQuotient X } =
    { toSetoid := toSetoid_1, isOpen_setOf_rel := isOpen_setOf_rel_1 }
have e_toSetoid : toSetoid = toSetoid_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
have simp_rw : (∀ (x : (↑S : Type u_2)), 𝓝[≠] x = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
Tactic: simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
simp_rw : (∀ (x : (↑S : Type u_2)), 𝓝[≠] x = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
⊢ DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
have simp_rw₁ : (∀ (x : (↑S : Type u_2)), 𝓝[≠] x = ⊥) ↔ ∀ (x : (↑S : Type u_2)), 𝓝[≠] (↑x : Y) ⊓ 𝓟 S = ⊥
Tactic: simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
⊢ IsDiscrete S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
have rw : DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
Tactic: rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
rw : DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
⊢ IsDiscrete S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
have rw₁ : (∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
Tactic: rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
have simp : (∀ (a : Y) (b : a ∈ S), ∃ (t : Set Y), IsOpen[inst] t ∧ ∀ (a_1 : Y) (b : a_1 ∈ S), a_1 ∈ t ↔ a_1 = a) ↔
  ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ ∀ (x : Y), x ∈ U ∧ x ∈ S ↔ x = y
Tactic: simp [discreteTopology_iff_isOpen_singleton, isOpen_induced_iff, Set.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
⊢ IsDiscrete S ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
have rw : DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
Tactic: rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff']
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
Y : Type u_2
inst : TopologicalSpace Y
S : Set Y
rw : DiscreteTopology.{u_2} (↑S : Type u_2) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
⊢ IsDiscrete S ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
have rw₁ : (∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}) ↔ ∀ y ∈ S, ∃ (U : Set Y), IsOpen[inst] U ∧ U ∩ S = {y}
Tactic: rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff']
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
⊢ IsDiscrete (f '' s)
have refine : ∀ x ∈ f '' s, 𝓝[f '' s] x ≤ pure x
Tactic: refine .of_nhdsWithin ?_
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝[f '' s] f x ≤ pure (f x)
have rw : 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)
Tactic: rw [← map_pure, ← hs.nhdsWithin x hx, nhdsWithin, nhdsWithin, map_inf hf', map_principal]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)
have grw : map f (𝓝 x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)
Tactic: grw [hf.nhds_le x]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
⊢ IsDiscrete (f '' s)
have refine : ∀ x ∈ f '' s, 𝓝[f '' s] x ≤ pure x
Tactic: refine .of_nhdsWithin ?_
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst] s
x : X
hx : x ∈ s
⊢ 𝓝[f '' s] f x ≤ pure (f x)
have rw : 𝓝 (f x) ≤ map f (𝓝 x)
Tactic: rw [(hf _ hs').nhdsWithin_eq ⟨x, hx, rfl⟩, ← map_pure, ← hs.nhdsWithin x hx, hs'.nhdsWithin_eq hx]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
⊢ IsDiscrete (f ⁻¹' s)
have refine : ∀ (x : X) (hx : x ∈ f ⁻¹' s), 𝓝[f ⁻¹' s] x ≤ pure x
Tactic: refine .of_nhdsWithin fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ 𝓝[f ⁻¹' s] x ≤ pure x
have rw : Tendsto f (𝓝[f ⁻¹' s] x) (𝓝[s] f x)
Tactic: rw [← map_le_map_iff hf', map_pure, ← hs.nhdsWithin _ hx, ← Tendsto]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
⊢ IsDiscrete (f ⁻¹' s)
have refine : ∀ (x : X) (hx : x ∈ f ⁻¹' s), 𝓝[f ⁻¹' s] x ≤ pure x
Tactic: refine .of_nhdsWithin fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
⊢ 𝓝[f ⁻¹' s] x ≤ pure x
have h : 𝓝[f ⁻¹' {f x}] x ≤ pure x
Tactic: have h := ((H (f x)).nhdsWithin _ rfl).le
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
⊢ Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
have rw : (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
Tactic: rw [hasBasis_cocompact.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
have refine : ∀ (K : Set Y), IsCompact K → ((∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite)
Tactic: refine forall₂_congr (fun K _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
⊢ DiscreteTopology X
have refine : ∀ (x : X), IsOpen[inst] {x}
Tactic: refine discreteTopology_iff_isOpen_singleton.mpr (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
⊢ IsOpen[inst] {x}
have obtain : ∀ (K : Set Y) (hK : IsCompact K) (hK' : K ∈ 𝓝 (f x)), IsOpen[inst] {x}
Tactic: obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen[inst] {x}
have obtain : ∀ (U : Set Y) (hU₁ : U ⊆ K) (hU₂ : IsOpen[inst_1] U) (hU₃ : f x ∈ U), IsOpen[inst] {x}
Tactic: obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
inst_3 : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst, inst_1] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen[inst_1] U
hU₃ : f x ∈ U
⊢ IsOpen[inst] {x}
have hU₄ : (f ⁻¹' U).Finite
Tactic: have hU₄ : Set.Finite (f ⁻¹' U) :=
    Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f cofinite (cocompact Y)
have h : cofinite = cocompact X
Tactic: convert! hf
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X
have h : Eq.{u_1 + 1} (α := Filter X) cofinite cofinite
Tactic: rw [cocompact_eq_cofinite X]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ IsClosed[inst] S ∧ IsDiscrete S ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
have rw : (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: rw [isDiscrete_iff_nhdsNE, isClosed_iff_clusterPt, ← forall_and]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
have a : ∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: congrm (∀ x, ?_)
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
⊢ (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
have a : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ← disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
have a : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) → Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
a : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) → Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
have a₁ : Disjoint (𝓝[≠] x) (𝓟 S) → (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
⊢ Disjoint (𝓝[≠] x) (𝓟 S)
have pos : ∀ (hx : x ∈ S), Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: by_cases hx : x ∈ S
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
pos : ∀ (hx : x ∈ S), Disjoint (𝓝[≠] x) (𝓟 S)
⊢ Disjoint (𝓝[≠] x) (𝓟 S)
have neg : ∀ (hx : x ∉ S), Disjoint (𝓝[≠] x) (𝓟 S)
Tactic: by_cases hx : x ∈ S
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
have a : ∀ (hx : x ∉ S), Disjoint (𝓝 x) (𝓟 S)
Tactic: refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))
have simp : (∀ (i : X) (i_1 : i ∈ T), ∃ (u : Set X), IsOpen[inst] u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
  ∀ x ∈ T, ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)
Tactic: simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
    mem_diff, mem_inter_iff, mem_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
⊢ (∀ (i : X) (i_1 : i ∈ T), ∃ (u : Set X), IsOpen[inst] u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)
have a : ∀ (x : X) (u : Set X) (y : X), y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
Tactic: congr! 7 with x - u y
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DiscreteSubset (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
have a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
Tactic: tauto