awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
refine_1 : ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine_2 : ⋂ i ∈ is, U i ∈ 𝓝 x
Tactic: refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
refine_1 : ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
refine_2 : ⋂ i ∈ is, U i ∈ 𝓝 x
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine_3 : ∀ (z : X) (hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i),
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
Tactic: refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (hypothesis)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ z ∈ n
have hz₁ : z ∈ n ∩ ((⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i)
Tactic: rw [inter_assoc] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (hypothesis)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have hzn : z ∈ n
Tactic: have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (hypothesis)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
hzn : z ∈ n
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have hz₁ : Membership.mem (γ := Set X) (⋂ j ∈ js, (mulTSupport (f j))ᶜ) z
Tactic: replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (hypothesis)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : Membership.mem (γ := Set X) (⋂ j ∈ js, (mulTSupport (f j))ᶜ) z
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have hz₁ : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
Tactic: simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i), x ∈ U i
Tactic: refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (hypothesis)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
⊢ x ∈ U i
have hz₁ : x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
Tactic: specialize hz i ⟨z, ⟨hi, hzn⟩⟩
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
hz : x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ x ∈ U i
have contrapose : ∀ (hz : x ∉ U i), ¬(x ∉ U i → z ∈ (mulTSupport (f i))ᶜ)
Tactic: contrapose hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine_3 : (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
  (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
Tactic: suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
⊢ i ∈ (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
have refine_3 : (mulSupport (f i) ∩ n).Nonempty
Tactic: simp only [Finite.coe_toFinset, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
let let₁ let₂ let₃ :
  ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine_1 : let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
Tactic: classical
    let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
      intro i hi
      simp only [Finite.coe_toFinset, mem_setOf_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
let let₁ let₂ let₃ :
  ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
refine_1 :
  let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
  ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine_2 : let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
⋂ i ∈ is, U i ∈ 𝓝 x
Tactic: classical
    let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
      intro i hi
      simp only [Finite.coe_toFinset, mem_setOf_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
let let₁ let₂ let₃ :
  ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
refine_1 :
  let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
  ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
refine_2 :
  let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
  ⋂ i ∈ is, U i ∈ 𝓝 x
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
have refine_3 : let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
∀ (z : X) (hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i),
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
Tactic: classical
    let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz
      suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
      intro i hi
      simp only [Finite.coe_toFinset, mem_setOf_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
s : ι → X → R
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
⊢ (s i • f i) x = 0
have rw : s i x • f i x = 0
Tactic: rw [Pi.smul_apply', h, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
s : ι → X → R
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
rw : s i x • f i x = 0
⊢ (s i • f i) x = 0
have rw₁ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) 0 (f i x) = 0
Tactic: rw [Pi.smul_apply', h, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
s : ι → X → R
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
rw : s i x • f i x = 0
rw₁ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) 0 (f i x) = 0
⊢ (s i • f i) x = 0
have rw₂ : Eq.{u_7 + 1} (α := M) 0 0
Tactic: rw [Pi.smul_apply', h, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : ι → X → M
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ (s i • f i) x = 0
have rw : s i x • f i x = 0
Tactic: rw [Pi.smul_apply', h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : ι → X → M
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
rw : s i x • f i x = 0
⊢ (s i • f i) x = 0
have rw₁ : HSMul.hSMul (β := M) (s i x) 0 = 0
Tactic: rw [Pi.smul_apply', h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : ι → X → M
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
rw : s i x • f i x = 0
rw₁ : HSMul.hSMul (β := M) (s i x) 0 = 0
⊢ (s i • f i) x = 0
have rw₂ : Eq.{u_7 + 1} (α := M) 0 0
Tactic: rw [Pi.smul_apply', h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
inst_2 : MonoidWithZero S
inst_3 : TopologicalSpace S
F : Type u_3
inst_4 : FunLike F R S
inst_5 : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst, inst_3] (⇑φ : (a : R) → S)
a : R
ha : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := S) (fun (x : ℕ) ↦ HPow.hPow (α := S) ((φ : (a : R) → S) a : S) x) atTop (𝓝 0)
have simp_rw : Tendsto.{0, u_2} (β := S) (fun (x : ℕ) ↦ (φ : (a : R) → S) (a ^ x)) atTop (𝓝 0)
Tactic: simp_rw [← map_pow]
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
x : ℕ
hi : x ≥ 1
⊢ HPow.hPow (α := R) 0 x = 0
have rw : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
ha : IsNilpotent a
⊢ IsTopologicallyNilpotent a
have obtain : ∀ (n : ℕ) (hn : a ^ n = 0), IsTopologicallyNilpotent a
Tactic: obtain ⟨n, hn⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
⊢ IsTopologicallyNilpotent a
have apply : ∀ i ≥ n, a ^ i = 0
Tactic: apply tendsto_atTop_of_eventually_const (i₀ := n)
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
⊢ a ^ i = 0
have rw : a ^ (n + (i - n)) = 0
Tactic: rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
rw : a ^ (n + (i - n)) = 0
⊢ a ^ i = 0
have rw₁ : a ^ n * a ^ (i - n) = 0
Tactic: rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
rw : a ^ (n + (i - n)) = 0
rw₁ : a ^ n * a ^ (i - n) = 0
⊢ a ^ i = 0
have rw₂ : 0 * a ^ (i - n) = 0
Tactic: rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.TopologicallyNilpotent (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
rw : a ^ (n + (i - n)) = 0
rw₁ : a ^ n * a ^ (i - n) = 0
rw₂ : 0 * a ^ (i - n) = 0
⊢ a ^ i = 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]