-- Mathlib/Algebra/Group/Pointwise/Set/Finite.lean
theorem card_pow_eq_card_pow_card_univ [∀ k : ℕ, DecidablePred (· ∈ S ^ k)] :
    ∀ k, Fintype.card G ≤ k → Fintype.card (↥(S ^ k)) = Fintype.card (↥(S ^ Fintype.card G))

Proof state:
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ Fintype ↑(S ^ n * Set.singleton a)

Tactic:
classical
apply fintypeMul

Result:
no goals

Proof state:
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)

Result:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)

case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Proof state:
case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
have key : ∀ (a) (s t : Set G) [Fintype s] [Fintype t],
    (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t := by
  refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
  rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
  exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))

Result:
case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Proof state:
case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})

Tactic:
convert key a (S ^ n) (S ^ n * {a}) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)

Result:
no goals

Proof state:
case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
  monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul hb ha

Result:
case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Proof state:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(∅ ^ k) ≃ ↑(∅ ^ Fintype.card G)

Tactic:
rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]

Result:
no goals

Proof state:
case refine_1
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

Tactic:
exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)

Result:
no goals

Proof state:
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

Tactic:
refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_

Result:
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a✝ : G
ha : a✝ ∈ S
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ b ∈ s, b * a ∈ t
⊢ Function.Injective fun x =>
    match x with
    | ⟨b, hb⟩ => ⟨b * a, ⋯⟩

Proof state:
case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ ⦃x : G⦄, x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)

Tactic:
intro x hx

Result:
case inr.intro
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
x : G
hx : x ∈ S ^ (n + 1)
⊢ x * a * a⁻¹ ∈ S ^ (n + 1)

Proof state:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)

Tactic:
refine fun k hk ↦ Fintype.card_congr ?_

Result:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(∅ ^ k) ≃ ↑(∅ ^ Fintype.card G)