[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
⊢ DecidablePred fun x => x ∈ s ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
⊢ DecidablePred fun x => x ∈ s ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, mem_one]
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
⊢ DecidablePred fun x => x = 1
[PROOFSTEP]
infer_instance
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : DecidablePred fun x => x ∈ s ^ n
⊢ DecidablePred fun x => x ∈ s ^ Nat.succ n
[PROOFSTEP]
letI := ih
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : DecidablePred fun x => x ∈ s ^ n
this : DecidablePred fun x => x ∈ s ^ n := ih
⊢ DecidablePred fun x => x ∈ s ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : DecidablePred fun x => x ∈ s ^ n
this : DecidablePred fun x => x ∈ s ^ n := ih
⊢ DecidablePred fun x => x ∈ s * s ^ n
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
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)
[PROOFSTEP]
have hG : 0 < Fintype.card G := Fintype.card_pos_iff.mpr ⟨1⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
by_cases hS : S = ∅
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : S = ∅
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
refine' fun k hk ↦ Fintype.card_congr _
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : S = ∅
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(S ^ k) ≃ ↑(S ^ Fintype.card G)
[PROOFSTEP]
rw [hS, empty_pow (ne_of_gt (lt_of_lt_of_le hG hk)), empty_pow (ne_of_gt hG)]
[GOAL]
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 hS
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
have key :
  ∀ (a) (s t : Set G) [Fintype s] [Fintype t], (∀ b : G, b ∈ s → a * b ∈ t) → Fintype.card s ≤ Fintype.card t :=
  by
  refine' fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨a * b, h b hb⟩) _
  rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
  exact Subtype.ext (mul_left_cancel (Subtype.ext_iff.mp hbc))
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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 ↑t
[PROOFSTEP]
refine' fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨a * b, h b hb⟩) _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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) }
[PROOFSTEP]
rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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 }
⊢ { val := b, property := hb } = { val := c, property := hc }
[PROOFSTEP]
exact Subtype.ext (mul_left_cancel (Subtype.ext_iff.mp hbc))
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
  monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul ha hb
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
refine'
  card_pow_eq_card_pow_card_univ_aux mono (fun n ↦ set_fintype_card_le_univ (S ^ n)) fun n h ↦
    le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) _)
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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))
⊢ ∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
[PROOFSTEP]
replace h₂ : { a } * S ^ n = S ^ (n + 1)
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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))
⊢ {a} * S ^ n = S ^ (n + 1)
[PROOFSTEP]
have : Fintype (Set.singleton a * S ^ n) := by
  classical!
  apply fintypeMul
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
[PROOFSTEP]
classical!
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
[PROOFSTEP]
apply fintypeMul
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
⊢ {a} * S ^ n = S ^ (n + 1)
[PROOFSTEP]
refine' Set.eq_of_subset_of_card_le _ (le_trans (ge_of_eq h) _)
[GOAL]
case h₂.refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
⊢ {a} * S ^ n ⊆ S ^ (n + 1)
[PROOFSTEP]
exact mul_subset_mul (Set.singleton_subset_iff.mpr ha) Set.Subset.rfl
[GOAL]
case h₂.refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑({a} * S ^ n)
[PROOFSTEP]
convert key a (S ^ n) ({ a } * S ^ n) fun b hb ↦ Set.mul_mem_mul (Set.mem_singleton a) hb
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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 : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
[PROOFSTEP]
rw [pow_succ', ← h₂, mul_assoc, ← pow_succ', h₂]
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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 : G), b ∈ {a} * S ^ (n + 1) → a⁻¹ * b ∈ S ^ (n + 1)
[PROOFSTEP]
rintro _ ⟨b, c, hb, hc, rfl⟩
[GOAL]
case neg.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
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)
⊢ a⁻¹ * (fun x x_1 => x * x_1) b c ∈ S ^ (n + 1)
[PROOFSTEP]
rwa [Set.mem_singleton_iff.mp hb, inv_mul_cancel_left]
