/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Floris van Doorn

! This file was ported from Lean 3 source module data.set.pointwise.finite
! leanprover-community/mathlib commit c941bb9426d62e266612b6d99e6c9fc93e7a1d07
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Finite
import Mathlib.Data.Set.Pointwise.SMul

/-! # Finiteness lemmas for pointwise operations on sets -/


open Pointwise

variable {F: Type ?u.31000
F α: Type ?u.5
α β: Type ?u.31006
β γ: Type ?u.31009
γ : Type _: Type (?u.11+1)
Type _}

namespace Set

section One

variable [One: Type ?u.41 → Type ?u.41
One α: Type ?u.17
α]

@[to_additive: ∀ {α : Type u_1} [inst : Zero α], Set.Finite 0
to_additive (attr := simp)]
theorem finite_one: ∀ {α : Type u_1} [inst : One α], Set.Finite 1
finite_one : (1: ?m.47
1 : Set: Type ?u.45 → Type ?u.45
Set α: Type ?u.32
α).Finite: {α : Type ?u.90} → Set α → Prop
Finite :=
  finite_singleton: ∀ {α : Type ?u.95} (a : α), Set.Finite {a}
finite_singleton _: ?m.96
_
#align set.finite_one Set.finite_one: ∀ {α : Type u_1} [inst : One α], Set.Finite 1
Set.finite_one
#align set.finite_zero Set.finite_zero: ∀ {α : Type u_1} [inst : Zero α], Set.Finite 0
Set.finite_zero

end One

section InvolutiveInv

variable [InvolutiveInv: Type ?u.156 → Type ?u.156
InvolutiveInv α: Type ?u.147
α] {s: Set α
s : Set: Type ?u.177 → Type ?u.177
Set α: Type ?u.147
α}

@[to_additive: ∀ {α : Type u_1} [inst : InvolutiveNeg α] {s : Set α}, Set.Finite s → Set.Finite (-s)
to_additive]
theorem Finite.inv: Set.Finite s → Set.Finite s⁻¹
Finite.inv (hs: Set.Finite s
hs : s: Set α
s.Finite: {α : Type ?u.180} → Set α → Prop
Finite) : s: Set α
s⁻¹.Finite: {α : Type ?u.359} → Set α → Prop
Finite :=
  hs: Set.Finite s
hs.preimage: ∀ {α : Type ?u.366} {β : Type ?u.365} {s : Set β} {f : α → β}, InjOn f (f ⁻¹' s) → Set.Finite s → Set.Finite (f ⁻¹' s)
preimage <| inv_injective: ∀ {G : Type ?u.388} [inst : InvolutiveInv G], Function.Injective Inv.inv
inv_injective.injOn: ∀ {α : Type ?u.406} {β : Type ?u.407} {f : α → β}, Function.Injective f → ∀ (s : Set α), InjOn f s
injOn _: Set ?m.418
_
#align set.finite.inv Set.Finite.inv: ∀ {α : Type u_1} [inst : InvolutiveInv α] {s : Set α}, Set.Finite s → Set.Finite s⁻¹
Set.Finite.inv
#align set.finite.neg Set.Finite.neg: ∀ {α : Type u_1} [inst : InvolutiveNeg α] {s : Set α}, Set.Finite s → Set.Finite (-s)
Set.Finite.neg

end InvolutiveInv

section Mul

variable [Mul: Type ?u.494 → Type ?u.494
Mul α: Type ?u.485
α] {s: Set α
s t: Set α
t : Set: Type ?u.479 → Type ?u.479
Set α: Type ?u.464
α}

@[to_additive: ∀ {α : Type u_1} [inst : Add α] {s t : Set α}, Set.Finite s → Set.Finite t → Set.Finite (s + t)
to_additive]
theorem Finite.mul: ∀ {α : Type u_1} [inst : Mul α] {s t : Set α}, Set.Finite s → Set.Finite t → Set.Finite (s * t)
Finite.mul : s: Set α
s.Finite: {α : Type ?u.504} → Set α → Prop
Finite → t: Set α
t.Finite: {α : Type ?u.511} → Set α → Prop
Finite → (s: Set α
s * t: Set α
t).Finite: {α : Type ?u.588} → Set α → Prop
Finite :=
  Finite.image2: ∀ {α : Type ?u.595} {β : Type ?u.594} {γ : Type ?u.593} {s : Set α} {t : Set β} (f : α → β → γ),
  Set.Finite s → Set.Finite t → Set.Finite (image2 f s t)
Finite.image2 _: ?m.596 → ?m.597 → ?m.598
_
#align set.finite.mul Set.Finite.mul: ∀ {α : Type u_1} [inst : Mul α] {s t : Set α}, Set.Finite s → Set.Finite t → Set.Finite (s * t)
Set.Finite.mul
#align set.finite.add Set.Finite.add: ∀ {α : Type u_1} [inst : Add α] {s t : Set α}, Set.Finite s → Set.Finite t → Set.Finite (s + t)
Set.Finite.add

/-- Multiplication preserves finiteness. -/
@[to_additive: {α : Type u_1} →
  [inst : Add α] →
    [inst_1 : DecidableEq α] → (s t : Set α) → [inst_2 : Fintype ↑s] → [inst_3 : Fintype ↑t] → Fintype ↑(s + t)
to_additive "Addition preserves finiteness."]
def fintypeMul: [inst : DecidableEq α] → (s t : Set α) → [inst : Fintype ↑s] → [inst : Fintype ↑t] → Fintype ↑(s * t)
fintypeMul [DecidableEq: Sort ?u.678 → Sort (max1?u.678)
DecidableEq α: Type ?u.660
α] (s: Set α
s t: Set α
t : Set: Type ?u.687 → Type ?u.687
Set α: Type ?u.660
α) [Fintype: Type ?u.693 → Type ?u.693
Fintype s: Set α
s] [Fintype: Type ?u.825 → Type ?u.825
Fintype t: Set α
t] : Fintype: Type ?u.950 → Type ?u.950
Fintype (s: Set α
s * t: Set α
t : Set: Type ?u.952 → Type ?u.952
Set α: Type ?u.660
α) :=
  Set.fintypeImage2: {α : Type ?u.1155} →
  {β : Type ?u.1154} →
    {γ : Type ?u.1153} →
      [inst : DecidableEq γ] →
        (f : α → β → γ) → (s : Set α) → (t : Set β) → [hs : Fintype ↑s] → [ht : Fintype ↑t] → Fintype ↑(image2 f s t)
Set.fintypeImage2 _: ?m.1156 → ?m.1157 → ?m.1158
_ _: Set ?m.1156
_ _: Set ?m.1157
_
#align set.fintype_mul Set.fintypeMul: {α : Type u_1} →
  [inst : Mul α] →
    [inst_1 : DecidableEq α] → (s t : Set α) → [inst_2 : Fintype ↑s] → [inst_3 : Fintype ↑t] → Fintype ↑(s * t)
Set.fintypeMul
#align set.fintype_add Set.fintypeAdd: {α : Type u_1} →
  [inst : Add α] →
    [inst_1 : DecidableEq α] → (s t : Set α) → [inst_2 : Fintype ↑s] → [inst_3 : Fintype ↑t] → Fintype ↑(s + t)
Set.fintypeAdd

end Mul

section Monoid

variable [Monoid: Type ?u.1829 → Type ?u.1829
Monoid α: Type ?u.1820
α] {s: Set α
s t: Set α
t : Set: Type ?u.1811 → Type ?u.1811
Set α: Type ?u.1820
α}

@[to_additive: {α : Type u_1} →
  [inst : AddMonoid α] →
    {s t : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] →
          [inst_3 : DecidablePred fun x => x ∈ s] →
            [inst_4 : DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s + t
to_additive]
instance decidableMemMul: {α : Type u_1} →
  [inst : Monoid α] →
    {s t : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] →
          [inst_3 : DecidablePred fun x => x ∈ s] →
            [inst_4 : DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s * t
decidableMemMul [Fintype: Type ?u.1838 → Type ?u.1838
Fintype α: Type ?u.1820
α] [DecidableEq: Sort ?u.1841 → Sort (max1?u.1841)
DecidableEq α: Type ?u.1820
α] [DecidablePred: {α : Sort ?u.1850} → (α → Prop) → Sort (max1?u.1850)
DecidablePred (· ∈ s: Set α
s)]
    [DecidablePred: {α : Sort ?u.1880} → (α → Prop) → Sort (max1?u.1880)
DecidablePred (· ∈ t: Set α
t)] : DecidablePred: {α : Sort ?u.1906} → (α → Prop) → Sort (max1?u.1906)
DecidablePred (· ∈ s: Set α
s * t: Set α
t) := fun _: ?m.2691
_ ↦ decidable_of_iff: {b : Prop} → (a : Prop) → (a ↔ b) → [inst : Decidable a] → Decidable b
decidable_of_iff _: Prop
_ mem_mul: ∀ {α : Type ?u.2697} [inst : Mul α] {s t : Set α} {a : α}, a ∈ s * t ↔ ∃ x y, x ∈ s ∧ y ∈ t ∧ x * y = a
mem_mul.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
#align set.decidable_mem_mul Set.decidableMemMul: {α : Type u_1} →
  [inst : Monoid α] →
    {s t : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] →
          [inst_3 : DecidablePred fun x => x ∈ s] →
            [inst_4 : DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s * t
Set.decidableMemMul
#align set.decidable_mem_add Set.decidableMemAdd: {α : Type u_1} →
  [inst : AddMonoid α] →
    {s t : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] →
          [inst_3 : DecidablePred fun x => x ∈ s] →
            [inst_4 : DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s + t
Set.decidableMemAdd

@[to_additive: {α : Type u_1} →
  [inst : AddMonoid α] →
    {s : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] → [inst_3 : DecidablePred fun x => x ∈ s] → (n : ℕ) → DecidablePred fun x => x ∈ n • s
to_additive]
instance decidableMemPow: [inst : Fintype α] →
  [inst : DecidableEq α] → [inst : DecidablePred fun x => x ∈ s] → (n : ℕ) → DecidablePred fun x => x ∈ s ^ n
decidableMemPow [Fintype: Type ?u.4466 → Type ?u.4466
Fintype α: Type ?u.4448
α] [DecidableEq: Sort ?u.4469 → Sort (max1?u.4469)
DecidableEq α: Type ?u.4448
α] [DecidablePred: {α : Sort ?u.4478} → (α → Prop) → Sort (max1?u.4478)
DecidablePred (· ∈ s: Set α
s)] (n: ℕ
n : ℕ: Type
ℕ) :
    DecidablePred: {α : Sort ?u.4510} → (α → Prop) → Sort (max1?u.4510)
DecidablePred (· ∈ s: Set α
s ^ n: ℕ
n) := by
Goals accomplished! 🐙
  F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

DecidablePred fun x => x ∈ s ^ ninduction' n: ℕ
n with n: ℕ
n ih: ?m.28961 n
ihF: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

zeroDecidablePred fun x => x ∈ s ^ Nat.zero
F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ n
  F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

DecidablePred fun x => x ∈ s ^ n·F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

zeroDecidablePred fun x => x ∈ s ^ Nat.zero F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

zeroDecidablePred fun x => x ∈ s ^ Nat.zero
F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ nsimp only [Nat.zero_eq: Nat.zero = 0
Nat.zero_eq, pow_zero: ∀ {M : Type ?u.28984} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zero, mem_one: ∀ {α : Type ?u.29001} [inst : One α] {a : α}, a ∈ 1 ↔ a = 1
mem_one]F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

zeroDecidablePred fun x => x = 1
    F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

zeroDecidablePred fun x => x ∈ s ^ Nat.zeroinfer_instance
Goals accomplished! 🐙
  F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

DecidablePred fun x => x ∈ s ^ n·F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ n F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ nletI := ih: ?m.28961 n
ihF: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

this:= ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ n
    F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ nrw [F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

this:= ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ npow_succ: ∀ {M : Type ?u.29662} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succF: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

this:= ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s * s ^ n]F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

this:= ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s * s ^ n
    F: Type ?u.4445

α: Type ?u.4448

β: Type ?u.4451

γ: Type ?u.4454

inst✝³: Monoid α

s, t: Set α

inst✝²: Fintype α

inst✝¹: DecidableEq α

inst✝: DecidablePred fun x => x ∈ s

n: ℕ

ih: DecidablePred fun x => x ∈ s ^ n

succDecidablePred fun x => x ∈ s ^ Nat.succ ninfer_instance
Goals accomplished! 🐙
#align set.decidable_mem_pow Set.decidableMemPow: {α : Type u_1} →
  [inst : Monoid α] →
    {s : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] → [inst_3 : DecidablePred fun x => x ∈ s] → (n : ℕ) → DecidablePred fun x => x ∈ s ^ n
Set.decidableMemPow
#align set.decidable_mem_nsmul Set.decidableMemNSMul: {α : Type u_1} →
  [inst : AddMonoid α] →
    {s : Set α} →
      [inst_1 : Fintype α] →
        [inst_2 : DecidableEq α] → [inst_3 : DecidablePred fun x => x ∈ s] → (n : ℕ) → DecidablePred fun x => x ∈ n • s
Set.decidableMemNSMul

end Monoid

section SMul

variable [SMul: Type ?u.31013 → Type ?u.31012 → Type (max?u.31013?u.31012)
SMul α: Type ?u.30981
α β: Type ?u.31006
β] {s: Set α
s : Set: Type ?u.31016 → Type ?u.31016
Set α: Type ?u.30981
α} {t: Set β
t : Set: Type ?u.31019 → Type ?u.31019
Set β: Type ?u.30984
β}

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {s : Set α} {t : Set β},
  Set.Finite s → Set.Finite t → Set.Finite (s +ᵥ t)
to_additive]
theorem Finite.smul: ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s : Set α} {t : Set β},
  Set.Finite s → Set.Finite t → Set.Finite (s • t)
Finite.smul : s: Set α
s.Finite: {α : Type ?u.31023} → Set α → Prop
Finite → t: Set β
t.Finite: {α : Type ?u.31030} → Set α → Prop
Finite → (s: Set α
s • t: Set β
t).Finite: {α : Type ?u.31087} → Set α → Prop
Finite :=
  Finite.image2: ∀ {α : Type ?u.31094} {β : Type ?u.31093} {γ : Type ?u.31092} {s : Set α} {t : Set β} (f : α → β → γ),
  Set.Finite s → Set.Finite t → Set.Finite (image2 f s t)
Finite.image2 _: ?m.31095 → ?m.31096 → ?m.31097
_
#align set.finite.smul Set.Finite.smul: ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s : Set α} {t : Set β},
  Set.Finite s → Set.Finite t → Set.Finite (s • t)
Set.Finite.smul
#align set.finite.vadd Set.Finite.vadd: ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {s : Set α} {t : Set β},
  Set.Finite s → Set.Finite t → Set.Finite (s +ᵥ t)
Set.Finite.vadd

end SMul

section HasSmulSet

variable [SMul: Type ?u.31331 → Type ?u.31330 → Type (max?u.31331?u.31330)
SMul α: Type ?u.31168
α β: Type ?u.31324
β] {s: Set β
s : Set: Type ?u.31202 → Type ?u.31202
Set β: Type ?u.31171
β} {a: α
a : α: Type ?u.31168
α}

@[to_additive: ∀ {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α}, Set.Finite s → Set.Finite (a +ᵥ s)
to_additive]
theorem Finite.smul_set: Set.Finite s → Set.Finite (a • s)
Finite.smul_set : s: Set β
s.Finite: {α : Type ?u.31208} → Set α → Prop
Finite → (a: α
a • s: Set β
s).Finite: {α : Type ?u.31261} → Set α → Prop
Finite :=
  Finite.image: ∀ {α : Type ?u.31267} {β : Type ?u.31266} {s : Set α} (f : α → β), Set.Finite s → Set.Finite (f '' s)
Finite.image _: ?m.31268 → ?m.31269
_
#align set.finite.smul_set Set.Finite.smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α}, Set.Finite s → Set.Finite (a • s)
Set.Finite.smul_set
#align set.finite.vadd_set Set.Finite.vadd_set: ∀ {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α}, Set.Finite s → Set.Finite (a +ᵥ s)
Set.Finite.vadd_set

@[to_additive: ∀ {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α}, Set.Infinite (a +ᵥ s) → Set.Infinite s
to_additive]
theorem Infinite.of_smul_set: Set.Infinite (a • s) → Set.Infinite s
Infinite.of_smul_set : (a: α
a • s: Set β
s).Infinite: {α : Type ?u.31388} → Set α → Prop
Infinite → s: Set β
s.Infinite: {α : Type ?u.31393} → Set α → Prop
Infinite :=
  Infinite.of_image: ∀ {α : Type ?u.31400} {β : Type ?u.31399} (f : α → β) {s : Set α}, Set.Infinite (f '' s) → Set.Infinite s
Infinite.of_image _: ?m.31401 → ?m.31402
_
#align set.infinite.of_smul_set Set.Infinite.of_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α}, Set.Infinite (a • s) → Set.Infinite s
Set.Infinite.of_smul_set
#align set.infinite.of_vadd_set Set.Infinite.of_vadd_set: ∀ {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α}, Set.Infinite (a +ᵥ s) → Set.Infinite s
Set.Infinite.of_vadd_set

end HasSmulSet

section Vsub

variable [VSub: outParam (Type ?u.31467) → Type ?u.31466 → Type (max?u.31467?u.31466)
VSub α: Type ?u.31479
α β: Type ?u.31460
β] {s: Set β
s t: Set β
t : Set: Type ?u.31495 → Type ?u.31495
Set β: Type ?u.31460
β}

theorem Finite.vsub: ∀ {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s t : Set β}, Set.Finite s → Set.Finite t → Set.Finite (s -ᵥ t)
Finite.vsub (hs: Set.Finite s
hs : s: Set β
s.Finite: {α : Type ?u.31498} → Set α → Prop
Finite) (ht: Set.Finite t
ht : t: Set β
t.Finite: {α : Type ?u.31505} → Set α → Prop
Finite) : Set.Finite: {α : Type ?u.31511} → Set α → Prop
Set.Finite (s: Set β
s -ᵥ t: Set β
t) :=
  hs: Set.Finite s
hs.image2: ∀ {α : Type ?u.31543} {β : Type ?u.31542} {γ : Type ?u.31541} {s : Set α} {t : Set β} (f : α → β → γ),
  Set.Finite s → Set.Finite t → Set.Finite (image2 f s t)
image2 _: ?m.31552 → ?m.31553 → ?m.31554
_ ht: Set.Finite t
ht
#align set.finite.vsub Set.Finite.vsub: ∀ {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s t : Set β}, Set.Finite s → Set.Finite t → Set.Finite (s -ᵥ t)
Set.Finite.vsub

end Vsub

section Cancel

variable [Mul: Type ?u.31648 → Type ?u.31648
Mul α: Type ?u.31592
α] [IsLeftCancelMul: (G : Type ?u.31651) → [inst : Mul G] → Prop
IsLeftCancelMul α: Type ?u.31639
α] [IsRightCancelMul: (G : Type ?u.31618) → [inst : Mul G] → Prop
IsRightCancelMul α: Type ?u.31639
α] {s: Set α
s t: Set α
t : Set: Type ?u.31630 → Type ?u.31630
Set α: Type ?u.31592
α}

@[to_additive: ∀ {α : Type u_1} [inst : Add α] [inst_1 : IsLeftCancelAdd α] [inst_2 : IsRightCancelAdd α] {s t : Set α},
  Set.Infinite (s + t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
to_additive]
theorem infinite_mul: Set.Infinite (s * t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
infinite_mul : (s: Set α
s * t: Set α
t).Infinite: {α : Type ?u.31755} → Set α → Prop
Infinite ↔ s: Set α
s.Infinite: {α : Type ?u.31760} → Set α → Prop
Infinite ∧ t: Set α
t.Nonempty: {α : Type ?u.31764} → Set α → Prop
Nonempty ∨ t: Set α
t.Infinite: {α : Type ?u.31768} → Set α → Prop
Infinite ∧ s: Set α
s.Nonempty: {α : Type ?u.31772} → Set α → Prop
Nonempty :=
  infinite_image2: ∀ {α : Type ?u.31779} {β : Type ?u.31778} {γ : Type ?u.31777} {f : α → β → γ} {s : Set α} {t : Set β},
  (∀ (b : β), b ∈ t → InjOn (fun a => f a b) s) →
    (∀ (a : α), a ∈ s → InjOn (f a) t) →
      (Set.Infinite (image2 f s t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s)
infinite_image2 (fun _: ?m.31809
_ _: ?m.31812
_ => (mul_left_injective: ∀ {G : Type ?u.31814} [inst : Mul G] [inst_1 : IsRightCancelMul G] (a : G), Function.Injective fun x => x * a
mul_left_injective _: ?m.31815
_).injOn: ∀ {α : Type ?u.31851} {β : Type ?u.31852} {f : α → β}, Function.Injective f → ∀ (s : Set α), InjOn f s
injOn _: Set ?m.31863
_) fun _: ?m.31895
_ _: ?m.31898
_ =>
    (mul_right_injective: ∀ {G : Type ?u.31900} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (a : G), Function.Injective ((fun x x_1 => x * x_1) a)
mul_right_injective _: ?m.31901
_).injOn: ∀ {α : Type ?u.31937} {β : Type ?u.31938} {f : α → β}, Function.Injective f → ∀ (s : Set α), InjOn f s
injOn _: Set ?m.31949
_
#align set.infinite_mul Set.infinite_mul: ∀ {α : Type u_1} [inst : Mul α] [inst_1 : IsLeftCancelMul α] [inst_2 : IsRightCancelMul α] {s t : Set α},
  Set.Infinite (s * t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
Set.infinite_mul
#align set.infinite_add Set.infinite_add: ∀ {α : Type u_1} [inst : Add α] [inst_1 : IsLeftCancelAdd α] [inst_2 : IsRightCancelAdd α] {s t : Set α},
  Set.Infinite (s + t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
Set.infinite_add

end Cancel

section Group

variable [Group: Type ?u.32373 → Type ?u.32373
Group α: Type ?u.32364
α] [MulAction: (α : Type ?u.32377) → Type ?u.32376 → [inst : Monoid α] → Type (max?u.32377?u.32376)
MulAction α: Type ?u.32364
α β: Type ?u.32057
β] {a: α
a : α: Type ?u.32054
α} {s: Set β
s : Set: Type ?u.32358 → Type ?u.32358
Set β: Type ?u.32057
β}

@[to_additive: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α} {s : Set β},
  Set.Finite (a +ᵥ s) ↔ Set.Finite s
to_additive (attr := simp)]
theorem finite_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Finite (a • s) ↔ Set.Finite s
finite_smul_set : (a: α
a • s: Set β
s).Finite: {α : Type ?u.33687} → Set α → Prop
Finite ↔ s: Set β
s.Finite: {α : Type ?u.33691} → Set α → Prop
Finite :=
  finite_image_iff: ∀ {α : Type ?u.33697} {β : Type ?u.33696} {s : Set α} {f : α → β}, InjOn f s → (Set.Finite (f '' s) ↔ Set.Finite s)
finite_image_iff <| (MulAction.injective: ∀ {α : Type ?u.33717} {β : Type ?u.33716} [inst : Group α] [inst_1 : MulAction α β] (g : α),
  Function.Injective ((fun x x_1 => x • x_1) g)
MulAction.injective _: ?m.33718
_).injOn: ∀ {α : Type ?u.33768} {β : Type ?u.33769} {f : α → β}, Function.Injective f → ∀ (s : Set α), InjOn f s
injOn _: Set ?m.33780
_
#align set.finite_smul_set Set.finite_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Finite (a • s) ↔ Set.Finite s
Set.finite_smul_set
#align set.finite_vadd_set Set.finite_vadd_set: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α} {s : Set β},
  Set.Finite (a +ᵥ s) ↔ Set.Finite s
Set.finite_vadd_set

@[to_additive: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α} {s : Set β},
  Set.Infinite (a +ᵥ s) ↔ Set.Infinite s
to_additive (attr := simp)]
theorem infinite_smul_set: Set.Infinite (a • s) ↔ Set.Infinite s
infinite_smul_set : (a: α
a • s: Set β
s).Infinite: {α : Type ?u.35263} → Set α → Prop
Infinite ↔ s: Set β
s.Infinite: {α : Type ?u.35267} → Set α → Prop
Infinite :=
  infinite_image_iff: ∀ {α : Type ?u.35273} {β : Type ?u.35272} {s : Set α} {f : α → β}, InjOn f s → (Set.Infinite (f '' s) ↔ Set.Infinite s)
infinite_image_iff <| (MulAction.injective: ∀ {α : Type ?u.35293} {β : Type ?u.35292} [inst : Group α] [inst_1 : MulAction α β] (g : α),
  Function.Injective ((fun x x_1 => x • x_1) g)
MulAction.injective _: ?m.35294
_).injOn: ∀ {α : Type ?u.35344} {β : Type ?u.35345} {f : α → β}, Function.Injective f → ∀ (s : Set α), InjOn f s
injOn _: Set ?m.35356
_
#align set.infinite_smul_set Set.infinite_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Infinite (a • s) ↔ Set.Infinite s
Set.infinite_smul_set
#align set.infinite_vadd_set Set.infinite_vadd_set: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α} {s : Set β},
  Set.Infinite (a +ᵥ s) ↔ Set.Infinite s
Set.infinite_vadd_set

alias finite_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Finite (a • s) ↔ Set.Finite s
finite_smul_set ↔ Finite.of_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Finite (a • s) → Set.Finite s
Finite.of_smul_set _
#align set.finite.of_smul_set Set.Finite.of_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Finite (a • s) → Set.Finite s
Set.Finite.of_smul_set

alias infinite_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Infinite (a • s) ↔ Set.Infinite s
infinite_smul_set ↔ _ Infinite.smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Infinite s → Set.Infinite (a • s)
Infinite.smul_set
#align set.infinite.smul_set Set.Infinite.smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Infinite s → Set.Infinite (a • s)
Set.Infinite.smul_set

attribute [to_additive: ∀ {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α} {s : Set β},
  Set.Infinite s → Set.Infinite (a +ᵥ s)
to_additive] Finite.of_smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Finite (a • s) → Set.Finite s
Finite.of_smul_set Infinite.smul_set: ∀ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst_1 : MulAction α β] {a : α} {s : Set β},
  Set.Infinite s → Set.Infinite (a • s)
Infinite.smul_set

end Group

end Set

open Set

namespace Group

variable {G: Type ?u.35647
G : Type _: Type (?u.35647+1)
Type _} [Group: Type ?u.35626 → Type ?u.35626
Group G: Type ?u.35647
G] [Fintype: Type ?u.35653 → Type ?u.35653
Fintype G: Type ?u.35623
G] (S: Set G
S : Set: Type ?u.35632 → Type ?u.35632
Set G: Type ?u.35623
G)

@[to_additive: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] (S : Set G)
  [inst_2 : (k : ℕ) → DecidablePred fun x => x ∈ k • S] (k : ℕ),
  Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)
to_additive]
theorem card_pow_eq_card_pow_card_univ: ∀ [inst : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k] (k : ℕ),
  Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
card_pow_eq_card_pow_card_univ [∀ k: ℕ
k : ℕ: Type
ℕ, DecidablePred: {α : Sort ?u.35662} → (α → Prop) → Sort (max1?u.35662)
DecidablePred (· ∈ S: Set G
S ^ k: ℕ
k)] :
    ∀ k: ?m.60061
k, Fintype.card: (α : Type ?u.60066) → [inst : Fintype α] → ℕ
Fintype.card G: Type ?u.35647
G ≤ k: ?m.60061
k → Fintype.card: (α : Type ?u.60080) → [inst : Fintype α] → ℕ
Fintype.card (↥(S: Set G
S ^ k: ?m.60061
k)) = Fintype.card: (α : Type ?u.85650) → [inst : Fintype α] → ℕ
Fintype.card (↥(S: Set G
S ^ Fintype.card: (α : Type ?u.85655) → [inst : Fintype α] → ℕ
Fintype.card G: Type ?u.35647
G)) := by
Goals accomplished! 🐙
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)have hG: 0 < Fintype.card G
hG : 0: ?m.111409
0 < Fintype.card: (α : Type ?u.111424) → [inst : Fintype α] → ℕ
Fintype.card G: Type u_1
G := Fintype.card_pos_iff: ∀ {α : Type ?u.111448} [inst : Fintype α], 0 < Fintype.card α ↔ Nonempty α
Fintype.card_pos_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨1: ?m.111542
1⟩F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

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)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)by_cases hS: ?m.112099
hS : S: Set G
S = ∅: ?m.111877
∅F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

pos∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

neg∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)·F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

pos∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

pos∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

neg∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)refine' fun k: ?m.112109
k hk: ?m.112112
hk ↦ Fintype.card_congr: ∀ {α : Type ?u.112114} {β : Type ?u.112115} [inst : Fintype α] [inst_1 : Fintype β],
  α ≃ β → Fintype.card α = Fintype.card β
Fintype.card_congr _: ?m.112116 ≃ ?m.112117
_F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑(S ^ k) ≃ ↑(S ^ Fintype.card G)
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

pos∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)rw [F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑(S ^ k) ≃ ↑(S ^ Fintype.card G)hS: ?m.112092
hS,F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑(∅ ^ k) ≃ ↑(∅ ^ Fintype.card G) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑(S ^ k) ≃ ↑(S ^ Fintype.card G)empty_pow: ∀ {α : Type ?u.112826} [inst : Monoid α] {n : ℕ}, n ≠ 0 → ∅ ^ n = ∅
empty_pow (ne_of_gt: ∀ {α : Type ?u.112830} [inst : Preorder α] {a b : α}, b < a → a ≠ b
ne_of_gt (lt_of_lt_of_le: ∀ {α : Type ?u.112863} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
lt_of_lt_of_le hG: 0 < Fintype.card G
hG hk: ?m.112112
hk)),F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑∅ ≃ ↑(∅ ^ Fintype.card G) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑(S ^ k) ≃ ↑(S ^ Fintype.card G)empty_pow: ∀ {α : Type ?u.113348} [inst : Monoid α] {n : ℕ}, n ≠ 0 → ∅ ^ n = ∅
empty_pow (ne_of_gt: ∀ {α : Type ?u.113352} [inst : Preorder α] {a b : α}, b < a → a ≠ b
ne_of_gt hG: 0 < Fintype.card G
hG)F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: S = ∅

k: ℕ

hk: Fintype.card G ≤ k

pos↑∅ ≃ ↑∅]
Goals accomplished! 🐙
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)obtain ⟨a, ha⟩: Set.Nonempty S
⟨a: G
a⟨a, ha⟩: Set.Nonempty S
, ha: a ∈ S
ha⟨a, ha⟩: Set.Nonempty S
⟩ := Set.nonempty_iff_ne_empty: ∀ {α : Type ?u.113442} {s : Set α}, Set.Nonempty s ↔ s ≠ ∅
Set.nonempty_iff_ne_empty.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hS: ?m.112099
hSF: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

neg.intro∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)have key: ∀ (a : G) (s : Set G) (t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
key : ∀ (a: ?m.113496
a) (s: Set G
s t: Set G
t : Set: Type ?u.113499 → Type ?u.113499
Set G: Type u_1
G) [Fintype: Type ?u.113505 → Type ?u.113505
Fintype s: Set G
s] [Fintype: Type ?u.113635 → Type ?u.113635
Fintype t: Set G
t],
      (∀ b: G
b : G: Type u_1
G, b: G
b ∈ s: Set G
s → a: ?m.113496
a * b: G
b ∈ t: Set G
t) → Fintype.card: (α : Type ?u.114510) → [inst : Fintype α] → ℕ
Fintype.card s: Set G
s ≤ Fintype.card: (α : Type ?u.114675) → [inst : Fintype α] → ℕ
Fintype.card t: Set G
t := F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

neg.intro∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)by
Goals accomplished! 🐙
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑trefine' fun a: ?m.114855
a s: ?m.114858
s t: ?m.114861
t _: ?m.114864
_ _: ?m.114867
_ h: ?m.114870
h ↦ Fintype.card_le_of_injective: ∀ {α : Type ?u.114876} {β : Type ?u.114877} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Injective f → Fintype.card α ≤ Fintype.card β
Fintype.card_le_of_injective (fun ⟨b: G
b, hb: b ∈ s
hb⟩ ↦ ⟨a: ?m.114855
a * b: G
b, h: ?m.114870
h b: G
b hb: b ∈ s
hb⟩) _: Function.Injective fun x =>
  match x with
  | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) }
_F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a✝: G

ha: a✝ ∈ S

a: G

s, t: Set G

x✝¹: Fintype ↑s

x✝: Fintype ↑t

h: ∀ (b : G), b ∈ s → a * b ∈ t

Function.Injective fun x =>
  match x with
  | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) }
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑trintro ⟨b, hb⟩: ↑s
⟨b: G
b⟨b, hb⟩: ↑s
, hb: b ∈ s
hb⟨b, hb⟩: ↑s
⟩ ⟨c, hc⟩: ↑s
⟨c: G
c⟨c, hc⟩: ↑s
, hc: c ∈ s
hc⟨c, hc⟩: ↑s
⟩ hbc: (fun x =>
      match x with
      | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
    { val := b, property := hb } =   (fun x =>
      match x with
      | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
    { val := c, property := hc }
hbcF: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a✝: G

ha: a✝ ∈ S

a: G

s, t: Set G

x✝¹: Fintype ↑s

x✝: Fintype ↑t

h: ∀ (b : G), b ∈ s → a * b ∈ t

b: G

hb: b ∈ s

c: G

hc: c ∈ s

hbc: (fun x =>
      match x with
      | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
    { val := b, property := hb } =   (fun x =>
      match x with
      | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
    { val := c, property := hc }

mk.mk{ val := b, property := hb } = { val := c, property := hc }
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑texact Subtype.ext: ∀ {α : Sort ?u.115966} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext (mul_left_cancel: ∀ {G : Type ?u.115980} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
mul_left_cancel (Subtype.ext_iff: ∀ {α : Sort ?u.116024} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
Subtype.ext_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp hbc: (fun x =>
      match x with
      | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
    { val := b, property := hb } =   (fun x =>
      match x with
      | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
    { val := c, property := hc }
hbc))
Goals accomplished! 🐙
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)have mono: Monotone fun n => Fintype.card ↑(S ^ n)
mono : Monotone: {α : Type ?u.116520} → {β : Type ?u.116519} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone (fun n: ?m.116577
n ↦ Fintype.card: (α : Type ?u.116579) → [inst : Fintype α] → ℕ
Fintype.card (↥(S: Set G
S ^ n: ?m.116577
n)) : ℕ: Type
ℕ → ℕ: Type
ℕ) :=
    monotone_nat_of_le_succ: ∀ {α : Type ?u.141260} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n ≤ f (n + 1)) → Monotone f
monotone_nat_of_le_succ fun n: ?m.141322
n ↦ key: ∀ (a : G) (s : Set G) (t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
key a: G
a _: Set G
_ _: Set G
_ fun b: ?m.141424
b hb: ?m.141427
hb ↦ Set.mul_mem_mul: ∀ {α : Type ?u.141449} [inst : Mul α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a * b ∈ s * t
Set.mul_mem_mul ha: a ∈ S
ha hb: ?m.141427
hbF: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

neg.intro∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)refine' card_pow_eq_card_pow_card_univ_aux: ∀ {f : ℕ → ℕ},
  Monotone f →
    ∀ {B : ℕ},
      (∀ (n : ℕ), f n ≤ B) → (∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)) → ∀ (k : ℕ), B ≤ k → f k = f B
card_pow_eq_card_pow_card_univ_aux mono: Monotone fun n => Fintype.card ↑(S ^ n)
mono (fun n: ?m.142349
n ↦ set_fintype_card_le_univ: ∀ {α : Type ?u.142351} [inst : Fintype α] (s : Set α) [inst_1 : Fintype ↑s], Fintype.card ↑s ≤ Fintype.card α
set_fintype_card_le_univ (S: Set G
S ^ n: ?m.142349
n))
    fun n: ?m.143033
n h: ?m.143036
h ↦ le_antisymm: ∀ {α : Type ?u.143038} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (mono: Monotone fun n => Fintype.card ↑(S ^ n)
mono (n: ?m.143033
n + 1: ?m.143172
1).le_succ: ∀ (n : ℕ), n ≤ Nat.succ n
le_succ) (key: ∀ (a : G) (s : Set G) (t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
key a: G
a⁻¹ (S: Set G
S ^ (n: ?m.143033
n + 2: ?m.143376
2)) (S: Set G
S ^ (n: ?m.143033
n + 1: ?m.167152
1)) _: ∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
_)F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)replace h₂: {a} * S ^ n = S ^ (n + 1)
h₂ : {a: G
a} * S: Set G
S ^ n: ?m.143033
n = S: Set G
S ^ (n: ?m.143033
n + 1: ?m.201304
1)F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1)
F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)·F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1)
F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)have : Fintype: Type ?u.226255 → Type ?u.226255
Fintype (Set.singleton: {α : Type ?u.226259} → α → Set α
Set.singleton a: G
a * S: Set G
S ^ n: ?m.143033
n) := F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1)by
Goals accomplished! 🐙
      F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

Fintype ↑(Set.singleton a * S ^ n)classical!F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

em✝: (a : Prop) → Decidable a

Fintype ↑(Set.singleton a * S ^ n)
      F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

Fintype ↑(Set.singleton a * S ^ n)apply fintypeMul: {α : Type ?u.243464} →
  [inst : Mul α] →
    [inst_1 : DecidableEq α] → (s t : Set α) → [inst_2 : Fintype ↑s] → [inst_3 : Fintype ↑t] → Fintype ↑(s * t)
fintypeMul
Goals accomplished! 🐙
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1)refine' Set.eq_of_subset_of_card_le: ∀ {α : Type ?u.244157} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  s ⊆ t → Fintype.card ↑t ≤ Fintype.card ↑s → s = t
Set.eq_of_subset_of_card_le _: ?m.244159 ⊆ ?m.244160
_ (le_trans: ∀ {α : Type ?u.244257} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans (ge_of_eq: ∀ {α : Type ?u.244356} [inst : Preorder α] {a b : α}, a = b → a ≥ b
ge_of_eq h: ?m.143036
h) _: ?m.244261 ≤ ?m.244262
_)F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_1{a} * S ^ n ⊆ S ^ (n + 1)
F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_2Fintype.card ↑(S ^ n) ≤ Fintype.card ↑({a} * S ^ n)
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1)·F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_1{a} * S ^ n ⊆ S ^ (n + 1) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_1{a} * S ^ n ⊆ S ^ (n + 1)
F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_2Fintype.card ↑(S ^ n) ≤ Fintype.card ↑({a} * S ^ n)exact mul_subset_mul: ∀ {α : Type ?u.244669} [inst : Mul α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂
mul_subset_mul (Set.singleton_subset_iff: ∀ {α : Type ?u.244724} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ s
Set.singleton_subset_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ha: a ∈ S
ha) Set.Subset.rfl: ∀ {α : Type ?u.244737} {s : Set α}, s ⊆ s
Set.Subset.rfl
Goals accomplished! 🐙
    F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂{a} * S ^ n = S ^ (n + 1)·F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_2Fintype.card ↑(S ^ n) ≤ Fintype.card ↑({a} * S ^ n) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

this: Fintype ↑(Set.singleton a * S ^ n)

h₂.refine'_2Fintype.card ↑(S ^ n) ≤ Fintype.card ↑({a} * S ^ n)convert key: ∀ (a : G) (s : Set G) (t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
key a: G
a (S: Set G
S ^ n: ?m.143033
n) ({a: G
a} * S: Set G
S ^ n: ?m.143033
n) fun b: ?m.293674
b hb: ?m.293677
hb ↦ Set.mul_mem_mul: ∀ {α : Type ?u.293679} [inst : Mul α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a * b ∈ s * t
Set.mul_mem_mul (Set.mem_singleton: ∀ {α : Type ?u.293721} (a : α), a ∈ {a}
Set.mem_singleton a: G
a) hb: ?m.293677
hb
Goals accomplished! 🐙
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)rw [F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)pow_succ': ∀ {M : Type ?u.294135} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
pow_succ',F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 1) * S → a⁻¹ * b ∈ S ^ (n + 1) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)← h₂: {a} * S ^ n = S ^ (n + 1)
h₂,F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ {a} * S ^ n * S → a⁻¹ * b ∈ {a} * S ^ n F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)mul_assoc: ∀ {G : Type ?u.294498} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ {a} * (S ^ n * S) → a⁻¹ * b ∈ {a} * S ^ n F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)← pow_succ': ∀ {M : Type ?u.294834} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
pow_succ',F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ {a} * S ^ (n + 1) → a⁻¹ * b ∈ {a} * S ^ n F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)h₂: {a} * S ^ n = S ^ (n + 1)
h₂F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ {a} * S ^ (n + 1) → a⁻¹ * b ∈ S ^ (n + 1)]F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

neg.intro∀ (b : G), b ∈ {a} * S ^ (n + 1) → a⁻¹ * b ∈ S ^ (n + 1)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)rintro _: G
_ ⟨b, c, hb, hc, rfl⟩: ∃ b_1, b ∈ {a} ∧ b_1 ∈ S ^ (n + 1) ∧ (fun x x_1 => x * x_1) b b_1 = b✝
⟨b: G
b⟨b, c, hb, hc, rfl⟩: ∃ b_1, b ∈ {a} ∧ b_1 ∈ S ^ (n + 1) ∧ (fun x x_1 => x * x_1) b b_1 = b✝
, c: G
c⟨b, c, hb, hc, rfl⟩: ∃ b_1, b ∈ {a} ∧ b_1 ∈ S ^ (n + 1) ∧ (fun x x_1 => x * x_1) b b_1 = b✝
, hb: b ∈ {a}
hb⟨b, c, hb, hc, rfl⟩: ∃ b_1, b ∈ {a} ∧ b_1 ∈ S ^ (n + 1) ∧ (fun x x_1 => x * x_1) b b_1 = b✝
, hc: c ∈ S ^ (n + 1)
hc⟨b, c, hb, hc, rfl⟩: ∃ b_1, b ∈ {a} ∧ b_1 ∈ S ^ (n + 1) ∧ (fun x x_1 => x * x_1) b b_1 = b✝
, rfl: (fun x x_1 => x * x_1) b c = b✝
rfl⟨b, c, hb, hc, rfl⟩: ∃ b_1, b ∈ {a} ∧ b_1 ∈ S ^ (n + 1) ∧ (fun x x_1 => x * x_1) b b_1 = b✝
⟩F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

b, c: G

hb: b ∈ {a}

hc: c ∈ S ^ (n + 1)

neg.intro.intro.intro.intro.introa⁻¹ * (fun x x_1 => x * x_1) b c ∈ S ^ (n + 1)
  F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)rwa [F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

b, c: G

hb: b ∈ {a}

hc: c ∈ S ^ (n + 1)

neg.intro.intro.intro.intro.introa⁻¹ * (fun x x_1 => x * x_1) b c ∈ S ^ (n + 1)Set.mem_singleton_iff: ∀ {α : Type ?u.295085} {a b : α}, a ∈ {b} ↔ a = b
Set.mem_singleton_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp hb: b ∈ {a}
hb,F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

b, c: G

hb: b ∈ {a}

hc: c ∈ S ^ (n + 1)

neg.intro.intro.intro.intro.introa⁻¹ * (fun x x_1 => x * x_1) a c ∈ S ^ (n + 1) F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

b, c: G

hb: b ∈ {a}

hc: c ∈ S ^ (n + 1)

neg.intro.intro.intro.intro.introa⁻¹ * (fun x x_1 => x * x_1) b c ∈ S ^ (n + 1)inv_mul_cancel_left: ∀ {G : Type ?u.295103} [inst : Group G] (a b : G), a⁻¹ * (a * b) = b
inv_mul_cancel_leftF: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

b, c: G

hb: b ∈ {a}

hc: c ∈ S ^ (n + 1)

neg.intro.intro.intro.intro.introc ∈ S ^ (n + 1)]F: Type ?u.35635

α: Type ?u.35638

β: Type ?u.35641

γ: Type ?u.35644

G: Type u_1

inst✝²: Group G

inst✝¹: Fintype G

S: Set G

inst✝: (k : ℕ) → DecidablePred fun x => x ∈ S ^ k

hG: 0 < Fintype.card G

hS: ¬S = ∅

a: G

ha: a ∈ S

key: ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
  (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

mono: Monotone fun n => Fintype.card ↑(S ^ n)

n: ℕ

h: Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))

h₂: {a} * S ^ n = S ^ (n + 1)

b, c: G

hb: b ∈ {a}

hc: c ∈ S ^ (n + 1)

neg.intro.intro.intro.intro.introc ∈ S ^ (n + 1)
#align group.card_pow_eq_card_pow_card_univ Group.card_pow_eq_card_pow_card_univ: ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] (S : Set G) [inst_2 : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k]
  (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
Group.card_pow_eq_card_pow_card_univ
#align add_group.card_nsmul_eq_card_nsmul_card_univ AddGroup.card_nsmul_eq_card_nsmul_card_univ: ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] (S : Set G)
  [inst_2 : (k : ℕ) → DecidablePred fun x => x ∈ k • S] (k : ℕ),
  Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)
AddGroup.card_nsmul_eq_card_nsmul_card_univ

end Group