Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
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 sSet.Finite (-s)
to_additive
] theorem
Finite.inv: Set.Finite sSet.Finite s⁻¹
Finite.inv
(hs :
s: Set α
s
.
Finite: {α : Type ?u.180} → Set αProp
Finite
) :
s: Set α
s
⁻¹.
Finite: {α : Type ?u.359} → Set αProp
Finite
:= hs.
preimage: ∀ {α : Type ?u.366} {β : Type ?u.365} {s : Set β} {f : αβ}, InjOn f (f ⁻¹' s)Set.Finite sSet.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 sSet.Finite s⁻¹
Set.Finite.inv
#align set.finite.neg
Set.Finite.neg: ∀ {α : Type u_1} [inst : InvolutiveNeg α] {s : Set α}, Set.Finite sSet.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 sSet.Finite tSet.Finite (s + t)
to_additive
] theorem
Finite.mul: ∀ {α : Type u_1} [inst : Mul α] {s t : Set α}, Set.Finite sSet.Finite tSet.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 sSet.Finite tSet.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 sSet.Finite tSet.Finite (s * t)
Set.Finite.mul
#align set.finite.add
Set.Finite.add: ∀ {α : Type u_1} [inst : Add α] {s t : Set α}, Set.Finite sSet.Finite tSet.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
) :=

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


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


succ
DecidablePred 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


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


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


succ
DecidablePred 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


zero
DecidablePred 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


zero

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


succ
DecidablePred 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


succ
DecidablePred 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

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


succ
DecidablePred 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


succ
DecidablePred 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

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


succ
DecidablePred 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

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


succ
DecidablePred 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


succ
DecidablePred 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


succ
DecidablePred fun x => x s ^ Nat.succ n

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 sSet.Finite tSet.Finite (s +ᵥ t)
to_additive
] theorem
Finite.smul: ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s : Set α} {t : Set β}, Set.Finite sSet.Finite tSet.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 sSet.Finite tSet.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 sSet.Finite tSet.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 sSet.Finite tSet.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 sSet.Finite (a +ᵥ s)
to_additive
] theorem
Finite.smul_set: Set.Finite sSet.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 sSet.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 sSet.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 sSet.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 sSet.Finite tSet.Finite (s -ᵥ t)
Finite.vsub
(hs :
s: Set β
s
.
Finite: {α : Type ?u.31498} → Set αProp
Finite
) (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.
image2: ∀ {α : Type ?u.31543} {β : Type ?u.31542} {γ : Type ?u.31541} {s : Set α} {t : Set β} (f : αβγ), Set.Finite sSet.Finite tSet.Finite (image2 f s t)
image2
_: ?m.31552?m.31553?m.31554
_
ht #align set.finite.vsub
Set.Finite.vsub: ∀ {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s t : Set β}, Set.Finite sSet.Finite tSet.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 : (
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 tInjOn (fun a => f a b) s) → (∀ (a : α), a sInjOn (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 sSet.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 sSet.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 sSet.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 sSet.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 kFintype.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 kFintype.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
)) :=

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 kFintype.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


∀ (k : ), Fintype.card G kFintype.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 kFintype.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 kFintype.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 kFintype.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 kFintype.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 kFintype.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 kFintype.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 kFintype.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 =

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 kFintype.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 =

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 =

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)
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
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 =

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 kFintype.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


neg.intro
∀ (k : ), Fintype.card G kFintype.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 kFintype.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


neg.intro
∀ (k : ), Fintype.card G kFintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

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 sa * b t) → Fintype.card s Fintype.card 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 sa * 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 sa * b t) → Fintype.card s Fintype.card 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 sa * 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 sa * b t) → Fintype.card s Fintype.card t

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 kFintype.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 sa * b t) → Fintype.card s Fintype.card t

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


neg.intro
∀ (k : ), Fintype.card G kFintype.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 kFintype.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 sa * 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 kFintype.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 sa * 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 sa * 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 kFintype.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 sa * 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 sa * 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 sa * 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

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 sa * 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)

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 sa * 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))


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 sa * 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


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 sa * 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))



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 sa * 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 sa * 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 sa * 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'_2
Fintype.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 sa * 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 sa * 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 sa * 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 sa * 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'_2
Fintype.card ↑(S ^ n) Fintype.card ↑({a} * S ^ n)

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 sa * 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 sa * 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'_2
Fintype.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 sa * 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'_2
Fintype.card ↑(S ^ n) Fintype.card ↑({a} * S ^ n)

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 kFintype.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 sa * 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

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 sa * 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) * Sa⁻¹ * 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 sa * 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

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 sa * 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 * Sa⁻¹ * 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 sa * 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

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 sa * 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 sa * 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

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 sa * 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 sa * 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

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 sa * 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 sa * 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 kFintype.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 sa * 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.intro
a⁻¹ * (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 kFintype.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 sa * 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.intro
a⁻¹ * (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

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 sa * 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.intro
a⁻¹ * (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 sa * 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.intro
a⁻¹ * (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

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 sa * 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.intro
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 sa * 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.intro
c 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 kFintype.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 kFintype.card ↑(k S) = Fintype.card ↑(Fintype.card G S)
AddGroup.card_nsmul_eq_card_nsmul_card_univ
end Group