-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem multipliable_const_iff [Infinite β] [T2Space G] (a : G) :
    Multipliable (fun _ : β ↦ a) ↔ a = 1

Proof state:
case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
⊢ Multipliable fun x => 1

Tactic:
exact multipliable_one

Result:
no goals

Proof state:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
⊢ False

Tactic:
have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)

Result:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
this : {a}ᶜ ∈ 𝓝 1
⊢ False

Proof state:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
this✝ : {a}ᶜ ∈ 𝓝 1
this : Finite β
⊢ False

Tactic:
exact not_finite β

Result:
no goals

Proof state:
case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ a = 1 → Multipliable fun x => a

Tactic:
rintro rfl

Result:
case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
⊢ Multipliable fun x => 1

Proof state:
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
this : {a}ᶜ ∈ 𝓝 1
⊢ Finite β

Tactic:
simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this

Result:
no goals

Proof state:
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ (Multipliable fun x => a) ↔ a = 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
⊢ a = 1

case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ a = 1 → Multipliable fun x => a

Proof state:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
this : {a}ᶜ ∈ 𝓝 1
⊢ False

Tactic:
have : Finite β := by
  simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this

Result:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
this✝ : {a}ᶜ ∈ 𝓝 1
this : Finite β
⊢ False

Proof state:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
⊢ a = 1

Tactic:
by_contra ha

Result:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x => a
ha : ¬a = 1
⊢ False