awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
hG : 0 < Fintype.card G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k
k : ℕ
hk : Fintype.card G ≤ k
inl : (↑∅ : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
inl₁ inl₂ : (↑∅ : Type u_5) ≃ (↑∅ : Type u_5)
⊢ (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)

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

Premises used: Set.empty_pow, ne_of_gt, LT.lt.ne', LT.lt.trans_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)

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

Premises used: Fintype.card_le_of_injective, HMul.hMul, Set.Elem, _private.0.Group.card_pow_eq_card_pow_card_univ.match_1, Subtype.mk
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
refine :
  ∀ (a : G) (s t : Set G) (x : Fintype (↑s : Type u_5)) (x : Fintype (↑t : Type u_5)) (h : ∀ b ∈ s, b * a ∈ t),
    Function.Injective (β := (↑t : Type u_5)) fun (x : (↑s : Type u_5)) ↦
      match (motive := (↑s : Type u_5) → (↑t : Type u_5)) x with
      | ⟨b, hb⟩ => Subtype.mk (p := fun (x : G) ↦ x ∈ t) (b * a) ⋯
⊢ ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)

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

Premises used: Fintype.card_le_of_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a_1 : G
ha : a_1 ∈ S
a : G
s t : Set G
x : Fintype (↑s : Type u_5)
x_1 : Fintype (↑t : Type u_5)
h : ∀ b ∈ s, b * a ∈ t
b : G
hb : b ∈ s
c : G
hc : c ∈ s
hbc :
  Eq.{u_5 + 1} (α := (↑t : Type u_5))
    ((fun (x : (↑s : Type u_5)) ↦
        (match (motive := (↑s : Type u_5) → (↑t : Type u_5)) x with
          | ⟨b, hb⟩ => Subtype.mk (p := fun (x : G) ↦ x ∈ t) (b * a) ⋯ :
          (↑t : Type u_5)))
      (Subtype.mk (p := fun (x : G) ↦ x ∈ s) b hb))
    ((fun (x : (↑s : Type u_5)) ↦
        (match (motive := (↑s : Type u_5) → (↑t : Type u_5)) x with
          | ⟨b, hb⟩ => Subtype.mk (p := fun (x : G) ↦ x ∈ t) (b * a) ⋯ :
          (↑t : Type u_5)))
      (Subtype.mk (p := fun (x : G) ↦ x ∈ s) c hc))
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ s) b hb = Subtype.mk (p := fun (x : G) ↦ x ∈ s) c hc

Tactic:
Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))

Premises used: Subtype.ext_iff, Iff.mp, mul_right_cancel, Subtype.ext
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a_1 : G
ha : a_1 ∈ S
a : G
s t : Set G
x : Fintype (↑s : Type u_5)
x_1 : Fintype (↑t : Type u_5)
h : ∀ b ∈ s, b * a ∈ t
b : G
hb : b ∈ s
c : G
hc : c ∈ s
hbc :
  Eq.{u_5 + 1} (α := (↑t : Type u_5))
    ((fun (x : (↑s : Type u_5)) ↦
        (match (motive := (↑s : Type u_5) → (↑t : Type u_5)) x with
          | ⟨b, hb⟩ => Subtype.mk (p := fun (x : G) ↦ x ∈ t) (b * a) ⋯ :
          (↑t : Type u_5)))
      (Subtype.mk (p := fun (x : G) ↦ x ∈ s) b hb))
    ((fun (x : (↑s : Type u_5)) ↦
        (match (motive := (↑s : Type u_5) → (↑t : Type u_5)) x with
          | ⟨b, hb⟩ => Subtype.mk (p := fun (x : G) ↦ x ∈ t) (b * a) ⋯ :
          (↑t : Type u_5)))
      (Subtype.mk (p := fun (x : G) ↦ x ∈ s) c hc))
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ s) b hb = Subtype.mk (p := fun (x : G) ↦ x ∈ s) c hc

Tactic:
exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))

Premises used: mul_right_cancel, Subtype.ext
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)

Tactic:
have key : ∀ (a) (s t : Set G) [Fintype s] [Fintype t],
      (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t := by
    refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
    rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
    exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
⊢ Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)

Tactic:
have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
    monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul hb ha
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)

Tactic:
fun _ ↦ Nat.stabilises_of_monotone 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)) ?_)

Premises used: Nat.le_succ, le_antisymm, Inv.inv, HPow.hPow, HAdd.hAdd, Nat.stabilises_of_monotone, set_fintype_card_le_univ, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
inr :
  ∀ (x n : ℕ) (h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)),
    ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(S ^ k) : Type u_5) = Fintype.card.{u_5} (↑(S ^ Fintype.card G) : Type u_5)

Tactic:
refine fun _ ↦ Nat.stabilises_of_monotone 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)) ?_)

Premises used: Nat.le_succ, le_antisymm, Inv.inv, HPow.hPow, HAdd.hAdd, Nat.stabilises_of_monotone, set_fintype_card_le_univ, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
⊢ Fintype (↑(S ^ n * Set.singleton a) : Type u_5)

Tactic:
apply fintypeMul

Premises used: Set.fintypeMul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
⊢ Fintype (↑(S ^ n * Set.singleton a) : Type u_5)

Tactic:
classical
      apply fintypeMul

Premises used: Set.fintypeMul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
have : ∀ (this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)), S ^ n * {a} = S ^ (n + 1)
⊢ S ^ n * {a} = S ^ (n + 1)

Tactic:
have : Fintype (S ^ n * Set.singleton a) := by
      classical
      apply fintypeMul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
⊢ S ^ n * {a} = S ^ (n + 1)

Tactic:
Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)

Premises used: ge_of_eq, Set.eq_of_subset_of_card_le, le_trans
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
refine_1 : S ^ n * {a} ⊆ S ^ (n + 1)
refine_2 : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) ≤ Fintype.card.{u_5} (↑(S ^ n * {a}) : Type u_5)
⊢ S ^ n * {a} = S ^ (n + 1)

Tactic:
refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)

Premises used: ge_of_eq, Set.eq_of_subset_of_card_le, le_trans
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

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

Premises used: Iff.mpr, Set.singleton_subset_iff, setOf, npowRec, Set.Subset.rfl, Set.image2, Set.mul_subset_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

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

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Subset.rfl, Set.mul_subset_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
⊢ Fintype.card.{u_5} (↑(S ^ n) : Type u_5) ≤ Fintype.card.{u_5} (↑(S ^ n * {a}) : Type u_5)

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

Premises used: Set.mem_singleton, HMul.hMul, HPow.hPow, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
this : Fintype (↑(S ^ n * Set.singleton a) : Type u_5)
⊢ Fintype.card.{u_5} (↑(S ^ n) : Type u_5) ≤ Fintype.card.{u_5} (↑(S ^ n * {a}) : Type u_5)

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

Premises used: HMul.hMul, HPow.hPow, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
⊢ S ^ n * {a} = S ^ (n + 1)

Tactic:
replace h₂ : S ^ n * {a} = S ^ (n + 1) := by
    have : Fintype (S ^ n * Set.singleton a) := by
      classical
      apply fintypeMul
    refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
    · exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)
    · convert! key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
h₂ : S ^ n * {a} = S ^ (n + 1)
inr : ∀ ⦃x : G⦄, x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)
⊢ ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)

Tactic:
rw [pow_succ', ← h₂, ← mul_assoc, ← pow_succ', h₂, mul_singleton, forall_mem_image]

Premises used: mul_assoc, Set.mul_singleton, pow_succ', Set.forall_mem_image
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
G : Type u_5
inst : Group G
inst_1 : Fintype G
S : Set G
inst_2 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst_3 : Fintype (↑s : Type u_5)] [inst_4 : Fintype (↑t : Type u_5)],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card.{u_5} (↑s : Type u_5) ≤ Fintype.card.{u_5} (↑t : Type u_5)
mono : Monotone (β := ℕ) fun (n : ℕ) ↦ Fintype.card.{u_5} (↑(S ^ n) : Type u_5)
x_1 n : ℕ
h : Fintype.card.{u_5} (↑(S ^ n) : Type u_5) = Fintype.card.{u_5} (↑(S ^ (n + 1)) : Type u_5)
h₂ : S ^ n * {a} = S ^ (n + 1)
x : G
hx : x ∈ S ^ (n + 1)
inr inr₁ inr₂ inr₃ : x ∈ S ^ (n + 1)
⊢ x * a * a⁻¹ ∈ S ^ (n + 1)

Tactic:
rwa [mul_inv_cancel_right]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Inv α
s : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), s i)⁻¹ (⋂ (i : ι), (s i)⁻¹)

Tactic:
preimage_iInter

Premises used: Set.preimage_iInter
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Inv α
S : Set (Set α)
⊢ (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹

Tactic:
preimage_sInter

Premises used: Set.preimage_sInter
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Inv α
s : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i)⁻¹ (⋃ (i : ι), (s i)⁻¹)

Tactic:
preimage_iUnion

Premises used: Set.preimage_iUnion
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Inv α
S : Set (Set α)
⊢ (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹

Tactic:
preimage_sUnion

Premises used: Set.preimage_sUnion
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ ⋃ a ∈ s, (fun (x : α) ↦ a * x) '' t = s * t

Tactic:
iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ ⋃ a ∈ t, (fun (x : α) ↦ x * a) '' s = s * t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Mul α
s : ι → Set α
t : Set α
⊢ (⋃ (i : ι), s i) * t = ⋃ (i : ι), s i * t

Tactic:
image2_iUnion_left ..

Premises used: Set.image2_iUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Mul α
s : Set α
t : ι → Set α
⊢ s * ⋃ (i : ι), t i = ⋃ (i : ι), s * t i

Tactic:
image2_iUnion_right ..

Premises used: Set.image2_iUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Mul α
S : Set (Set α)
t : Set α
⊢ ⋃₀ S * t = ⋃ s ∈ S, s * t

Tactic:
image2_sUnion_left ..

Premises used: Set.image2_sUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Mul α
s : Set α
T : Set (Set α)
⊢ s * ⋃₀ T = ⋃ t ∈ T, s * t

Tactic:
image2_sUnion_right ..

Premises used: Set.image2_sUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Mul α
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ (i : ι), ⋃ (j : κ i), s i j) * t = ⋃ (i : ι), ⋃ (j : κ i), s i j * t

Tactic:
image2_iUnion₂_left ..

Premises used: Set.image2_iUnion₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Mul α
s : Set α
t : (i : ι) → κ i → Set α
⊢ s * ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s * t i j

Tactic:
image2_iUnion₂_right ..

Premises used: Set.image2_iUnion₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Mul α
s : ι → Set α
t : Set α
⊢ (⋂ (i : ι), s i) * t ⊆ ⋂ (i : ι), s i * t

Tactic:
Set.image2_iInter_subset_left ..

Premises used: Set.image2_iInter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Mul α
s : Set α
t : ι → Set α
⊢ s * ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s * t i

Tactic:
image2_iInter_subset_right ..

Premises used: Set.image2_iInter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Mul α
s : Set α
T : Set (Set α)
⊢ s * ⋂₀ T ⊆ ⋂ t ∈ T, s * t

Tactic:
image2_sInter_right_subset s T (fun a b => a * b)

Premises used: HMul.hMul, Set.image2_sInter_right_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Mul α
S : Set (Set α)
t : Set α
⊢ ⋂₀ S * t ⊆ ⋂ s ∈ S, s * t

Tactic:
image2_sInter_left_subset S t (fun a b => a * b)

Premises used: HMul.hMul, Set.image2_sInter_left_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Mul α
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι), ⋂ (j : κ i), s i j) * t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j * t

Tactic:
image2_iInter₂_subset_left ..

Premises used: Set.image2_iInter₂_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Mul α
s : Set α
t : (i : ι) → κ i → Set α
⊢ s * ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s * t i j

Tactic:
image2_iInter₂_subset_right ..

Premises used: Set.image2_iInter₂_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ ⋃ a ∈ s, (fun (x : α) ↦ a / x) '' t = s / t

Tactic:
iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ ⋃ a ∈ t, (fun (x : α) ↦ x / a) '' s = s / t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Div α
s : ι → Set α
t : Set α
⊢ (⋃ (i : ι), s i) / t = ⋃ (i : ι), s i / t

Tactic:
image2_iUnion_left ..

Premises used: Set.image2_iUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
inst : Div α
s : Set α
t : ι → Set α
⊢ s / ⋃ (i : ι), t i = ⋃ (i : ι), s / t i

Tactic:
image2_iUnion_right ..

Premises used: Set.image2_iUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Div α
S : Set (Set α)
t : Set α
⊢ ⋃₀ S / t = ⋃ s ∈ S, s / t

Tactic:
image2_sUnion_left ..

Premises used: Set.image2_sUnion_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
inst : Div α
s : Set α
T : Set (Set α)
⊢ s / ⋃₀ T = ⋃ t ∈ T, s / t

Tactic:
image2_sUnion_right ..

Premises used: Set.image2_sUnion_right
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Div α
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ (i : ι), ⋃ (j : κ i), s i j) / t = ⋃ (i : ι), ⋃ (j : κ i), s i j / t

Tactic:
image2_iUnion₂_left ..

Premises used: Set.image2_iUnion₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice
Goal:
α : Type u_2
ι : Sort u_5
κ : ι → Sort u_6
inst : Div α
s : Set α
t : (i : ι) → κ i → Set α
⊢ s / ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s / t i j

Tactic:
image2_iUnion₂_right ..

Premises used: Set.image2_iUnion₂_right