-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem mapClusterPt_self_zpow_atTop_pow (x : G) (m : ℤ) :
    MapClusterPt (x ^ m) atTop (x ^ · : ℕ → G)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
⊢ MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)

Tactic:
have : ContinuousAt (fun yz ↦ x ^ m * yz.2 / yz.1) (y, y) := by fun_prop

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
this : ContinuousAt (fun yz => x ^ m * yz.2 / yz.1) (y, y)
⊢ MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿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)

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
a : ℤ
⊢ Tendsto (fun b => m + b - a) atTop atTop

Tactic:
simp only [sub_eq_add_neg]

Result:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
a : ℤ
⊢ Tendsto (fun b => m + b + -a) atTop atTop

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
⊢ 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

Result:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
⊢ Tendsto (↿fun a b => m + b - a) (atTop.curry atTop) atTop

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
⊢ Tendsto (↿fun a b => m + b - a) (atTop.curry atTop) atTop

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

Result:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
a : ℤ
⊢ Tendsto (fun b => m + b - a) atTop atTop

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
this : ContinuousAt (fun yz => x ^ m * yz.2 / yz.1) (y, y)
⊢ MapClusterPt (x ^ m) (atTop.curry atTop) ↿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

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
⊢ ContinuousAt (fun yz => x ^ m * yz.2 / yz.1) (y, y)

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 => x ^ x_1

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

Result:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 => x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b => x ^ (m + b - a)
⊢ MapClusterPt (x ^ m) atTop fun x_1 => x ^ x_1