-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem mapClusterPt_atTop_pow_tfae (x y : G) :
    List.TFAE [
      MapClusterPt x atTop (y ^ · : ℕ → G),
      MapClusterPt x atTop (y ^ · : ℤ → G),
      x ∈ closure (range (y ^ · : ℕ → G)),
      x ∈ closure (range (y ^ · : ℤ → G)),
    ]

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
⊢ x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)

Tactic:
refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
h : x ∈ closure (range fun x => y ^ x)
n : ℕ
⊢ y ^ n ∈ range fun x => y ^ x

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
tfae_4_to_1 : x ∈ closure (range fun x => y ^ x) → MapClusterPt x atTop fun x => y ^ x
tfae_1_to_3 : (MapClusterPt x atTop fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
⊢ x ∈ closure (range fun x => y ^ x) → MapClusterPt x atTop fun x => y ^ x

Tactic:
refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
h : x ∈ closure (range fun x => y ^ x)
⊢ (range fun x => y ^ x) ⊆ {x | ClusterPt x (map (fun x => y ^ x) atTop)}

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
h : x ∈ closure (range fun x => y ^ x)
⊢ (range fun x => y ^ x) ⊆ {x | ClusterPt x (map (fun x => y ^ x) atTop)}

Tactic:
exact range_subset_iff.2 (mapClusterPt_self_zpow_atTop_pow _)

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
tfae_4_to_1 : x ∈ closure (range fun x => y ^ x) → MapClusterPt x atTop fun x => y ^ x
⊢ (MapClusterPt x atTop fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)

Tactic:
rw [mem_closure_iff_clusterPt]

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
tfae_4_to_1 : x ∈ closure (range fun x => y ^ x) → MapClusterPt x atTop fun x => y ^ x
⊢ (MapClusterPt x atTop fun x => y ^ x) → ClusterPt x (𝓟 (range fun x => y ^ x))

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
h : x ∈ closure (range fun x => y ^ x)
n : ℕ
⊢ y ^ n ∈ range fun x => y ^ x

Tactic:
exact ⟨n, zpow_natCast _ _⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE

Tactic:
tfae_have 3 → 4 := by
  refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h
  exact ⟨n, zpow_natCast _ _⟩

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE

Tactic:
tfae_have 4 → 1 := by
  refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h
  exact range_subset_iff.2 (mapClusterPt_self_zpow_atTop_pow _)

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
tfae_3_to_4 : x ∈ closure (range fun x => y ^ x) → x ∈ closure (range fun x => y ^ x)
tfae_4_to_1 : x ∈ closure (range fun x => y ^ x) → MapClusterPt x atTop fun x => y ^ x
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE

Tactic:
tfae_have 2 ↔ 1 := mapClusterPt_atTop_zpow_iff_pow

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x
⊢ [MapClusterPt x atTop fun x => y ^ x, MapClusterPt x atTop fun x => y ^ x, x ∈ closure (range fun x => y ^ x),
      x ∈ closure (range fun x => y ^ x)].TFAE