awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
⊢ ⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x
have refine : IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
Tactic: refine IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
this : IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
have rwa : ∀ (this : IsOpen[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))ᶜ), IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
Tactic: rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
this : IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))
rwa :
  ∀ (this : IsOpen[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))ᶜ), IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
have rwa₁ : ∀ (this : IsOpen[inst] (⋂ (i : { i : ι // x ∉ f i }), (f (↑i : ι))ᶜ)), IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
Tactic: rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
this : IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))
rwa :
  ∀ (this : IsOpen[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))ᶜ), IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
rwa₁ :
  ∀ (this : IsOpen[inst] (⋂ (i : { i : ι // x ∉ f i }), (f (↑i : ι))ᶜ)),
    IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
have rwa₂ : ∀
  (this :
    IsOpen[inst] (⋂ (x_1 : ι), ⋂ (hx : x ∉ f x_1), (f (↑(Subtype.mk (p := fun (x_2 : ι) ↦ x ∉ f x_2) x_1 hx) : ι))ᶜ)),
  IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
Tactic: rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst] (f i)
x : X
⊢ IsOpen[inst] (⋂ (i : ι), ⋂ (_ : x ∉ f i), (f i)ᶜ)
have suffices : IsClosed[inst] (⋃ (i : { i : ι // x ∉ f i }), f (↑i : ι))
Tactic: suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
    rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite.{0, u_4} (X := X) fun (n : ℕ) ↦ {x : X | f (n + 1) x ≠ f n x}
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
have choose : ∀ (U : (x : X) → Set X) (hUx : ∀ (x : X), U x ∈ 𝓝 x)
  (hU :
    ∀ (x : X),
      Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}),
  ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
Tactic: choose U hUx hU using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
have choose : ∀ (N : (x : X) → ℕ)
  (hN :
    ∀ (x : X),
      Membership.mem (γ := Set ℕ)
        (upperBounds {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}) (N x)),
  ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
Tactic: choose N hN using fun x => (hU x).bddAbove
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (hypothesis)
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN :
  ∀ (x : X),
    Membership.mem (γ := Set ℕ)
      (upperBounds {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}) (N x)
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
have hN₁ : ∀ (x : X), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y
Tactic: replace hN : ∀ (x), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y :=
    fun x n hn y hy => by_contra fun hne => hn.lt.not_ge <| hN x ⟨y, hne, hy⟩
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (hypothesis)
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
have hN₁ : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
Tactic: replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y :=
    fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
⊢ ∃ (F : (x : X) → π x),
    ∀ (x : X), ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x), Eq (α := π p.2) (f p.1 p.2) (F p.2)
have refine : ∀ (x : X),
  ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x),
    Eq (α := π p.2) (f p.1 p.2) ((fun (x : X) ↦ f (N x + 1) x) p.2)
Tactic: refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : (x : X) → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite (α := ℕ) {i : ℕ | ((fun (n : ℕ) ↦ ({x : X | f (n + 1) x ≠ f n x} : Set X)) i ∩ U x).Nonempty}
N : (x : X) → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
⊢ ∀ᶠ (p : ℕ × X) in SProd.sprod (α := Filter ℕ) atTop (𝓝 x),
    Eq (α := π p.2) (f p.1 p.2) ((fun (x : X) ↦ f (N x + 1) x) p.2)
have h : ∀ a ∈ SProd.sprod (α := Set ℕ) {x_1 : ℕ | N x < x_1} (U x), Eq (α := π a.2) (f a.1 a.2) (f (N a.2 + 1) a.2)
Tactic: filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)
have rw : LocallyFinite (ι := ι)
      (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι)) Sum.inl) ∧
    LocallyFinite (ι := PUnit.{1})
      (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι)) Sum.inr) ↔
  LocallyFinite (f ∘ some)
Tactic: rw [← (Equiv.optionEquivSumPUnit.{0, _} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite (ι := ι)
        (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι))
          Sum.inl) ∧
      LocallyFinite (ι := PUnit.{1})
        (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι))
          Sum.inr) ↔
    LocallyFinite (f ∘ some)
have simp : LocallyFinite (ι := ι)
    (comp (β := ι ⊕ PUnit.{1}) (f ∘ (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{1}) → Option ι)) Sum.inl) ↔
  LocallyFinite (f ∘ some)
Tactic: simp only [locallyFinite_of_finite, and_true]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (goal)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst] (s i)
x : X
⊢ ∀ᶠ (y : X) in 𝓝 x, Subset.{u_1} (α := Set ι) {i : ι | y ∈ s i} {i : ι | x ∈ s i}
have h : ∀ (y : X) (hy : Membership.mem (γ := Set X) (⋂ (i : ι), ⋂ (_ : x ∉ s i), (s i)ᶜ) y) ⦃i : ι⦄
  (hi : Membership.mem (γ := Set ι) {i : ι | y ∈ s i} i), Membership.mem (γ := Set ι) {i : ι | x ∈ s i} i
Tactic: filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi
-- Lean 4 proof step from Mathlib.Topology.LocallyFinite (hypothesis)
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst] (s i)
x y : X
hy : Membership.mem (γ := Set X) (⋂ (i : ι), ⋂ (_ : x ∉ s i), (s i)ᶜ) y
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | y ∈ s i} i
⊢ Membership.mem (γ := Set ι) {i : ι | x ∈ s i} i
have hy₁ : ∀ (i : ι) (i_1 : x ∉ s i), y ∉ s i
Tactic: push _ ∈ _ at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ support.{u_1, u_2} (M := Y) fun (x : X) ↦ 0).Finite
have simp_rw : ∃ (t : Set X), t ∈ 𝓝 z
Tactic: simp_rw [support_fun_zero, inter_empty, finite_empty, and_true]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
z : X
hz : z ∈ U
w : Set X
⊢ ∃ (t : Set X), t ∈ 𝓝 z
have h : univ ∈ 𝓝 z
Tactic: use Set.univ, univ_mem
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
⊢ support f = U \ {x : X | f x = 0 x}
have h₁ : ∀ (x : X), x ∈ support f ↔ x ∈ U \ {x : X | f x = 0 x}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
x : X
⊢ x ∈ support f ↔ x ∈ U \ {x : X | f x = 0 x}
have h₁ : ¬f x = 0 → x ∈ U
Tactic: simp only [mem_support, ne_eq, Pi.zero_apply, mem_diff, mem_setOf_eq, iff_and_self]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
have this : support f = U \ {x : X | f x = 0 x}
Tactic: have : f.support = (U \ {x | f x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, mem_diff, mem_setOf_eq, iff_and_self]
    exact (h ·)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x : X | f x = 0 x}
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
have rw : (∀ᶠ (x : X) in codiscreteWithin U, f x = 0 x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
Tactic: rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x : X | f x = 0 x}
rw : (∀ᶠ (x : X) in codiscreteWithin U, f x = 0 x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
have rw₁ : {x : X | f x = 0 x} ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
Tactic: rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x : X | f x = 0 x}
rw : (∀ᶠ (x : X) in codiscreteWithin U, f x = 0 x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
rw₁ : {x : X | f x = 0 x} ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
have rw₂ : (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
Tactic: rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x : X | f x = 0 x}
rw : (∀ᶠ (x : X) in codiscreteWithin U, f x = 0 x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
rw₁ : {x : X | f x = 0 x} ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
rw₂ : (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
have rw₃ : (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite) ↔
  ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite
Tactic: rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
⊢ (∀ (x : X),
      ∃ t ∈ 𝓝 x,
        Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty}) ↔
    LocallyFiniteSupport f
have h : ∀ (z : X) (t : Set X) (ht : t ∈ 𝓝 z),
  Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty} ↔
    (t ∩ support f).Finite
Tactic: peel with z t ht
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
⊢ Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty} ↔
    (t ∩ support f).Finite
have aux1 : t ∩ support f =
  image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
    {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
Tactic: have aux1 : t ∩ f.support = {i : f.support | ↑i ∈ t} := by aesop
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
aux1 :
  t ∩ support f =
    image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
⊢ Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty} ↔
    (t ∩ support f).Finite
have aux2 : InjOn.{u_1, u_1} (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
  {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
Tactic: have aux2 : InjOn Subtype.val {i : f.support | ↑i ∈ t} := by aesop
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
⊢ (W ∩ support f).Finite
have this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
Tactic: have := LocallyFinite.finite_nonempty_inter_compact
    (LocallyFiniteSupport.locallyFinite_support f h) hW
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
⊢ (W ∩ support f).Finite
have lem : ∀ {α : Type u_1} (s t : Set α),
  image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
    t ∩ s
Tactic: have lem {α : Type u_1} (s t : Set α) : {i : s | ({↑i} ∩ t).Nonempty} = (t ∩ s) := by aesop
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
lem :
  ∀ {α : Type u_1} (s t : Set α),
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
      t ∩ s
⊢ (W ∩ support f).Finite
have rw : Set.Finite.{u_1} (α := X)
  (image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
    {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty})
Tactic: rw [← lem f.support W]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x₁ x₂ : X
y : Y
⊢ (single x₁ y : (a : X) → Y) x₂ = if x₂ = x₁ then y else 0
have simp_rw : toFun (U := univ) (single x₁ y) x₂ = if x₂ = x₁ then y else 0
Tactic: simp_rw [DFunLike.coe, single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x₁ x₂ : X
y : Y
simp_rw : toFun (U := univ) (single x₁ y) x₂ = if x₂ = x₁ then y else 0
⊢ (single x₁ y : (a : X) → Y) x₂ = if x₂ = x₁ then y else 0
have simp_rw₁ : Pi.single (M := fun (a : X) ↦ Y) x₁ y x₂ = if x₂ = x₁ then y else 0
Tactic: simp_rw [DFunLike.coe, single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x₁ x₂ : X
y : Y
⊢ (single x₁ y : (a : X) → Y) x₂ = if x₂ = x₁ then y else 0
have simp_rw : toFun (U := univ) (single x₁ y) x₂ = if x₂ = x₁ then y else 0
Tactic: classical
  simp_rw [DFunLike.coe, single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x₁ x₂ : X
y : Y
simp_rw : toFun (U := univ) (single x₁ y) x₂ = if x₂ = x₁ then y else 0
⊢ (single x₁ y : (a : X) → Y) x₂ = if x₂ = x₁ then y else 0
have simp_rw₁ : Pi.single (M := fun (a : X) ↦ Y) x₁ y x₂ = if x₂ = x₁ then y else 0
Tactic: classical
  simp_rw [DFunLike.coe, single, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x : X
y : Y
⊢ Eq (α := (a : X) → Y) (⇑(single x y) : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y)
have h : ∀ (x_1 : X), Eq.{u_2 + 1} (α := Y) ((single x y : (a : X) → Y) x_1 : Y) (Pi.single (M := fun (j : X) ↦ Y) x y x_1 : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
⊢ EventuallyEq.{u_1, u_2} (β := Y) (codiscreteWithin U) (⇑D : (a : X) → Y) 0
have apply : ∀ z ∈ U,
  ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x})).Finite
Tactic: apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
⊢ D.support (U := U) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
have h : ∀ (x : X), x ∈ D.support (U := U) ↔ x ∈ U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ D.support (U := U) ↔ x ∈ U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
have h : ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) → x ∈ U
Tactic: simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_diff, Set.mem_setOf_eq, iff_and_self]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
⊢ ∀ z ∈ U,
    ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x})).Finite
have this : D.support (U := U) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
Tactic: have : D.support = (U \ {x | D x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_diff, Set.mem_setOf_eq, iff_and_self]
    exact (support_subset_iff.1 D.supportWithinDomain) x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
⊢ ∀ z ∈ U,
    ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x})).Finite
have rw : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support (U := U)).Finite
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
⊢ D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
have h : ∀ (x : X), x ∈ D.support (U := U) ↔ x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ D.support (U := U) ↔ x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
have h : x ∈ D.support (U := U) → x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
x : X
h : x ∈ D.support (U := U) → x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
⊢ x ∈ D.support (U := U) ↔ x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
have h₁ : x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U → x ∈ D.support (U := U)
Tactic: constructor