-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem tprod_const [T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β)

Proof state:
case inr.inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ∏' (x : β), a = 1

Tactic:
apply tprod_eq_one_of_not_multipliable

Result:
case inr.inr.h
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ¬Multipliable fun b => a

Proof state:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]

Result:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏ b : β, a = a ^ Nat.card β

Proof state:
case inr.inr.h
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ¬Multipliable fun b => a

Tactic:
simpa [multipliable_const_iff] using ha

Result:
no goals

Proof state:
case inr.inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
hβ : Infinite β
⊢ ∏' (x : β), 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏ b : β, a = a ^ Nat.card β

Tactic:
simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]

Result:
no goals

Proof state:
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
rcases finite_or_infinite β with hβ|hβ

Result:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
⊢ ∏' (x : β), a = a ^ Nat.card β

case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Proof state:
case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = 1

Tactic:
rcases eq_or_ne a 1 with rfl|ha

Result:
case inr.inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
hβ : Infinite β
⊢ ∏' (x : β), 1 = 1

case inr.inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ∏' (x : β), a = 1

Proof state:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
letI : Fintype β := Fintype.ofFinite β

Result:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Proof state:
case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
simp only [Nat.card_eq_zero_of_infinite, pow_zero]

Result:
case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = 1