awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : ∀ (hg : ∀ i ∈ tl, g i ∈ f i), (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod

Tactic:
mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

Premises used: List.mem_cons_of_mem, List.mem_cons_self, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : ∀ (hg : ∀ i ∈ tl, g i ∈ f i), (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod

Tactic:
exact mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

Premises used: List.mem_cons_of_mem, List.mem_cons_self, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
nil : ∀ (hg : ∀ (i : ι), Membership.mem (γ := List ι) [] i → g i ∈ f i), (List.map g []).prod ∈ (List.map f []).prod
cons :
  ∀ (h : ι) (tl : List ι) (ih : ∀ (hg : ∀ i ∈ tl, g i ∈ f i), (List.map g tl).prod ∈ (List.map f tl).prod)
    (hg : ∀ i ∈ h :: tl, g i ∈ f i), (List.map g (h :: tl)).prod ∈ (List.map f (h :: tl)).prod
⊢ (List.map g t).prod ∈ (List.map f t).prod

Tactic:
induction t with
  | nil => simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

Premises used: List.map_cons, Set.mem_one, List.prod_nil, List.prod_cons, List.map_nil
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f₁ f₂ : ι → Set α
hf : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f₁ i ⊆ f₂ i
⊢ (List.map f₁ []).prod ⊆ (List.map f₁ []).prod

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : ∀ (hf : ∀ i ∈ tl, f₁ i ⊆ f₂ i), (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ f₁ h * (List.map f₁ tl).prod ⊆ f₂ h * (List.map f₂ tl).prod

Tactic:
mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

Premises used: List.mem_cons_of_mem, List.mem_cons_self, Set.mul_subset_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : ∀ (hf : ∀ i ∈ tl, f₁ i ⊆ f₂ i), (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ f₁ h * (List.map f₁ tl).prod ⊆ f₂ h * (List.map f₂ tl).prod

Tactic:
exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

Premises used: List.mem_cons_of_mem, List.mem_cons_self, Set.mul_subset_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
nil : ∀ (hf : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f₁ i ⊆ f₂ i), (List.map f₁ []).prod ⊆ (List.map f₁ []).prod
cons :
  ∀ (h : ι) (tl : List ι) (ih : ∀ (hf : ∀ i ∈ tl, f₁ i ⊆ f₂ i), (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod)
    (hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i), (List.map f₁ (h :: tl)).prod ⊆ (List.map f₂ (h :: tl)).prod
⊢ (List.map f₁ t).prod ⊆ (List.map f₂ t).prod

Tactic:
induction t with
  | nil => rfl
  | cons h tl ih =>
    simp_rw [List.map_cons, List.prod_cons]
    exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
M : Type u_5
inst : Monoid M
s : List M
⊢ Eq (α := Set M) (List.prod (List.map (fun (i : M) ↦ {i}) s)) {s.prod}

Tactic:
(map_list_prod (singletonMonoidHom : M →* Set M) _).symm

Premises used: setOf, map_list_prod, Set.singleton, Eq.symm, Set.singletonMonoidHom
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Multiset ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
h : ∀ (a : List ι) (hg : ∀ i ∈ ⟦a⟧, g i ∈ f i), (Multiset.map g ⟦a⟧).prod ∈ (Multiset.map f ⟦a⟧).prod
⊢ (Multiset.map g t).prod ∈ (Multiset.map f t).prod

Tactic:
induction t using Quotient.inductionOn
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
a : List ι
hg : ∀ i ∈ ⟦a⟧, g i ∈ f i
⊢ (List.map g a).prod ∈ (List.map f a).prod

Tactic:
list_prod_mem_list_prod _ _ _ hg

Premises used: Set.Mem, Set.list_prod_mem_list_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f : ι → Set α
g : ι → α
a : List ι
hg : ∀ i ∈ ⟦a⟧, g i ∈ f i
⊢ (List.map g a).prod ∈ (List.map f a).prod

Tactic:
exact list_prod_mem_list_prod _ _ _ hg

Premises used: Set.list_prod_mem_list_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
h : ∀ (a : List ι) (hf : ∀ i ∈ ⟦a⟧, f₁ i ⊆ f₂ i), (Multiset.map f₁ ⟦a⟧).prod ⊆ (Multiset.map f₂ ⟦a⟧).prod
⊢ (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod

Tactic:
induction t using Quotient.inductionOn
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f₁ f₂ : ι → Set α
a : List ι
hf : ∀ i ∈ ⟦a⟧, f₁ i ⊆ f₂ i
⊢ (List.map f₁ a).prod ⊆ (List.map f₂ a).prod

Tactic:
list_prod_subset_list_prod _ _ _ hf

Premises used: Set.list_prod_subset_list_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
f₁ f₂ : ι → Set α
a : List ι
hf : ∀ i ∈ ⟦a⟧, f₁ i ⊆ f₂ i
⊢ (List.map f₁ a).prod ⊆ (List.map f₂ a).prod

Tactic:
exact list_prod_subset_list_prod _ _ _ hf

Premises used: Set.list_prod_subset_list_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
⊢ Eq (α := Set M) (Multiset.prod (Multiset.map (fun (i : M) ↦ {i}) s)) {s.prod}

Tactic:
(map_multiset_prod (singletonMonoidHom : M →* Set M) _).symm

Premises used: setOf, map_multiset_prod, Set.singleton, Eq.symm, Set.singletonMonoidHom
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Finset ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ Membership.mem (γ := Set α) (∏ i ∈ t, f i) (∏ i ∈ t, g i)

Tactic:
multiset_prod_mem_multiset_prod _ _ _ hg

Premises used: Set.Mem, Finset.prod, Set.multiset_prod_mem_multiset_prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
t : Finset ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ Subset.{u_2} (α := Set α) (∏ i ∈ t, f₁ i) (∏ i ∈ t, f₂ i)

Tactic:
multiset_prod_subset_multiset_prod _ _ _ hf

Premises used: Set.multiset_prod_subset_multiset_prod, Finset.prod
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
M : Type u_5
ι : Type u_6
inst : CommMonoid M
s : Finset ι
I : ι → M
⊢ Eq (α := Set M) (∏ i ∈ s, {I i}) {∏ i ∈ s, I i}

Tactic:
(map_prod (singletonMonoidHom : M →* Set M) _ _).symm

Premises used: setOf, map_prod, Set.singleton, Eq.symm, Set.singletonMonoidHom
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
      Membership.mem (γ := Set α) (∏ i ∈ l, S i) x
⊢ Eq.{u_2 + 1} (α := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S)
    (∏ i ∈ l, S i)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
l : Finset ι
S : ι → Set α
x : α
h :
  Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
h₁ :
  (∃ x_1 ∈ (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S, ∏ i ∈ l, x_1 i = x) ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
h₂ :
  (∃ (x_1 : ι → α), (∀ i ∈ (↑l : Set ι), x_1 i ∈ S i) ∧ ∏ i ∈ l, x_1 i = x) ↔
    ∃ (g : ι → α) (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x
h₃ :
  (∃ (x_1 : ι → α), (∀ i ∈ (↑l : Set ι), x_1 i ∈ S i) ∧ ∏ i ∈ l, x_1 i = x) ↔
    ∃ (g : ι → α), (∀ {i : ι}, i ∈ l → g i ∈ S i) ∧ ∏ i ∈ l, g i = x
⊢ Membership.mem (γ := Set α) ((fun (f : ι → α) ↦ ∏ i ∈ l, f i) '' (↑l : Set ι).pi (α := fun (a : ι) ↦ α) S) x ↔
    Membership.mem (γ := Set α) (∏ i ∈ l, S i) x

Tactic:
simp_rw [mem_finsetProd, mem_image, mem_pi, exists_prop, Finset.mem_coe]

Premises used: Set.mem_image, Set.mem_pi, exists_prop, Set.mem_finsetProd, Finset.mem_coe
-- Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Fintype ι
S : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) ((fun (f : ι → α) ↦ ∏ i : ι, f i) '' pi (α := fun (a : ι) ↦ α) univ S) (∏ i : ι, S i)

Tactic:
simpa only [Finset.coe_univ] using image_finsetProd_pi Finset.univ S

Premises used: Finset.univ, Finset.coe_univ, Set.image_finsetProd_pi
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
⊢ #(↑(image2 (fun (x1 x2 : M) ↦ x1 * x2) s t) : Type u_2) ≤ #(↑s : Type u_2) * #(↑t : Type u_2)

Tactic:
Cardinal.mk_image2_le

Premises used: Cardinal.mk_image2_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
⊢ #(↑(image2 (fun (x1 x2 : M) ↦ x1 * x2) s t) : Type u_2) ≤ #(↑s : Type u_2) * #(↑t : Type u_2)

Tactic:
exact Cardinal.mk_image2_le

Premises used: Cardinal.mk_image2_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
inl :
  ∀ (h : (s * t).Infinite),
    Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
inr :
  ∀ (h : (s * t).Finite),
    Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)
⊢ Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)

Tactic:
obtain h | h := (s * t).infinite_or_finite

Premises used: HMul.hMul, Set.infinite_or_finite
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Infinite
⊢ Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)

Tactic:
simp [Set.Infinite.card_eq_zero h]

Premises used: Set.Infinite.card_eq_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Finite
inr :
  LE.le (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) #(↑(s * t) : Type u_2) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) (#(↑s : Type u_2) * #(↑t : Type u_2)) : ℕ)
⊢ Nat.card.{u_2} (↑(s * t) : Type u_2) ≤ Nat.card.{u_2} (↑s : Type u_2) * Nat.card.{u_2} (↑t : Type u_2)

Tactic:
simp only [Nat.card, ← Cardinal.toNat_mul]

Premises used: Cardinal.toNat_mul, Nat.card
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Finite
⊢ LE.le (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) #(↑(s * t) : Type u_2) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) (#(↑s : Type u_2) * #(↑t : Type u_2)) : ℕ)

Tactic:
Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_

Premises used: Cardinal.toNat_le_toNat, Cardinal.mk_mul_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Finite
inr : #(↑s : Type u_2) * #(↑t : Type u_2) < ℵ₀
⊢ LE.le (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) #(↑(s * t) : Type u_2) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u_2}) → ℕ) (#(↑s : Type u_2) * #(↑t : Type u_2)) : ℕ)

Tactic:
refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_

Premises used: Cardinal.toNat_le_toNat, Cardinal.mk_mul_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : Mul M
s t : Set M
inst_1 : IsCancelMul M
h : (s * t).Finite
⊢ #(↑s : Type u_2) * #(↑t : Type u_2) < ℵ₀

Tactic:
aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul])

Premises used: Cardinal.mul_lt_aleph0_iff, Set.finite_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : InvolutiveInv G
s : Set G
rw : #(↑((fun (x : G) ↦ x⁻¹) '' s) : Type u_1) = #(↑s : Type u_1)
rw₁ rw₂ : #(↑s : Type u_1) = #(↑s : Type u_1)
⊢ #(↑s⁻¹ : Type u_1) = #(↑s : Type u_1)

Tactic:
rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]

Premises used: Function.Injective.injOn, inv_injective, Cardinal.mk_image_eq_of_injOn, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : InvolutiveInv G
s : Set G
⊢ s⁻¹.encard = s.encard

Tactic:
simp [← toENat_cardinalMk]

Premises used: Set.toENat_cardinalMk
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : InvolutiveInv G
s : Set G
⊢ s⁻¹.ncard = s.ncard

Tactic:
simp [ncard]

Premises used: Set.ncard
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : InvolutiveInv G
s : Set G
⊢ Nat.card.{u_1} (↑s⁻¹ : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : DivInvMonoid M
s t : Set M
⊢ #(↑(image2 (fun (x1 x2 : M) ↦ x1 / x2) s t) : Type u_2) ≤ #(↑s : Type u_2) * #(↑t : Type u_2)

Tactic:
Cardinal.mk_image2_le

Premises used: Cardinal.mk_image2_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
M : Type u_2
inst : DivInvMonoid M
s t : Set M
⊢ #(↑(image2 (fun (x1 x2 : M) ↦ x1 / x2) s t) : Type u_2) ≤ #(↑s : Type u_2) * #(↑t : Type u_2)

Tactic:
exact Cardinal.mk_image2_le

Premises used: Cardinal.mk_image2_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : Group G
s t : Set G
rw : Nat.card.{u_1} (↑(s * t⁻¹) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) * Nat.card.{u_1} (↑t⁻¹ : Type u_1)
⊢ Nat.card.{u_1} (↑(s / t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) * Nat.card.{u_1} (↑t : Type u_1)

Tactic:
rw [div_eq_mul_inv, ← natCard_inv t]

Premises used: div_eq_mul_inv, Set.natCard_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : Group G
s t : Set G
⊢ Nat.card.{u_1} (↑(s * t⁻¹) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) * Nat.card.{u_1} (↑t⁻¹ : Type u_1)

Tactic:
natCard_mul_le

Premises used: Set.natCard_mul_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
inst : Group G
s t : Set G
⊢ Nat.card.{u_1} (↑(s * t⁻¹) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) * Nat.card.{u_1} (↑t⁻¹ : Type u_1)

Tactic:
exact natCard_mul_le

Premises used: Set.natCard_mul_le
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ #(↑(a • s) : Type u_3) = #(↑s : Type u_3)

Tactic:
Cardinal.mk_image_eq_of_injOn _ _ (MulAction.injective a).injOn

Premises used: Function.Injective.injOn, Cardinal.mk_image_eq_of_injOn, MulAction.injective
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ (a • s).encard = s.encard

Tactic:
simp [← toENat_cardinalMk]

Premises used: Set.toENat_cardinalMk
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ (a • s).ncard = s.ncard

Tactic:
simp [ncard]

Premises used: Set.ncard
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Card
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
a : G
s : Set α
⊢ Nat.card.{u_3} (↑(a • s) : Type u_3) = Nat.card.{u_3} (↑s : Type u_3)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : One α
⊢ Set.Finite.{u_2} (α := α) 1

Tactic:
finite_singleton _

Premises used: Set.finite_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ s.Finite → t.Finite → (s * t).Finite

Tactic:
Finite.image2 _

Premises used: Set.Finite.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ DecidablePred fun (x : α) ↦ x = 1

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
n : ℕ
ih : DecidablePred fun (x : α) ↦ x ∈ s ^ n
succ : DecidablePred fun (x : α) ↦ x ∈ s ^ n * s
⊢ DecidablePred fun (x : α) ↦ x ∈ s ^ (n + 1)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
n : ℕ
ih : DecidablePred fun (x : α) ↦ x ∈ s ^ n
⊢ DecidablePred fun (x : α) ↦ x ∈ s ^ n * s

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid α
s t : Set α
inst_1 : Fintype α
inst_2 : DecidableEq α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
n : ℕ
zero : DecidablePred fun (x : α) ↦ x ∈ HPow.hPow (β := ℕ) s 0
succ : (n : ℕ) → (ih : DecidablePred fun (x : α) ↦ x ∈ s ^ n) → DecidablePred fun (x : α) ↦ x ∈ s ^ (n + 1)
⊢ DecidablePred fun (x : α) ↦ x ∈ s ^ n

Tactic:
induction n with
  | zero =>
    simp only [pow_zero, mem_one]
    infer_instance
  | succ n ih =>
    rw [pow_succ]
    infer_instance

Premises used: pow_succ, Set.mem_one, pow_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set α
t : Set β
⊢ s.Finite → t.Finite → (s • t).Finite

Tactic:
Finite.image2 _

Premises used: Set.Finite.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set β
a : α
⊢ s.Finite → (a • s).Finite

Tactic:
Finite.image _

Premises used: Set.Finite.image
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
s : Set β
a : α
⊢ (a • s).Infinite → s.Infinite

Tactic:
Infinite.of_image _

Premises used: Set.Infinite.of_image
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
s t : Set β
hs : s.Finite
ht : t.Finite
⊢ (s -ᵥ t).Finite

Tactic:
hs.image2 _ ht

Premises used: Set.Finite.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : IsRightCancelMul α
s t : Set α
⊢ (s * t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
finite_image2 (fun _ _ ↦ (mul_left_injective _).injOn) fun _ _ ↦ (mul_right_injective _).injOn

Premises used: Function.Injective.injOn, mul_left_injective, mul_right_injective, Set.finite_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : IsRightCancelMul α
s t : Set α
⊢ (s * t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
infinite_image2 (fun _ _ => (mul_left_injective _).injOn) fun _ _ => (mul_right_injective _).injOn

Premises used: Function.Injective.injOn, Set.infinite_image2, mul_left_injective, mul_right_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
rw : Set.Finite (α := α) ((fun (x : α) ↦ x⁻¹) '' s) ↔ s.Finite
rw₁ rw₂ : s.Finite ↔ s.Finite
⊢ s⁻¹.Finite ↔ s.Finite

Tactic:
rw [← image_inv_eq_inv, finite_image_iff inv_injective.injOn]

Premises used: Function.Injective.injOn, Set.finite_image_iff, inv_injective, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : InvolutiveInv α
s : Set α
⊢ s⁻¹.Infinite ↔ s.Infinite

Tactic:
finite_inv.not

Premises used: Iff.not, Set.finite_inv, Set.Infinite
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : Div α
s t : Set α
⊢ s.Finite → t.Finite → (s / t).Finite

Tactic:
.image2 _

Premises used: Set.Finite.image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : Group α
s t : Set α
⊢ (s / t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
finite_image2 (fun _ _ ↦ div_left_injective.injOn) fun _ _ ↦ div_right_injective.injOn

Premises used: Function.Injective.injOn, div_left_injective, div_right_injective, Set.finite_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Set.Finite
Goal:
α : Type u_2
inst : Group α
s t : Set α
⊢ (s / t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
infinite_image2 (fun _ _ ↦ div_left_injective.injOn) fun _ _ ↦ div_right_injective.injOn

Premises used: Function.Injective.injOn, div_left_injective, Set.infinite_image2, div_right_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
⊢ 0 < Fintype.card G

Tactic:
have hG : 0 < Fintype.card G := Fintype.card_pos
-- 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
inl :
  ∀ [inst_3 : (k : ℕ) → DecidablePred fun (x : G) ↦ x ∈ HPow.hPow (α := Set G) ∅ k] (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) =
        Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
inr :
  ∀ (a : G) (ha : a ∈ S) (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)
⊢ ∀ (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:
rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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 : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) =
        Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)

Tactic:
fun k hk ↦ Fintype.card_congr ?_

Premises used: Fintype.card_congr
-- 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
inl :
  (k : ℕ) →
    (hk : Fintype.card G ≤ k) →
      (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) ≃ (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)
⊢ ∀ (k : ℕ),
    Fintype.card G ≤ k →
      Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ k) : Type u_5) =
        Fintype.card.{u_5} (↑(HPow.hPow (α := Set G) ∅ (Fintype.card G)) : Type u_5)

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

Premises used: Fintype.card_congr