awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
x : G
hx : f x ≠ 0
⊢ k ∈ 𝓝 x

Tactic:
have : k ∈ 𝓝 x :=
    mem_of_superset (h'f.isOpen_support.mem_nhds hx) hf
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
x : G
hx : f x ≠ 0
this : k ∈ 𝓝 x
⊢ LocallyCompactSpace G

Tactic:
IsCompact.locallyCompactSpace_of_mem_nhds_of_group hk this

Premises used: IsCompact.locallyCompactSpace_of_mem_nhds_of_group
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
x : G
hx : f x ≠ 0
this : k ∈ 𝓝 x
⊢ LocallyCompactSpace G

Tactic:
exact IsCompact.locallyCompactSpace_of_mem_nhds_of_group hk this

Premises used: IsCompact.locallyCompactSpace_of_mem_nhds_of_group
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
hf : HasCompactSupport f
h'f : Continuous[inst, inst_3] f
⊢ f = 0 ∨ LocallyCompactSpace G

Tactic:
eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group hf (subset_tsupport f) h'f

Premises used: subset_tsupport, eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : CompactSpace G
N : Subgroup G
⊢ CompactSpace.{u_1} (G ⧸ N)

Tactic:
Quotient.compactSpace

Premises used: Quotient.compactSpace
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
N : Subgroup G
⊢ IsQuotientMap.{u_1, u_1} (X := G) (Y := G ⧸ N) mk

Tactic:
isQuotientMap_quot_mk

Premises used: Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
N : Subgroup G
⊢ Continuous[inst, instTopologicalSpace N] mk

Tactic:
continuous_quot_mk

Premises used: Quotient, continuous_quot_mk, Quotient.mk'
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsOpenMap.{u_1, u_1} (X := G) (Y := G ⧸ N) mk

Tactic:
isOpenMap_quotient_mk'_mul

Premises used: isOpenMap_quotient_mk'_mul, Quotient.mk'
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsOpenQuotientMap.{u_1, u_1} (X := G) (Y := G ⧸ N) mk

Tactic:
MulAction.isOpenQuotientMap_quotientMk

Premises used: MulAction.isOpenQuotientMap_quotientMk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
s : Set (G ⧸ N)
⊢ Dense (mk ⁻¹' s) ↔ Dense s

Tactic:
isOpenQuotientMap_mk.dense_preimage_iff

Premises used: IsOpenQuotientMap.dense_preimage_iff, QuotientGroup.isOpenQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
rw : Dense (Set.preimage (β := G ⧸ N) mk (mk '' s)) ↔ Dense (s * (↑N : Set G))
rw₁ rw₂ : Dense (s * (↑N : Set G)) ↔ Dense (s * (↑N : Set G))
⊢ Dense (X := G ⧸ N) (mk '' s) ↔ Dense (s * (↑N : Set G))

Tactic:
rw [← dense_preimage_mk, preimage_image_mk_eq_mul]

Premises used: QuotientGroup.preimage_image_mk_eq_mul, QuotientGroup.dense_preimage_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G_1 : Type u_1
inst : TopologicalSpace G_1
inst_1 : Group G_1
inst_2 : SeparatelyContinuousMul G_1
N_1 : Subgroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : ContinuousMul G
N : Subgroup G
rw : Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun (p : G × G ⧸ N) ↦ p.1 • p.2) ∘ Prod.map id mk)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun (p : G × G ⧸ N) ↦ p.1 • p.2

Tactic:
rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]

Premises used: IsOpenQuotientMap.prodMap, IsOpenQuotientMap.id, IsOpenQuotientMap.continuous_comp_iff, QuotientGroup.isOpenQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G_1 : Type u_1
inst : TopologicalSpace G_1
inst_1 : Group G_1
inst_2 : SeparatelyContinuousMul G_1
N_1 : Subgroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : ContinuousMul G
N : Subgroup G
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun (p : G × G ⧸ N) ↦ p.1 • p.2) ∘ Prod.map id mk)

Tactic:
continuous_mk.comp continuous_mul

Premises used: continuous_mul, Continuous.comp, QuotientGroup.continuous_mk, Quot.map, Quotient.map'
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G_1 : Type u_1
inst : TopologicalSpace G_1
inst_1 : Group G_1
inst_2 : SeparatelyContinuousMul G_1
N_1 : Subgroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : ContinuousMul G
N : Subgroup G
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun (p : G × G ⧸ N) ↦ p.1 • p.2) ∘ Prod.map id mk)

Tactic:
exact continuous_mk.comp continuous_mul

Premises used: continuous_mul, Continuous.comp, QuotientGroup.continuous_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
γ : G
rw : Continuous[inst, instTopologicalSpace N] ((fun (x : G ⧸ N) ↦ γ • x) ∘ mk)
⊢ Continuous[instTopologicalSpace N, instTopologicalSpace N] fun (x : G ⧸ N) ↦ γ • x

Tactic:
rw [← isOpenQuotientMap_mk.continuous_comp_iff]

Premises used: IsOpenQuotientMap.continuous_comp_iff, QuotientGroup.isOpenQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
γ : G
⊢ Continuous[inst, instTopologicalSpace N] ((fun (x : G ⧸ N) ↦ γ • x) ∘ mk)

Tactic:
continuous_mk.comp <| continuous_const_smul γ

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, QuotientGroup.continuous_mk, Quot.map, Quotient.map'
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
γ : G
⊢ Continuous[inst, instTopologicalSpace N] ((fun (x : G ⧸ N) ↦ γ • x) ∘ mk)

Tactic:
exact continuous_mk.comp <| continuous_const_smul γ

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, QuotientGroup.continuous_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
rw :
  IsClosed[inst] (Set.preimage (β := G ⧸ N) Quotient.mk' {(↑1 : G ⧸ N)}) ↔
    IsClosed[inst] (Set.preimage (β := G ⧸ N) mk {(↑1 : G ⧸ N)})
⊢ T1Space.{u_1} (G ⧸ N) ↔ IsClosed[inst] (↑N : Set G)

Tactic:
rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1),
      isClosed_coinduced]

Premises used: QuotientGroup.mk, QuotientGroup.preimage_mk_one, OfNat.ofNat, isClosed_coinduced, MulAction.IsPretransitive.t1Space_iff
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsClosed[inst] (Set.preimage (β := G ⧸ N) Quotient.mk' {(↑1 : G ⧸ N)}) ↔
    IsClosed[inst] (Set.preimage (β := G ⧸ N) mk {(↑1 : G ⧸ N)})

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
rw :
  IsOpen[inst] (Set.preimage (β := G ⧸ N) Quotient.mk' {(↑1 : G ⧸ N)}) ↔
    IsOpen[inst] (Set.preimage (β := G ⧸ N) mk {(↑1 : G ⧸ N)})
⊢ DiscreteTopology.{u_1} (G ⧸ N) ↔ IsOpen[inst] (↑N : Set G)

Tactic:
rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.discreteTopology_iff G (mk 1),
      isOpen_coinduced]

Premises used: QuotientGroup.mk, isOpen_coinduced, QuotientGroup.preimage_mk_one, OfNat.ofNat, MulAction.IsPretransitive.discreteTopology_iff
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsOpen[inst] (Set.preimage (β := G ⧸ N) Quotient.mk' {(↑1 : G ⧸ N)}) ↔
    IsOpen[inst] (Set.preimage (β := G ⧸ N) mk {(↑1 : G ⧸ N)})

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
hN : IsClosed[inst] (↑N : Set G)
⊢ T1Space.{u_1} (G ⧸ N)

Tactic:
t1Space_iff.mpr hN

Premises used: Iff.mpr, QuotientGroup.t1Space_iff
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
hN : IsOpen[inst] (↑N : Set G)
⊢ DiscreteTopology.{u_1} (G ⧸ N)

Tactic:
discreteTopology_iff.mpr hN

Premises used: Iff.mpr, QuotientGroup.discreteTopology_iff
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N_1 : Subgroup G
inst_3 : LocallyCompactSpace G
N : Subgroup G
⊢ LocallyCompactSpace.{u_1} (G ⧸ N)

Tactic:
QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace

Premises used: IsOpenQuotientMap.locallyCompactSpace, QuotientGroup.isOpenQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
x : G
⊢ Eq (α := Filter (G ⧸ N)) (𝓝 (↑x : G ⧸ N)) (Filter.map mk (𝓝 x))

Tactic:
(isOpenQuotientMap_mk.map_nhds_eq _).symm

Premises used: IsOpenQuotientMap.map_nhds_eq, QuotientGroup.isOpenQuotientMap_mk, Eq.symm
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
inst_3 : SecondCountableTopology G
⊢ SecondCountableTopology.{u_1} (G ⧸ N)

Tactic:
ContinuousConstSMul.secondCountableTopology

Premises used: ContinuousConstSMul.secondCountableTopology
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
rw :
  Continuous[instTopologicalSpaceProd, instTopologicalSpace N]
    ((fun (p : (G ⧸ N) × G ⧸ N) ↦ p.1 * p.2) ∘ Prod.map mk mk)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun (p : (G ⧸ N) × G ⧸ N) ↦ p.1 * p.2

Tactic:
rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]

Premises used: IsOpenQuotientMap.prodMap, IsOpenQuotientMap.continuous_comp_iff, QuotientGroup.isOpenQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N]
    ((fun (p : (G ⧸ N) × G ⧸ N) ↦ p.1 * p.2) ∘ Prod.map mk mk)

Tactic:
continuous_mk.comp continuous_mul

Premises used: continuous_mul, Continuous.comp, Quotient.map₂, QuotientGroup.continuous_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N]
    ((fun (p : (G ⧸ N) × G ⧸ N) ↦ p.1 * p.2) ∘ Prod.map mk mk)

Tactic:
exact continuous_mk.comp continuous_mul

Premises used: continuous_mul, Continuous.comp, QuotientGroup.continuous_mk
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact (↑H : Set G)
t : Set G
ht : IsClosed[inst] t
rw : IsClosed[inst] (t * (↑H : Set G))
⊢ IsClosed[instTopologicalSpace H] (mk '' t)

Tactic:
rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]

Premises used: QuotientGroup.isQuotientMap_mk, QuotientGroup.preimage_image_mk_eq_mul, Topology.IsCoinducing.isClosed_preimage, Topology.IsQuotientMap.isCoinducing
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact (↑H : Set G)
t : Set G
ht : IsClosed[inst] t
⊢ IsClosed[inst] (t * (↑H : Set G))

Tactic:
ht.mul_right_of_isCompact hH

Premises used: IsClosed.mul_right_of_isCompact
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact (↑H : Set G)
t : Set G
ht : IsClosed[inst] t
⊢ IsClosed[inst] (t * (↑H : Set G))

Tactic:
exact ht.mul_right_of_isCompact hH

Premises used: IsClosed.mul_right_of_isCompact
-- Module: Mathlib.Topology.Algebra.Group.Quotient
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
N : Subgroup G
inst_3 : N.Normal
hN : IsClosed[inst] (↑N : Set G)
⊢ T3Space.{u_1} (G ⧸ N)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : DivInvMonoid G
inst_1 : TopologicalSpace G
x y : G
simp_rw : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
simp_rw₁ : ClusterPt x (map (fun (x : ℤ) ↦ y ^ x) (map Nat.cast atTop)) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
simp_rw₂ : ClusterPt x (map ((fun (x : ℤ) ↦ y ^ x) ∘ Nat.cast) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
simp_rw₃ :
  ClusterPt x (map (fun (x : ℕ) ↦ HPow.hPow (β := ℤ) y (↑x : ℤ)) atTop) ↔ ClusterPt x (map (fun (x : ℕ) ↦ y ^ x) atTop)
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x

Tactic:
simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]

Premises used: zpow_natCast, Filter.map_map, Function.comp_def, MapClusterPt, Nat.map_cast_int_atTop
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
⊢ ∃ (y : G), MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1

Tactic:
exists_clusterPt_of_compactSpace _

Premises used: exists_clusterPt_of_compactSpace, MapClusterPt
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
obtain :
  ∀ (y : G) (hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1), MapClusterPt (x ^ m) atTop fun (x_1 : ℕ) ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℕ) ↦ x ^ x_1

Tactic:
obtain ⟨y, hy⟩ : ∃ y, MapClusterPt y atTop (x ^ · : ℤ → G) :=
    exists_clusterPt_of_compactSpace _

Premises used: exists_clusterPt_of_compactSpace
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
rw : MapClusterPt (x ^ m) atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℕ) ↦ x ^ x_1

Tactic:
rw [← mapClusterPt_atTop_zpow_iff_pow]

Premises used: mapClusterPt_atTop_zpow_iff_pow
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ ContinuousAt (Y := G) (fun (yz : G × G) ↦ x ^ m * yz.2 / yz.1) (y, y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ ContinuousAt (Y := G) (fun (yz : G × G) ↦ x ^ m * yz.2 / yz.1) (y, y)

Tactic:
have : ContinuousAt (fun yz ↦ x ^ m * yz.2 / yz.1) (y, y) := by fun_prop
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
this : ContinuousAt (Y := G) (fun (yz : G × G) ↦ x ^ m * yz.2 / yz.1) (y, y)
⊢ MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))

Tactic:
simpa only [comp_def, ← zpow_sub, ← zpow_add, div_eq_mul_inv, Prod.map, mul_inv_cancel_right]
      using (hy.curry_prodMap hy).continuousAt_comp this

Premises used: mul_inv_cancel_right, zpow_add, Prod.map, div_eq_mul_inv, Function.comp_def, MapClusterPt.continuousAt_comp, MapClusterPt.curry_prodMap, zpow_sub
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))

Tactic:
have H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿(fun a b ↦ x ^ (m + b - a)) := by
    have : ContinuousAt (fun yz ↦ x ^ m * yz.2 / yz.1) (y, y) := by fun_prop
    simpa only [comp_def, ← zpow_sub, ← zpow_add, div_eq_mul_inv, Prod.map, mul_inv_cancel_right]
      using (hy.curry_prodMap hy).continuousAt_comp this
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
suffices : Tendsto (HasUncurry.uncurry (α := (a b : ℤ) → ℤ) fun (a b : ℤ) ↦ m + b - a) (Filter.curry atTop atTop) atTop
⊢ MapClusterPt (x ^ m) atTop fun (x_1 : ℤ) ↦ x ^ x_1

Tactic:
suffices Tendsto ↿(fun a b ↦ m + b - a) (atTop.curry atTop) atTop from H.of_comp this
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
⊢ Tendsto (HasUncurry.uncurry (α := (a b : ℤ) → ℤ) fun (a b : ℤ) ↦ m + b - a) (Filter.curry atTop atTop) atTop

Tactic:
Tendsto.curry <| .of_forall fun a ↦ ?_

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.curry
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
refine : ∀ (a : ℤ), Tendsto (β := ℤ) (fun (b : ℤ) ↦ m + b - a) atTop atTop
⊢ Tendsto (HasUncurry.uncurry (α := (a b : ℤ) → ℤ) fun (a b : ℤ) ↦ m + b - a) (Filter.curry atTop atTop) atTop

Tactic:
refine Tendsto.curry <| .of_forall fun a ↦ ?_

Premises used: Filter.Tendsto.curry
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
a : ℤ
⊢ Tendsto (β := ℤ) (fun (b : ℤ) ↦ m + b + -a) atTop atTop

Tactic:
tendsto_atTop_add_const_right _ _ (tendsto_atTop_add_const_left atTop m tendsto_id)

Premises used: Filter.tendsto_atTop_add_const_right, Filter.tendsto_atTop_add_const_left, Filter.tendsto_id, Filter.atTop
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun (x_1 : ℤ) ↦ x ^ x_1
H :
  MapClusterPt (x ^ m) (Filter.curry atTop atTop)
    (HasUncurry.uncurry (α := (a b : ℤ) → G) fun (a b : ℤ) ↦ x ^ (m + b - a))
a : ℤ
⊢ Tendsto (β := ℤ) (fun (b : ℤ) ↦ m + b + -a) atTop atTop

Tactic:
exact tendsto_atTop_add_const_right _ _ (tendsto_atTop_add_const_left atTop m tendsto_id)

Premises used: Filter.tendsto_atTop_add_const_right, Filter.tendsto_atTop_add_const_left, Filter.tendsto_id, Filter.atTop
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
⊢ MapClusterPt.{u_1, 0} (X := G) 1 atTop fun (x_1 : ℕ) ↦ x ^ x_1

Tactic:
simpa using mapClusterPt_self_zpow_atTop_pow x 0

Premises used: mapClusterPt_self_zpow_atTop_pow, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x : G
⊢ MapClusterPt x atTop fun (x_1 : ℕ) ↦ x ^ x_1

Tactic:
simpa using mapClusterPt_self_zpow_atTop_pow x 1

Premises used: mapClusterPt_self_zpow_atTop_pow, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
⊢ MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
⊢ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x

Tactic:
2 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
⊢ (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x

Tactic:
tfae_have 2 ↔ 1 := mapClusterPt_atTop_zpow_iff_pow

Premises used: mapClusterPt_atTop_zpow_iff_pow
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun (x : ℤ) ↦ y ^ x) ↔ MapClusterPt x atTop fun (x : ℕ) ↦ y ^ x
⊢ Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℕ) ↦ y ^ x)) x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false