awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
simp_rw₁ : (¬∀ t ∈ 𝓝 x, (t ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₂ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), ¬(x_1 ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw₃ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
simp_rw₁ : (¬∀ t ∈ 𝓝 x, (t ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₂ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), ¬(x_1 ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₃ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw₄ : (∃ x_1 ∈ 𝓝 x, x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
simp_rw₁ : (¬∀ t ∈ 𝓝 x, (t ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₂ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), ¬(x_1 ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₃ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
simp_rw₄ : (∃ x_1 ∈ 𝓝 x, x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw₅ : (∃ x_1 ∈ 𝓝 x, Disjoint x_1 (mulSupport f)) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
simp_rw₁ : (¬∀ t ∈ 𝓝 x, (t ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₂ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), ¬(x_1 ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
simp_rw₃ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
simp_rw₄ : (∃ x_1 ∈ 𝓝 x, x_1 ∩ mulSupport f = ∅) ↔ f =ᶠ[𝓝 x] 1
simp_rw₅ : (∃ x_1 ∈ 𝓝 x, Disjoint x_1 (mulSupport f)) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw₆ : (∃ x_1 ∈ 𝓝 x, EqOn f 1 x_1) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : R1Space α
⊢ (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
have simp_rw : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, x ∉ mulSupport f) ↔ HasCompactMulSupport f
Tactic: simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : R1Space α
simp_rw : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, x ∉ mulSupport f) ↔ HasCompactMulSupport f
⊢ (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
have simp_rw₁ : (∃ (K : Set α), IsCompact K ∧ ∀ x ∈ Kᶜ, x ∈ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
Tactic: simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : R1Space α
simp_rw : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, x ∉ mulSupport f) ↔ HasCompactMulSupport f
simp_rw₁ : (∃ (K : Set α), IsCompact K ∧ ∀ x ∈ Kᶜ, x ∈ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
⊢ (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
have simp_rw₂ : (∃ (K : Set α), IsCompact K ∧ Kᶜ ⊆ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
Tactic: simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : R1Space α
simp_rw : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, x ∉ mulSupport f) ↔ HasCompactMulSupport f
simp_rw₁ : (∃ (K : Set α), IsCompact K ∧ ∀ x ∈ Kᶜ, x ∈ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
simp_rw₂ : (∃ (K : Set α), IsCompact K ∧ Kᶜ ⊆ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
⊢ (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
have simp_rw₃ : (∃ (K : Set α), IsCompact K ∧ mulSupport f ⊆ K) ↔ HasCompactMulSupport f
Tactic: simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : R1Space α
simp_rw : (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, x ∉ mulSupport f) ↔ HasCompactMulSupport f
simp_rw₁ : (∃ (K : Set α), IsCompact K ∧ ∀ x ∈ Kᶜ, x ∈ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
simp_rw₂ : (∃ (K : Set α), IsCompact K ∧ Kᶜ ⊆ (mulSupport f)ᶜ) ↔ HasCompactMulSupport f
simp_rw₃ : (∃ (K : Set α), IsCompact K ∧ mulSupport f ⊆ K) ↔ HasCompactMulSupport f
⊢ (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
have simp_rw₄ : (∃ (K : Set α), IsCompact K ∧ mulSupport f ⊆ K) ↔ IsCompact (closure[inst] (mulSupport f))
Tactic: simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst] K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ K
have rw : mulTSupport f ⊆ closure[inst] K
Tactic: rw [← h'K.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (hypothesis)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst] K
hfK : ∀ x ∉ K, f x = 1
⊢ HasCompactMulSupport f
have this : mulTSupport f ⊆ K
Tactic: have : mulTSupport f ⊆ K := by
    rw [← h'K.closure_eq]
    apply closure_mono (mulSupport_subset_iff'.2 hfK)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
inst_2 : TopologicalSpace β
hf : Continuous[inst, inst_2] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
⊢ IsCompact (range f)
have inl : ∀ (h2 : range f = f '' K), IsCompact (range f)
Tactic: rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
inst_2 : TopologicalSpace β
hf : Continuous[inst, inst_2] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
inl : ∀ (h2 : range f = f '' K), IsCompact (range f)
⊢ IsCompact (range f)
have inr : ∀ (h2 : range f = insert 1 (f '' K)), IsCompact (range f)
Tactic: rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
inst_2 : TopologicalSpace β
hf : Continuous[inst, inst_2] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = f '' K
⊢ IsCompact (range f)
have inl : IsCompact (f '' K)
Tactic: rw [h2]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
inst_2 : TopologicalSpace β
hf : Continuous[inst, inst_2] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = insert 1 (f '' K)
⊢ IsCompact (range f)
have inr : IsCompact (insert 1 (f '' K))
Tactic: rw [h2]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace α'
inst_2 : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)
have rw : IsCompact (closure[inst_1] (g ⁻¹' mulSupport f))
Tactic: rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace α'
inst_2 : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure[inst_1] (g ⁻¹' mulSupport f))
have refine : closure[inst_1] (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
Tactic: refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace α'
inst_2 : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ closure[inst_1] (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
have rw : g ⁻¹' closure[inst] (g '' g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
Tactic: rw [hg.isEmbedding.closure_eq_preimage_closure_image]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
inst_3 : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport.{u_2, u_6} (β := δ) fun (x : α) ↦ m (f x) (f₂ x)
have rw : ∀ (hf : f =ᶠ[coclosedCompact α] 1) (hf₂ : f₂ =ᶠ[coclosedCompact α] 1) (hm : m 1 1 = 1),
  EventuallyEq.{u_2, u_6} (β := δ) (coclosedCompact α) (fun (x : α) ↦ m (f x) (f₂ x)) 1
Tactic: rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢
Cleared hypotheses: hf, hf₂, hm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
inst_3 : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ EventuallyEq.{u_2, u_6} (β := δ) (coclosedCompact α) (fun (x : α) ↦ m (f x) (f₂ x)) 1
have h : ∀ (x : α) (hx : f x = 1 x) (hx₂ : f₂ x = 1 x), m (f x) (f₂ x) = 1 x
Tactic: filter_upwards [hf, hf₂] with x hx hx₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
inst_3 : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (f x) (f₂ x) = 1 x
have h : m (1 x) (f₂ x) = 1 x
Tactic: simp_rw [hx, hx₂, Pi.one_apply, hm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
inst_3 : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
h : m (1 x) (f₂ x) = 1 x
⊢ m (f x) (f₂ x) = 1 x
have h₁ : m (1 x) (1 x) = 1 x
Tactic: simp_rw [hx, hx₂, Pi.one_apply, hm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : TopologicalSpace β
K : Set β
h'f : HasCompactMulSupport f
hf : Continuous[inst, inst_2] f
hk : IsClosed[inst_2] K
h'k : 1 ∉ K
⊢ IsCompact (f ⁻¹' K)
have apply : ∀ (x : α) (hx : x ∈ f ⁻¹' K), x ∈ mulTSupport f
Tactic: apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : TopologicalSpace β
K : Set β
h'f : HasCompactMulSupport f
hf : Continuous[inst, inst_2] f
hk : IsClosed[inst_2] K
h'k : 1 ∉ K
x : α
hx : x ∈ f ⁻¹' K
⊢ x ∈ mulTSupport f
have a : x ∈ mulSupport f
Tactic: apply subset_mulTSupport
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α'
inst_1 : One β
inst_2 : T2Space α'
inst_3 : TopologicalSpace β
U : Set α'
hU : IsOpen[inst] U
f : (↑U : Type u_3) → β
cont : Continuous[instTopologicalSpaceSubtype, inst_3] f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend (Subtype.val (p := fun (x : α') ↦ x ∈ U)) f 1)
⊢ ContinuousAt (extend (Subtype.val (p := fun (x : α') ↦ x ∈ U)) f 1) x
have rw : ContinuousAt f (Subtype.mk (p := fun (x : α') ↦ x ∈ U) x sorry)
Tactic: rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _
      (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,
      ← (hU.isOpenEmbedding_subtypeVal).continuousAt_iff, extend_comp Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One γ
f : α → γ
inst_2 : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : Membership.mem (γ := Filter γ) (𝓝 1) N
⊢ N ∈ map f (cocompact α)
have rw : ∃ (t : Set α), IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
Tactic: rw [mem_map, mem_cocompact']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One γ
f : α → γ
inst_2 : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : Membership.mem (γ := Filter γ) (𝓝 1) N
⊢ ∃ (t : Set α), IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
have refine : (f ⁻¹' N)ᶜ ⊆ mulTSupport f
Tactic: refine ⟨mulTSupport f, h.isCompact, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One γ
f : α → γ
inst_2 : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : Membership.mem (γ := Filter γ) (𝓝 1) N
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f
have rw : (mulTSupport f)ᶜ ⊆ f ⁻¹' N
Tactic: rw [compl_subset_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One γ
f : α → γ
inst_2 : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : Membership.mem (γ := Filter γ) (𝓝 1) N
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N
have rw : 1 ∈ N
Tactic: rw [mem_preimage, image_eq_one_of_notMem_mulTSupport hv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : α → R
f' : α → M
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
have rw : ∀ (hf : f' =ᶠ[coclosedCompact α] 0), f • f' =ᶠ[coclosedCompact α] 0
Tactic: rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f • f') x = 0 x
have simp_rw : f x • f' x = 0 x
Tactic: simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
simp_rw : f x • f' x = 0 x
⊢ (f • f') x = 0 x
have simp_rw₁ : HSMul.hSMul (β := M) (f x) (0 x) = 0 x
Tactic: simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
simp_rw : f x • f' x = 0 x
simp_rw₁ : HSMul.hSMul (β := M) (f x) (0 x) = 0 x
⊢ (f • f') x = 0 x
have simp_rw₂ : HSMul.hSMul (β := M) (f x) 0 = 0
Tactic: simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
f : α → R
f' : α → M
hf : HasCompactSupport f
⊢ HasCompactSupport (f • f')
have rw : ∀ (hf : f =ᶠ[coclosedCompact α] 0), f • f' =ᶠ[coclosedCompact α] 0
Tactic: rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f • f') x = 0 x
have simp_rw : f x • f' x = 0 x
Tactic: simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
simp_rw : f x • f' x = 0 x
⊢ (f • f') x = 0 x
have simp_rw₁ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) (0 x) (f' x) = 0 x
Tactic: simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
M : Type u_7
R : Type u_8
inst : TopologicalSpace α
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
simp_rw : f x • f' x = 0 x
simp_rw₁ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) (0 x) (f' x) = 0 x
⊢ (f • f') x = 0 x
have simp_rw₂ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) 0 (f' x) = 0
Tactic: simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f
⊢ HasCompactSupport (f * f')
have rw : ∀ (hf : f =ᶠ[coclosedCompact α] 0), f * f' =ᶠ[coclosedCompact α] 0
Tactic: rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f * f') x = 0 x
have simp_rw : f x * f' x = 0 x
Tactic: simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
simp_rw : f x * f' x = 0 x
⊢ (f * f') x = 0 x
have simp_rw₁ : 0 x * f' x = 0 x
Tactic: simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
simp_rw : f x * f' x = 0 x
simp_rw₁ : 0 x * f' x = 0 x
⊢ (f * f') x = 0 x
have simp_rw₂ : 0 * f' x = 0
Tactic: simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f'
⊢ HasCompactSupport (f * f')
have rw : ∀ (hf : f' =ᶠ[coclosedCompact α] 0), f * f' =ᶠ[coclosedCompact α] 0
Tactic: rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f * f') x = 0 x
have simp_rw : f x * f' x = 0 x
Tactic: simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
simp_rw : f x * f' x = 0 x
⊢ (f * f') x = 0 x
have simp_rw₁ : f x * 0 x = 0 x
Tactic: simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
simp_rw : f x * f' x = 0 x
simp_rw₁ : f x * 0 x = 0 x
⊢ (f * f') x = 0 x
have simp_rw₂ : f x * 0 = 0
Tactic: simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
-- 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
⊢ ∃ (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 obtain : ∀ (n : Set X) (hn : n ∈ 𝓝 x)
  (hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}),
  ∃ (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 ι)
Tactic: obtain ⟨n, hn, hnf⟩ := hlf x
-- 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}
⊢ ∃ (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 : ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 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 => ?_⟩