awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ Eq.{u_2 + 1} (α := (a : α) → α) (⇑(Homeomorph.symm (Homeomorph.smulOfNeZero c hc)) : (a : α) → α) fun (x : α) ↦
    c⁻¹ • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ IsHomeomorph (Y := α) fun (x : α) ↦ c • x

Tactic:
(Homeomorph.smulOfNeZero c hc).isHomeomorph

Premises used: Homeomorph.isHomeomorph, Homeomorph.smulOfNeZero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ IsOpenMap (Y := α) fun (x : α) ↦ c • x

Tactic:
(Homeomorph.smulOfNeZero c hc).isOpenMap

Premises used: Homeomorph.smulOfNeZero, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
s : Set α
hs : IsOpen[inst] s
hc : c ≠ 0
⊢ IsOpen[inst] (c • s)

Tactic:
isOpenMap_smul₀ hc s hs

Premises used: isOpenMap_smul₀
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
s : Set α
⊢ closure[inst] (c • s) = c • closure[inst] s

Tactic:
((Homeomorph.smulOfNeZero c hc).image_closure s).symm

Premises used: Homeomorph.image_closure, Homeomorph.smulOfNeZero, Eq.symm
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
s : Set E
inl :
  closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
inr : ∀ (hc : c ≠ 0), closure[inst_3] (c • s) = c • closure[inst_3] s
⊢ closure[inst_3] (c • s) = c • closure[inst_3] s

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
inl :
  closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 ∅) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 (closure[inst_3] ∅)
inl₁ :
  ∀ (hs : s.Nonempty),
    closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
      HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)
⊢ closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
⊢ closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 ∅) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := Set E) 0 (closure[inst_3] ∅)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
inl : Eq.{u_5 + 1} (α := Set E) (closure[inst_3] 0) 0
⊢ closure[inst_3] (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 s) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 (closure[inst_3] s)

Tactic:
rw [zero_smul_set hs, zero_smul_set hs.closure]

Premises used: Set.zero_smul_set, Set.Nonempty.closure
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ Eq.{u_5 + 1} (α := Set E) (closure[inst_3] 0) 0

Tactic:
closure_singleton

Premises used: closure_singleton
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ Eq.{u_5 + 1} (α := Set E) (closure[inst_3] 0) 0

Tactic:
exact closure_singleton

Premises used: closure_singleton
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure[inst_3] (c • s) = c • closure[inst_3] s

Tactic:
closure_smul₀' hc s

Premises used: closure_smul₀'
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure[inst_3] (c • s) = c • closure[inst_3] s

Tactic:
exact closure_smul₀' hc s

Premises used: closure_smul₀'
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
x : α
⊢ 𝓝 (c • x) = c • 𝓝 x

Tactic:
nhds_smul (Units.mk0 c hc) x

Premises used: Units.mk0, nhds_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
x : α
⊢ 𝓝[≠] (c • x) = c • 𝓝[≠] x

Tactic:
punctured_nhds_smul (Units.mk0 c hc) x

Premises used: punctured_nhds_smul, Set.Mem, setOf, Units.mk0
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ IsClosedMap (Y := α) fun (x : α) ↦ c • x

Tactic:
(Homeomorph.smulOfNeZero c hc).isClosedMap

Premises used: Homeomorph.isClosedMap, Homeomorph.smulOfNeZero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
c : G₀
s : Set α
hs : IsClosed[inst] s
hc : c ≠ 0
⊢ IsClosed[inst] (c • s)

Tactic:
isClosedMap_smul_of_ne_zero hc s hs

Premises used: isClosedMap_smul_of_ne_zero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
inl : IsClosedMap (Y := E) fun (x : E) ↦ HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x
inr : ∀ (hne : c ≠ 0), IsClosedMap (Y := E) fun (x : E) ↦ c • x
⊢ IsClosedMap (Y := E) fun (x : E) ↦ c • x

Tactic:
rcases eq_or_ne c 0 with (rfl | hne)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
inl : IsClosedMap (Y := E) fun (x : E) ↦ 0
⊢ IsClosedMap (Y := E) fun (x : E) ↦ HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x

Tactic:
simp only [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
⊢ IsClosedMap (Y := E) fun (x : E) ↦ 0

Tactic:
isClosedMap_const

Premises used: isClosedMap_const
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
⊢ IsClosedMap (Y := E) fun (x : E) ↦ 0

Tactic:
exact isClosedMap_const

Premises used: isClosedMap_const
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
hne : c ≠ 0
⊢ IsClosedMap (Y := E) fun (x : E) ↦ c • x

Tactic:
(Homeomorph.smulOfNeZero c hne).isClosedMap

Premises used: Homeomorph.isClosedMap, Homeomorph.smulOfNeZero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
hne : c ≠ 0
⊢ IsClosedMap (Y := E) fun (x : E) ↦ c • x

Tactic:
exact (Homeomorph.smulOfNeZero c hne).isClosedMap

Premises used: Homeomorph.isClosedMap, Homeomorph.smulOfNeZero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G₀ : Type u_4
inst : GroupWithZero G₀
E : Type u_5
inst_1 : Zero E
inst_2 : MulActionWithZero G₀ E
inst_3 : TopologicalSpace E
inst_4 : T1Space E
inst_5 : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hs : IsClosed[inst_3] s
⊢ IsClosed[inst_3] (c • s)

Tactic:
isClosedMap_smul₀ c s hs

Premises used: isClosedMap_smul₀
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
β : Type u_5
inst_4 : One β
f : α → β
h : HasCompactMulSupport f
c : G₀
hc : c ≠ 0
⊢ HasCompactMulSupport.{u_2, u_5} (β := β) fun (x : α) ↦ f (c • x)

Tactic:
h.comp_homeomorph (Homeomorph.smulOfNeZero c hc)

Premises used: HasCompactMulSupport.comp_homeomorph, Homeomorph.smulOfNeZero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
β : Type u_5
inst_4 : Zero β
f : α → β
h : HasCompactSupport f
c : G₀
hc : c ≠ 0
⊢ HasCompactSupport.{u_2, u_5} (β := β) fun (x : α) ↦ f (c • x)

Tactic:
h.comp_homeomorph (Homeomorph.smulOfNeZero c hc)

Premises used: HasCompactSupport.comp_homeomorph, Homeomorph.smulOfNeZero
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
f : β → α
l : Filter β
a : α
c : M
hc : IsUnit c
⊢ Tendsto (fun (x : β) ↦ c • f x) l (𝓝 (c • a)) ↔ Tendsto f l (𝓝 a)

Tactic:
tendsto_const_smul_iff hc.unit

Premises used: tendsto_const_smul_iff, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
inst_4 : TopologicalSpace β
f : β → α
b : β
c : M
s : Set β
hc : IsUnit c
⊢ ContinuousWithinAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) s b ↔ ContinuousWithinAt f s b

Tactic:
continuousWithinAt_const_smul_iff hc.unit

Premises used: continuousWithinAt_const_smul_iff, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
inst_4 : TopologicalSpace β
f : β → α
c : M
s : Set β
hc : IsUnit c
⊢ ContinuousOn.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) s ↔ ContinuousOn f s

Tactic:
continuousOn_const_smul_iff hc.unit

Premises used: continuousOn_const_smul_iff, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
inst_4 : TopologicalSpace β
f : β → α
b : β
c : M
hc : IsUnit c
⊢ ContinuousAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) b ↔ ContinuousAt f b

Tactic:
continuousAt_const_smul_iff hc.unit

Premises used: IsUnit.unit, continuousAt_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
inst_4 : TopologicalSpace β
f : β → α
c : M
hc : IsUnit c
⊢ (Continuous[inst_4, inst_1] fun (x : β) ↦ c • f x) ↔ Continuous[inst_4, inst_1] f

Tactic:
continuous_const_smul_iff hc.unit

Premises used: IsUnit.unit, continuous_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
c : M
hc : IsUnit c
⊢ IsHomeomorph (Y := α) fun (x : α) ↦ c • x

Tactic:
isHomeomorph_smul hc.unit

Premises used: isHomeomorph_smul, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
c : M
hc : IsUnit c
⊢ IsOpenMap (Y := α) fun (x : α) ↦ c • x

Tactic:
isOpenMap_smul hc.unit

Premises used: isOpenMap_smul, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
c : M
hc : IsUnit c
⊢ IsClosedMap (Y := α) fun (x : α) ↦ c • x

Tactic:
isClosedMap_smul hc.unit

Premises used: isClosedMap_smul, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
c : M
hc : IsUnit c
s : Set α
a : α
⊢ c • s ∈ 𝓝 (c • a) ↔ s ∈ 𝓝 a

Tactic:
smul_mem_nhds_smul_iff hc.unit

Premises used: Set.Mem, smul_mem_nhds_smul_iff, IsUnit.unit
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst_4 : SMul S M
inst_5 : SMul S α
inst_6 : IsScalarTower S M α
inst_7 : SMul S β
f : MulActionHom.{u_4, u_4, u_2, u_5} (M := S) id α β
inst_8 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
c : S
hc : IsUnit (HSMul.hSMul (β := M) c 1)
⊢ IsQuotientMap.{u_2, u_5} (X := α) (Y := β)
    (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x)

Tactic:
hf.comp hc.isHomeomorph_smul.isQuotientMap

Premises used: IsHomeomorph.isQuotientMap, Topology.IsQuotientMap.comp, IsUnit.isHomeomorph_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst_4 : SMul S M
inst_5 : SMul S α
inst_6 : IsScalarTower S M α
inst_7 : SMul S β
f : MulActionHom.{u_4, u_4, u_2, u_5} (M := S) id α β
inst_8 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
c : S
hc : IsUnit (HSMul.hSMul (β := M) c 1)
h :
  Eq (α := α → β) ((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β))
    (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x)
⊢ IsQuotientMap.{u_2, u_5} (X := α) (Y := β) ((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β))

Tactic:
convert! hf.comp hc.isHomeomorph_smul.isQuotientMap

Premises used: IsHomeomorph.isQuotientMap, Topology.IsQuotientMap.comp, IsUnit.isHomeomorph_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst_4 : SMul S M
inst_5 : SMul S α
inst_6 : IsScalarTower S M α
inst_7 : SMul S β
f : MulActionHom.{u_4, u_4, u_2, u_5} (M := S) id α β
inst_8 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
c : S
hc : IsUnit (HSMul.hSMul (β := M) c 1)
h :
  ∀ (x : α),
    Eq.{u_5 + 1} (α := β) (((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β)) x)
      (Function.comp (β := α) (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x) x)
⊢ Eq (α := α → β) ((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β))
    (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst_4 : SMul S M
inst_5 : SMul S α
inst_6 : IsScalarTower S M α
inst_7 : SMul S β
f : MulActionHom.{u_4, u_4, u_2, u_5} (M := S) id α β
inst_8 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
c : S
hc : IsUnit (HSMul.hSMul (β := M) c 1)
x : α
⊢ Eq.{u_5 + 1} (α := β) (((fun (x : β) ↦ c • x) ∘ (⇑f : (a : α) → β)) x)
    (Function.comp (β := α) (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul (β := M) c 1 • x) x)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
inst : TopologicalSpace α
M : Type u_4
β : Type u_5
inst_1 : Semiring M
inst_2 : AddCommMonoid α
inst_3 : Module M α
inst_4 : ContinuousConstSMul M α
inst_5 : AddMonoid β
f : α →+ β
inst_6 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
n : ℕ
hc rwa rwa₁ rwa₂ rwa₃ : IsUnit.{u_4} (M := M) (↑n : M)
⊢ IsUnit (HSMul.hSMul (β := M) n 1)

Tactic:
rwa [nsmul_one]

Premises used: nsmul_one
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
inst : TopologicalSpace α
M : Type u_4
β : Type u_5
inst_1 : Ring M
inst_2 : AddCommGroup α
inst_3 : Module M α
inst_4 : ContinuousConstSMul M α
inst_5 : AddGroup β
f : α →+ β
inst_6 : TopologicalSpace β
hf : IsQuotientMap.{u_2, u_5} (X := α) (Y := β) (⇑f : (a : α) → β)
n : ℤ
hc rwa rwa₁ rwa₂ rwa₃ : IsUnit.{u_4} (M := M) (↑n : M)
⊢ IsUnit (HSMul.hSMul (β := M) n 1)

Tactic:
rwa [zsmul_one n]

Premises used: zsmul_one
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
⊢ ProperlyDiscontinuousSMul M α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := M) {m : M | (m • K ∩ L).Nonempty}

Tactic:
⟨fun _ _ _ ↦ ProperlyDiscontinuousSMul.finite_disjoint_inter_image, .mk⟩

Premises used: ProperlyDiscontinuousSMul.mk, Iff.intro, ProperlyDiscontinuousSMul.finite_disjoint_inter_image
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
x : T
simp_rw : Set.Finite.{u_4} (α := Γ) {γ : Γ | (image (α := T) (HSMul.hSMul γ) {x} ∩ {x}).Nonempty}
⊢ Set.Finite.{u_4} (α := Γ) {γ : Γ | γ • x = x}

Tactic:
simp_rw [← mem_singleton_iff, ← singleton_inter_nonempty, ← image_singleton]

Premises used: Set.image_singleton, Set.mem_singleton_iff, Set.singleton_inter_nonempty
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
x : T
⊢ Set.Finite.{u_4} (α := Γ) {γ : Γ | (image (α := T) (HSMul.hSMul γ) {x} ∩ {x}).Nonempty}

Tactic:
finite_disjoint_inter_image isCompact_singleton isCompact_singleton

Premises used: setOf, isCompact_singleton, ProperlyDiscontinuousSMul.finite_disjoint_inter_image
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
x : T
⊢ Set.Finite.{u_4} (α := Γ) {γ : Γ | (image (α := T) (HSMul.hSMul γ) {x} ∩ {x}).Nonempty}

Tactic:
exact finite_disjoint_inter_image isCompact_singleton isCompact_singleton

Premises used: isCompact_singleton, ProperlyDiscontinuousSMul.finite_disjoint_inter_image
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
obtain :
  ∀ (V : Set T) (V_cpt : IsCompact V) (V_nhd : V ∈ 𝓝 x),
    ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x

Tactic:
obtain ⟨V, V_cpt, V_nhd⟩ := exists_compact_mem_nhds x

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
⊢ Finite.{u_4 + 1} (↑Γ₀ : Type u_4)

Tactic:
have : Finite Γ₀ := (finite_disjoint_inter_image V_cpt V_cpt).subset fun _ ↦ And.left
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
choose :
  ∀ (u v : (γ : (↑Γ₀ : Type u_4)) → Set T) (hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x))
    (hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x) (u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)),
    ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x

Tactic:
choose u v hu hv u_v_disjoint using fun γ : Γ₀ ↦ t2_separation_nhds γ.2.2

Premises used: t2_separation_nhds, And.right, Subtype.property
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
Γ : Type u_4
T : Type u_5
inst : TopologicalSpace T
inst_1 : SMul Γ T
inst_2 : ProperlyDiscontinuousSMul Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite.{u_4 + 1} (↑Γ₀ : Type u_4)
u v : (γ : (↑Γ₀ : Type u_4)) → Set T
hu : ∀ (γ : (↑Γ₀ : Type u_4)), u γ ∈ 𝓝 ((↑γ : Γ) • x)
hv : ∀ (γ : (↑Γ₀ : Type u_4)), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : (↑Γ₀ : Type u_4)), Disjoint (u γ) (v γ)
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), ((fun (x : T) ↦ γ • x) '' U ∩ U).Nonempty → γ • x = x

Tactic:
⟨V ∩ ⋂ γ : Γ₀, (γ.1 • ·) ⁻¹' u γ ∩ v γ, inter_mem V_nhd (iInter_mem.mpr fun γ ↦
    inter_mem ((continuous_const_smul _).continuousAt <| hu γ) (hv γ)), fun γ hγ ↦ ?_⟩

Premises used: Iff.mpr, ContinuousConstSMul.continuous_const_smul, Set.iInter, Filter.inter_mem, Inter.inter, Continuous.continuousAt, Set.preimage, Filter.iInter_mem, And.intro, Exists.intro, HSMul.hSMul, Subtype.val