awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x_1 x y : ↥(adjoin R {a})
hx :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
hy :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) y :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) y :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x * y) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x * y) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)

Tactic:
simp only [map_mul, hx, hy]

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x_1 x : ↥(adjoin R {a})
hx :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (star x) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (star x) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)

Tactic:
simp only [map_star, hx]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x : ↥(adjoin R {a})
⊢ ∀ (x : A) (h : Membership.mem (γ := Set A) {a} x),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) x ⋯) :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
      ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) x ⋯) :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)

Tactic:
exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by
    simp only [AlgHomClass.commutes], fun x y hx hy => by simp only [map_add, hx, hy],
    fun x y hx hy => by simp only [map_mul, hx, hy], fun x hx => by simp only [map_star, hx]]
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ mulSupport f ⊆ mulTSupport f

Tactic:
subset_closure

Premises used: subset_closure, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ IsClosed[inst_1] (mulTSupport f)

Tactic:
isClosed_closure

Premises used: mulTSupport, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
rw : closure[inst_1] (mulSupport f) = ∅ ↔ f = 1
rw₁ : mulSupport f = ∅ ↔ f = 1
rw₂ rw₃ : f = 1 ↔ f = 1
⊢ mulTSupport f = ∅ ↔ f = 1

Tactic:
rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]

Premises used: closure_empty_iff, Function.mulSupport_eq_empty_iff, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) fun (x : X) ↦ 1)) ∅
rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ∅) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ 1) ∅

Tactic:
rw [mulTSupport, mulSupport_fun_one, closure_empty]

Premises used: closure_empty, mulTSupport, Function.mulSupport_fun_one
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) 1)) ∅
rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ∅) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) 1) ∅

Tactic:
rw [mulTSupport, mulSupport_one, closure_empty]

Premises used: closure_empty, mulTSupport, Function.mulSupport_one
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_5
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
inst_3 : One γ
op : α → β → γ
op1 : op 1 1 = 1
f : X → α
g : X → β
⊢ (mulTSupport.{u_1, u_5} (α := γ) fun (x : X) ↦ op (f x) (g x)) ⊆ mulTSupport f ∪ mulTSupport g

Tactic:
closure_mono (mulSupport_binop_subset op op1 f g) |>.trans closure_union.subset

Premises used: HasSubset.Subset.trans, Function.mulSupport_binop_subset, closure_mono, closure_union, Eq.subset, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
hg : g 1 = 1
f : X → α
⊢ mulTSupport (g ∘ f) ⊆ mulTSupport f

Tactic:
closure_mono (mulSupport_comp_subset hg f)

Premises used: Function.mulSupport_comp_subset, closure_mono, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
hg : ∀ {x : α}, g x = 1 → x = 1
f : X → α
⊢ mulTSupport f ⊆ mulTSupport (g ∘ f)

Tactic:
closure_mono (mulSupport_subset_comp hg f)

Premises used: Function.mulSupport_subset_comp, closure_mono, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
rw₁ : closure[inst_1] (mulSupport (g ∘ f)) = closure[inst_1] (mulSupport f)
rw₂ rw₃ : closure[inst_1] (mulSupport f) = closure[inst_1] (mulSupport f)
⊢ mulTSupport (g ∘ f) = mulTSupport f

Tactic:
rw [mulTSupport, mulTSupport, mulSupport_comp_eq g hg]

Premises used: Function.mulSupport_comp_eq, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
rw₁ : closure[inst_1] (mulSupport (g ∘ f)) = closure[inst_1] (mulSupport f)
rw₂ rw₃ : closure[inst_1] (mulSupport f) = closure[inst_1] (mulSupport f)
⊢ mulTSupport (g ∘ f) = mulTSupport f

Tactic:
rw [mulTSupport, mulTSupport, mulSupport_comp_eq_of_range_subset hg]

Premises used: Function.mulSupport_comp_eq_of_range_subset, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst_1, inst_2] f
rw : closure[inst_1] (f ⁻¹' mulSupport g) ⊆ f ⁻¹' closure[inst_2] (mulSupport g)
⊢ mulTSupport (g ∘ f) ⊆ f ⁻¹' mulTSupport g

Tactic:
rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage]

Premises used: Function.mulSupport_comp_eq_preimage, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst_1, inst_2] f
⊢ closure[inst_1] (f ⁻¹' mulSupport g) ⊆ f ⁻¹' closure[inst_2] (mulSupport g)

Tactic:
hf.closure_preimage_subset _

Premises used: Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst_1, inst_2] f
⊢ closure[inst_1] (f ⁻¹' mulSupport g) ⊆ f ⁻¹' closure[inst_2] (mulSupport g)

Tactic:
exact hf.closure_preimage_subset _

Premises used: Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
rw :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
rw₁ :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
rw₂ :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
    ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
rw₃ rw₄ :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
    (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport (g ∘ (⇑f : (a : X) → Y))) ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)

Tactic:
rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage, Homeomorph.preimage_closure]

Premises used: Function.mulSupport_comp_eq_preimage, Homeomorph.preimage_closure, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
x : X
hx : x ∉ mulTSupport f
⊢ f x = 1

Tactic:
mulSupport_subset_iff'.mp (subset_mulTSupport f) x hx

Premises used: subset_mulTSupport, Function.mulSupport_subset_iff', Iff.mp
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
grw : range f ⊆ insert 1 (f '' mulSupport f)
⊢ range f ⊆ insert 1 (f '' mulTSupport f)

Tactic:
grw [← subset_mulTSupport f]

Premises used: subset_mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
range_subset_insert_image_mulSupport f

Premises used: Function.range_subset_insert_image_mulSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
exact range_subset_insert_image_mulSupport f

Premises used: Function.range_subset_insert_image_mulSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ range f = f '' mulTSupport f ∨ range f = insert 1 (f '' mulTSupport f)

Tactic:
(wcovBy_insert _ _).eq_or_eq (image_subset_range _ _) (range_subset_insert_image_mulTSupport f)

Premises used: WCovBy.eq_or_eq, range_subset_insert_image_mulTSupport, Set.image_subset_range, Set.wcovBy_insert
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_9
inst_1 : MulZeroClass α
f g : X → α
⊢ (tsupport.{u_1, u_9} (α := α) fun (x : X) ↦ f x * g x) ⊆ tsupport f

Tactic:
closure_mono (support_mul_subset_left _ _)

Premises used: tsupport, closure_mono, Function.support_mul_subset_left
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_9
inst_1 : MulZeroClass α
f g : X → α
⊢ (tsupport.{u_1, u_9} (α := α) fun (x : X) ↦ f x * g x) ⊆ tsupport g

Tactic:
closure_mono (support_mul_subset_right _ _)

Premises used: Function.support_mul_subset_right, tsupport, closure_mono
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : MulOneClass α
f g : X → α
⊢ Eq.{u_2 + 1} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) 1 1) 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : Monoid α
f : X → α
n : ℕ
⊢ (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ f x ^ n) ⊆ mulTSupport f

Tactic:
closure_mono <| mulSupport_pow f n

Premises used: Function.mulSupport_pow, closure_mono, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : DivisionMonoid α
f : X → α
⊢ (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ (f x)⁻¹) = mulTSupport f

Tactic:
congrArg closure <| mulSupport_fun_inv f

Premises used: congrArg, closure, Function.mulSupport_fun_inv, mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : DivisionMonoid α
f : X → α
⊢ mulTSupport f⁻¹ = mulTSupport f

Tactic:
mulTSupport_fun_inv f

Premises used: mulTSupport_fun_inv
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : DivisionMonoid α
f g : X → α
⊢ Eq.{u_2 + 1} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2⁻¹) 1 1) 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : DivisionMonoid α
f g : X → α
⊢ (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ f x / g x) ⊆ mulTSupport f ∪ mulTSupport g

Tactic:
mulTSupport_binop_subset (· / ·) one_div_one f g

Premises used: mulTSupport_binop_subset, HDiv.hDiv, one_div_one
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
M : Type u_9
α : Type u_10
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMulWithZero M α
f : X → M
g : X → α
⊢ (tsupport.{u_1, u_10} (α := α) fun (x : X) ↦ f x • g x) ⊆ tsupport f

Tactic:
closure_mono <| support_smul_subset_left f g

Premises used: Function.support_smul_subset_left, tsupport, closure_mono
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
M : Type u_9
α : Type u_10
inst_1 : Zero α
inst_2 : SMulZeroClass M α
f : X → M
g : X → α
⊢ (tsupport.{u_1, u_10} (α := α) fun (x : X) ↦ f x • g x) ⊆ tsupport g

Tactic:
closure_mono <| support_smul_subset_right f g

Premises used: Function.support_smul_subset_right, tsupport, closure_mono
-- Module: Mathlib.Topology.Algebra.Support
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
simp_rw₆ : (∃ x_1 ∈ 𝓝 x, EqOn f 1 x_1) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport 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]

Premises used: mem_closure_iff_nhds, Set.not_nonempty_iff_eq_empty, exists_prop, Function.disjoint_mulSupport_iff, Set.disjoint_iff_inter_eq_empty, Filter.eventuallyEq_iff_exists_mem, mulTSupport, Classical.not_forall
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
hf : ∀ x ∈ mulTSupport f, ContinuousAt f x
⊢ Continuous[inst, inst_2] f

Tactic:
continuous_iff_continuousAt.2 fun x => (em _).elim (hf x) fun hx =>
    (@continuousAt_const _ _ _ _ _ 1).congr (notMem_mulTSupport_iff_eventuallyEq.mp hx).symm

Premises used: Iff.mpr, Membership.mem, em, ContinuousAt.congr, continuousAt_const, Iff.mp, Or.elim, mulTSupport, notMem_mulTSupport_iff_eventuallyEq, Filter.EventuallyEq.symm, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
s : Set α
hs : ContinuousOn f s
h's : IsOpen[inst] s
h''s : mulTSupport f ⊆ s
⊢ Continuous[inst, inst_2] f

Tactic:
continuous_of_mulTSupport fun _ hx ↦ h's.continuousOn_iff.mp hs <| h''s hx

Premises used: IsOpen.continuousOn_iff, Iff.mp, continuous_of_mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
⊢ HasCompactMulSupport f ↔ IsCompact (closure[inst] (mulSupport f))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Support
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
simp_rw₄ : (∃ (K : Set α), IsCompact K ∧ mulSupport f ⊆ K) ↔ IsCompact (closure[inst] (mulSupport f))
⊢ (∃ (K : Set α), IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f

Tactic:
simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
    hasCompactMulSupport_def, exists_isCompact_superset_iff]

Premises used: Set.subset_def, hasCompactMulSupport_def, Set.compl_subset_compl, exists_isCompact_superset_iff, Function.notMem_mulSupport, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
inst_2 : R1Space α
hK : IsCompact K
hfK : ∀ x ∉ K, f x = 1
⊢ HasCompactMulSupport f

Tactic:
exists_compact_iff_hasCompactMulSupport.mp ⟨K, hK, hfK⟩

Premises used: And.intro, Exists.intro, Iff.mp, exists_compact_iff_hasCompactMulSupport
-- Module: Mathlib.Topology.Algebra.Support
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
rw : mulTSupport f ⊆ closure[inst] K
⊢ mulTSupport f ⊆ K

Tactic:
rw [← h'K.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Algebra.Support
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 ⊆ closure[inst] K

Tactic:
apply closure_mono (mulSupport_subset_iff'.2 hfK)

Premises used: Iff.mpr, Function.mulSupport_subset_iff', closure_mono
-- Module: Mathlib.Topology.Algebra.Support
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

Tactic:
have : mulTSupport f ⊆ K := by
    rw [← h'K.closure_eq]
    apply closure_mono (mulSupport_subset_iff'.2 hfK)
-- Module: Mathlib.Topology.Algebra.Support
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
this : mulTSupport f ⊆ K
⊢ HasCompactMulSupport f

Tactic:
IsCompact.of_isClosed_subset hK (isClosed_mulTSupport f) this

Premises used: HasCompactMulSupport, isClosed_mulTSupport, IsCompact.of_isClosed_subset
-- Module: Mathlib.Topology.Algebra.Support
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
this : mulTSupport f ⊆ K
⊢ HasCompactMulSupport f

Tactic:
exact IsCompact.of_isClosed_subset hK (isClosed_mulTSupport f) this

Premises used: isClosed_mulTSupport, IsCompact.of_isClosed_subset
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
K : Set α
inst_2 : R1Space α
hK : IsCompact K
h : mulSupport f ⊆ K
⊢ HasCompactMulSupport f

Tactic:
hK.closure_of_subset h

Premises used: HasCompactMulSupport, mulTSupport, IsCompact.closure_of_subset
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
hf : HasCompactMulSupport f
⊢ IsCompact (mulTSupport f)

Tactic:
hf

Premises used: HasCompactMulSupport