awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
⊢ HasCompactMulSupport f ↔ f =ᶠ[coclosedCompact α] 1

Tactic:
mem_coclosedCompact_iff.symm

Premises used: Set.Mem, Filter.Eventually, Filter.mem_coclosedCompact_iff, setOf, HasCompactMulSupport, Filter.EventuallyEq, Function.mulSupport, mulTSupport, Iff.symm
-- Module: Mathlib.Topology.Algebra.Support
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)
inr : ∀ (h2 : range f = insert 1 (f '' K)), IsCompact (range f)
⊢ IsCompact (range f)

Tactic:
rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2

Premises used: Function.range_eq_image_or_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.Support
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
inl : IsCompact (f '' K)
⊢ IsCompact (range f)

Tactic:
rw [h2]
-- Module: Mathlib.Topology.Algebra.Support
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)
inr : IsCompact (insert 1 (f '' K))
⊢ IsCompact (range f)

Tactic:
rw [h2]
-- Module: Mathlib.Topology.Algebra.Support
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 (f '' K)

Tactic:
hk.image hf

Premises used: IsCompact.image
-- Module: Mathlib.Topology.Algebra.Support
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 (insert 1 (f '' K))

Tactic:
(hk.image hf).insert 1

Premises used: IsCompact.insert, OfNat.ofNat, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Support
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 (f '' K)

Tactic:
exacts [hk.image hf, (hk.image hf).insert 1]

Premises used: IsCompact.insert, OfNat.ofNat, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
inst_2 : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous[inst, inst_2] f
⊢ IsCompact (range f)

Tactic:
isCompact_range_of_mulSupport_subset_isCompact hf h (subset_mulTSupport f)

Premises used: subset_mulTSupport, isCompact_range_of_mulSupport_subset_isCompact
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
f : α → β
f' : α → γ
hf : HasCompactMulSupport f
hff' : mulSupport f' ⊆ mulTSupport f
⊢ HasCompactMulSupport f'

Tactic:
IsCompact.of_isClosed_subset hf isClosed_closure <| closure_minimal hff' isClosed_closure

Premises used: closure_minimal, HasCompactMulSupport, IsCompact.of_isClosed_subset, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
f : α → β
f' : α → γ
hf : HasCompactMulSupport f
hff' : mulSupport f' ⊆ mulSupport f
⊢ HasCompactMulSupport f'

Tactic:
hf.mono' <| hff'.trans subset_closure

Premises used: subset_closure, HasSubset.Subset.trans, HasCompactMulSupport.mono'
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One β
inst_2 : One γ
g : β → γ
f : α → β
hf : HasCompactMulSupport f
hg : g 1 = 1
⊢ HasCompactMulSupport (g ∘ f)

Tactic:
hf.mono <| mulSupport_comp_subset hg f

Premises used: Function.mulSupport_comp_subset, HasCompactMulSupport.mono
-- Module: Mathlib.Topology.Algebra.Support
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
rw : IsCompact (closure[inst_1] (g ⁻¹' mulSupport f))
⊢ HasCompactMulSupport (f ∘ g)

Tactic:
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]

Premises used: hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage
-- Module: Mathlib.Topology.Algebra.Support
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))

Tactic:
IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_

Premises used: IsCompact.of_isClosed_subset, Topology.IsClosedEmbedding.isCompact_preimage, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Support
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
refine : closure[inst_1] (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
⊢ IsCompact (closure[inst_1] (g ⁻¹' mulSupport f))

Tactic:
refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_

Premises used: IsCompact.of_isClosed_subset, Topology.IsClosedEmbedding.isCompact_preimage, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Support
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
rw : g ⁻¹' closure[inst] (g '' g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
⊢ closure[inst_1] (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f

Tactic:
rw [hg.isEmbedding.closure_eq_preimage_closure_image]

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.Algebra.Support
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
⊢ g ⁻¹' closure[inst] (g '' g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f

Tactic:
preimage_mono (closure_mono <| image_preimage_subset _ _)

Premises used: closure_mono, Set.preimage_mono, Set.image_preimage_subset
-- Module: Mathlib.Topology.Algebra.Support
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
⊢ g ⁻¹' closure[inst] (g '' g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f

Tactic:
exact preimage_mono (closure_mono <| image_preimage_subset _ _)

Premises used: closure_mono, Set.preimage_mono, Set.image_preimage_subset
-- Module: Mathlib.Topology.Algebra.Support
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
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
⊢ HasCompactMulSupport.{u_2, u_6} (β := δ) fun (x : α) ↦ m (f x) (f₂ x)

Tactic:
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢

Premises used: hasCompactMulSupport_iff_eventuallyEq
-- Module: Mathlib.Topology.Algebra.Support
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
h : ∀ (x : α) (hx : f x = 1 x) (hx₂ : f₂ x = 1 x), m (f x) (f₂ x) = 1 x
⊢ EventuallyEq.{u_2, u_6} (β := δ) (coclosedCompact α) (fun (x : α) ↦ m (f x) (f₂ x)) 1

Tactic:
filter_upwards [hf, hf₂] with x hx hx₂
-- Module: Mathlib.Topology.Algebra.Support
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
h₁ : m (1 x) (1 x) = 1 x
h₂ : m 1 1 = 1
⊢ m (f x) (f₂ x) = 1 x

Tactic:
simp_rw [hx, hx₂, Pi.one_apply, hm]

Premises used: Pi.one_apply
-- Module: Mathlib.Topology.Algebra.Support
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
apply : ∀ (x : α) (hx : x ∈ f ⁻¹' K), x ∈ mulTSupport f
⊢ IsCompact (f ⁻¹' K)

Tactic:
apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)

Premises used: IsCompact.of_isClosed_subset, IsClosed.preimage
-- Module: Mathlib.Topology.Algebra.Support
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
a : x ∈ mulSupport f
⊢ x ∈ mulTSupport f

Tactic:
apply subset_mulTSupport

Premises used: subset_mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
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 ∈ mulSupport f

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace α'
inst_2 : One β
f : α → β
inst_3 : T2Space α'
hf : HasCompactMulSupport f
g : α → α'
cont : Continuous[inst, inst_1] g
⊢ mulTSupport (extend g f 1) ⊆ g '' mulTSupport f

Tactic:
(hf.image cont).isClosed.closure_subset_iff.mpr <|
    mulSupport_extend_one_subset.trans (image_mono subset_closure)

Premises used: Iff.mpr, subset_closure, Set.image_mono, HasSubset.Subset.trans, Function.mulSupport_extend_one_subset, IsClosed.closure_subset_iff, mulTSupport, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace α'
inst_2 : One β
f : α → β
inst_3 : T2Space α'
hf : HasCompactMulSupport f
g : α → α'
cont : Continuous[inst, inst_1] g
⊢ HasCompactMulSupport (extend g f 1)

Tactic:
HasCompactMulSupport.of_mulSupport_subset_isCompact (hf.image cont)
    (subset_closure.trans <| hf.mulTSupport_extend_one_subset cont)

Premises used: HasCompactMulSupport.mulTSupport_extend_one_subset, subset_closure, HasCompactMulSupport.of_mulSupport_subset_isCompact, HasSubset.Subset.trans, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
α' : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace α'
inst_2 : One β
f : α → β
inst_3 : T2Space α'
hf : HasCompactMulSupport f
g : α → α'
cont : Continuous[inst, inst_1] g
inj : Injective g
⊢ mulTSupport (extend g f 1) = g '' mulTSupport f

Tactic:
(hf.mulTSupport_extend_one_subset cont).antisymm <|
    (image_closure_subset_closure_image cont).trans
      (closure_mono (mulSupport_extend_one inj).superset)

Premises used: HasCompactMulSupport.mulTSupport_extend_one_subset, HasSubset.Subset.trans, closure_mono, HasSubset.Subset.antisymm, image_closure_subset_closure_image, Function.mulSupport_extend_one, Eq.superset
-- Module: Mathlib.Topology.Algebra.Support
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)
⊢ x = (↑(Subtype.mk (p := fun (x : α') ↦ x ∈ U) x ⋯) : α')

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Support
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)
rw : ContinuousAt f (Subtype.mk (p := fun (x : α') ↦ x ∈ U) x ⋯)
⊢ ContinuousAt (extend (Subtype.val (p := fun (x : α') ↦ x ∈ U)) f 1) x

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]

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Subtype.val_injective, Topology.IsOpenEmbedding.continuousAt_iff, Function.extend_comp
-- Module: Mathlib.Topology.Algebra.Support
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 f (Subtype.mk (p := fun (x : α') ↦ x ∈ U) x ⋯)

Tactic:
cont.continuousAt

Premises used: Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Support
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 f (Subtype.mk (p := fun (x : α') ↦ x ∈ U) x ⋯)

Tactic:
exact cont.continuousAt

Premises used: Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Support
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
rw : ∃ (t : Set α), IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
⊢ N ∈ map f (cocompact α)

Tactic:
rw [mem_map, mem_cocompact']

Premises used: Filter.mem_map, Filter.mem_cocompact'
-- Module: Mathlib.Topology.Algebra.Support
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

Tactic:
⟨mulTSupport f, h.isCompact, ?_⟩

Premises used: HasCompactMulSupport.isCompact, And.intro, Exists.intro, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
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
refine : (f ⁻¹' N)ᶜ ⊆ mulTSupport f
⊢ ∃ (t : Set α), IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t

Tactic:
refine ⟨mulTSupport f, h.isCompact, ?_⟩
-- Module: Mathlib.Topology.Algebra.Support
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
rw : (mulTSupport f)ᶜ ⊆ f ⁻¹' N
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f

Tactic:
rw [compl_subset_comm]

Premises used: Set.compl_subset_comm
-- Module: Mathlib.Topology.Algebra.Support
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)ᶜ
rw : 1 ∈ N
⊢ v ∈ f ⁻¹' N

Tactic:
rw [mem_preimage, image_eq_one_of_notMem_mulTSupport hv]

Premises used: image_eq_one_of_notMem_mulTSupport, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Support
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)ᶜ
⊢ 1 ∈ N

Tactic:
mem_of_mem_nhds hN

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Support
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)ᶜ
⊢ 1 ∈ N

Tactic:
exact mem_of_mem_nhds hN

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
γ : Type u_5
inst : TopologicalSpace α
inst_1 : One γ
inst_2 : CompactSpace α
f : α → γ
⊢ HasCompactMulSupport f

Tactic:
IsCompact.of_isClosed_subset isCompact_univ (isClosed_mulTSupport f)
    (Set.subset_univ (mulTSupport f))

Premises used: Set.subset_univ, HasCompactMulSupport, isClosed_mulTSupport, IsCompact.of_isClosed_subset, isCompact_univ, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulOneClass β
f f' : α → β
hf : HasCompactMulSupport f
hf' : HasCompactMulSupport f'
⊢ HasCompactMulSupport (f * f')

Tactic:
hf.comp₂_left hf' (mul_one 1)

Premises used: HasCompactMulSupport.comp₂_left, mul_one, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_9
β : Type u_10
inst : TopologicalSpace α
inst_1 : One β
⊢ HasCompactMulSupport.{u_9, u_10} (α := α) (β := β) 1

Tactic:
simp [HasCompactMulSupport]

Premises used: HasCompactMulSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulOneClass β
f : α → β
⊢ Membership.mem (γ := Submonoid (α → β)) (submonoid α β) f ↔ HasCompactMulSupport f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, HasCompactMulSupport, IsCompact
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_9
β : Type u_10
inst : TopologicalSpace α
inst_1 : Monoid β
l : List (α → β)
hl : ∀ f ∈ l, HasCompactMulSupport f
⊢ HasCompactMulSupport l.prod

Tactic:
list_prod_mem (S := HasCompactMulSupport.submonoid α β) hl

Premises used: list_prod_mem, Set.Mem, setOf, HasCompactMulSupport, IsCompact
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : CommMonoid β
m : Multiset (α → β)
hm : ∀ f ∈ m, HasCompactMulSupport f
⊢ HasCompactMulSupport m.prod

Tactic:
multiset_prod_mem (S := HasCompactMulSupport.submonoid α β) m hm

Premises used: Set.Mem, multiset_prod_mem, setOf, HasCompactMulSupport, IsCompact
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : CommMonoid β
ι : Type u_9
s : Finset ι
f : ι → α → β
hf : ∀ i ∈ s, HasCompactMulSupport (f i)
⊢ HasCompactMulSupport.{u_2, u_4} (α := α) (β := β) (∏ i ∈ s, f i)

Tactic:
prod_mem (S := HasCompactMulSupport.submonoid α β) hf

Premises used: Set.Mem, setOf, HasCompactMulSupport, IsCompact, prod_mem
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_9
β : Type u_10
inst : TopologicalSpace α
inst_1 : DivisionMonoid β
f : α → β
hf : HasCompactMulSupport f
⊢ HasCompactMulSupport f⁻¹

Tactic:
simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv] using hf

Premises used: Function.mulSupport_inv, HasCompactMulSupport, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_9
β : Type u_10
inst : TopologicalSpace α
inst_1 : DivisionMonoid β
f f' : α → β
hf : HasCompactMulSupport f
hf' : HasCompactMulSupport f'
⊢ HasCompactMulSupport (f / f')

Tactic:
div_eq_mul_inv f f' ▸ hf.mul hf'.inv

Premises used: Eq.rec, HasCompactMulSupport.inv, HasCompactMulSupport.mul, div_eq_mul_inv, Eq.symm
-- Module: Mathlib.Topology.Algebra.Support
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'
rw : ∀ (hf : f' =ᶠ[coclosedCompact α] 0), f • f' =ᶠ[coclosedCompact α] 0
⊢ HasCompactSupport (f • f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Premises used: hasCompactSupport_iff_eventuallyEq
-- Module: Mathlib.Topology.Algebra.Support
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
simp_rw₂ : HSMul.hSMul (β := M) (f x) 0 = 0
⊢ (f • f') x = 0 x

Tactic:
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]

Premises used: Pi.smul_apply', smul_zero, Pi.zero_apply
-- Module: Mathlib.Topology.Algebra.Support
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
⊢ f • f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Algebra.Support
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
rw : ∀ (hf : f =ᶠ[coclosedCompact α] 0), f • f' =ᶠ[coclosedCompact α] 0
⊢ HasCompactSupport (f • f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Premises used: hasCompactSupport_iff_eventuallyEq
-- Module: Mathlib.Topology.Algebra.Support
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
simp_rw₂ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) 0 (f' x) = 0
⊢ (f • f') x = 0 x

Tactic:
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Premises used: Pi.smul_apply', Pi.zero_apply, zero_smul
-- Module: Mathlib.Topology.Algebra.Support
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
⊢ f • f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f
rw : ∀ (hf : f =ᶠ[coclosedCompact α] 0), f * f' =ᶠ[coclosedCompact α] 0
⊢ HasCompactSupport (f * f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Premises used: hasCompactSupport_iff_eventuallyEq
-- Module: Mathlib.Topology.Algebra.Support
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
simp_rw₂ : 0 * f' x = 0
⊢ (f * f') x = 0 x

Tactic:
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]

Premises used: Pi.mul_apply, MulZeroClass.zero_mul, Pi.zero_apply
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f'
rw : ∀ (hf : f' =ᶠ[coclosedCompact α] 0), f * f' =ᶠ[coclosedCompact α] 0
⊢ HasCompactSupport (f * f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Premises used: hasCompactSupport_iff_eventuallyEq