awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
exact hs.zpow

Premises used: Finset.Nonempty.zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
⊢ (HPow.hPow (β := ℤ) s 0).Nonempty

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := Finset α) ∅ n = ∅

Tactic:
empty_zpow hn

Premises used: Finset.empty_zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := Finset α) ∅ n = ∅

Tactic:
exact empty_zpow hn

Premises used: Finset.empty_zpow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
n : ℤ
ofNat : ∀ (a_1 : ℕ), HPow.hPow (α := Finset α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}
negSucc : ∀ (a_1 : ℕ), HPow.hPow (α := Finset α) {a} (Int.negSucc a_1) = {a ^ Int.negSucc a_1}
⊢ HPow.hPow (α := Finset α) {a} n = {a ^ n}

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
a_1 : ℕ
⊢ HPow.hPow (α := Finset α) {a} (Int.ofNat a_1) = {a ^ Int.ofNat a_1}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
a_1 : ℕ
⊢ HPow.hPow (α := Finset α) {a} (Int.negSucc a_1) = {a ^ Int.negSucc a_1}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
rw : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint s t
rw₁ : 1 ∈ (↑(s / t) : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
rw₂ : 1 ∈ (↑s : Set α) / (↑t : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
rw₃ rw₄ : ¬Disjoint (↑s : Set α) (↑t : Set α) ↔ ¬Disjoint (↑s : Set α) (↑t : Set α)
⊢ 1 ∈ s / t ↔ ¬Disjoint s t

Tactic:
rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]

Premises used: Finset.disjoint_coe, Finset.coe_div, Set.one_mem_div_iff, Finset.mem_coe
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
⊢ 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t

Tactic:
aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv,
    Finset.Nonempty])

Premises used: mul_eq_one_iff_eq_inv, Finset.not_disjoint_iff_nonempty_inter, Finset.Nonempty, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
⊢ 1 ∉ s / t ↔ Disjoint s t

Tactic:
one_mem_div_iff.not_left

Premises used: Finset.one_mem_div_iff, Iff.not_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s t : Finset α
⊢ 1 ∉ t⁻¹ * s ↔ Disjoint s t

Tactic:
one_mem_inv_mul_iff.not_left

Premises used: Finset.one_mem_inv_mul_iff, Iff.not_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s : Finset α
h : s.Nonempty
⊢ 1 ∈ s / s

Tactic:
let ⟨a, ha⟩ := h
  mem_div.2 ⟨a, ha, a, ha, div_self' _⟩

Premises used: Iff.mpr, Membership.mem, HDiv.hDiv, Finset.mem_div, div_self', And.intro, Exists.intro, OfNat.ofNat, _private.0.Finset.Nonempty.one_mem_div.match_1
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
a : α
⊢ IsUnit (M := Finset α) {a}

Tactic:
(Group.isUnit a).finset

Premises used: Group.isUnit, IsUnit.finset
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
s : Finset α
⊢ IsUnit s ↔ ∃ (a : α), s = {a}

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

Premises used: and_true, Group.isUnit, Finset.isUnit_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_5
inst : Group α
s : Finset α
⊢ (∃ (a : α), s = {a} ∧ IsUnit a) ↔ ∃ (a : α), s = {a}

Tactic:
simp only [Group.isUnit, and_true]

Premises used: and_true, Group.isUnit
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
t : Finset α
a : α
⊢ (↑(image (fun (b : α) ↦ a * b) t) : Set α) = (↑(t.preimage (fun (b : α) ↦ a⁻¹ * b) ⋯) : Set α)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
t : Finset α
b : α
⊢ (↑(image (fun (x : α) ↦ x * b) t) : Set α) = (↑(t.preimage (fun (x : α) ↦ x * b⁻¹) ⋯) : Set α)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
t : Finset α
a : α
⊢ image (fun (b : α) ↦ a⁻¹ * b) t = t.preimage (fun (b : α) ↦ a * b) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Group α
t : Finset α
b : α
⊢ image (fun (x : α) ↦ x * b⁻¹) t = t.preimage (fun (x : α) ↦ x * b) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Group α
inst_3 : DivisionMonoid β
inst_4 : FunLike F α β
inst_5 : MonoidHomClass F α β
f : F
s : Finset α
⊢ Eq.{u_3 + 1} (α := Finset β) (image (⇑f : (a : α) → β) s⁻¹) (image (⇑f : (a : α) → β) s)⁻¹

Tactic:
image_comm (map_inv _)

Premises used: map_inv, Finset.image_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Group α
inst_3 : DivisionMonoid β
inst_4 : FunLike F α β
inst_5 : MonoidHomClass F α β
f : F
s t : Finset α
⊢ image (⇑f : (a : α) → β) (s / t) = HDiv.hDiv (α := Finset β) (image (⇑f : (a : α) → β) s) (image (⇑f : (a : α) → β) t)

Tactic:
image_image₂_distrib <| map_div f

Premises used: map_div, Finset.image_image₂_distrib
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) {b}) {a⁻¹ * b}
rw₁ rw₂ : Eq (α := Finset α) {a⁻¹ * b} {a⁻¹ * b}
⊢ preimage {b} (fun (x : α) ↦ a * x) ⋯ = {a⁻¹ * b}

Tactic:
rw [← image_mul_left', image_singleton]

Premises used: Finset.image_mul_left', Finset.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) {b}) {a⁻¹ * b}
classical₁ classical₂ : Eq (α := Finset α) {a⁻¹ * b} {a⁻¹ * b}
⊢ preimage {b} (fun (x : α) ↦ a * x) ⋯ = {a⁻¹ * b}

Tactic:
classical rw [← image_mul_left', image_singleton]

Premises used: Finset.image_mul_left', Finset.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
rw : Eq (α := Finset α) (image (fun (x : α) ↦ x * a⁻¹) {b}) {b * a⁻¹}
rw₁ rw₂ : Eq (α := Finset α) {b * a⁻¹} {b * a⁻¹}
⊢ preimage {b} (fun (x : α) ↦ x * a) ⋯ = {b * a⁻¹}

Tactic:
rw [← image_mul_right', image_singleton]

Premises used: Finset.image_singleton, Finset.image_mul_right'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a b : α
classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * a⁻¹) {b}) {b * a⁻¹}
classical₁ classical₂ : Eq (α := Finset α) {b * a⁻¹} {b * a⁻¹}
⊢ preimage {b} (fun (x : α) ↦ x * a) ⋯ = {b * a⁻¹}

Tactic:
classical rw [← image_mul_right', image_singleton]

Premises used: Finset.image_singleton, Finset.image_mul_right'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
rw₁ : Eq (α := Finset α) {a⁻¹ * 1} {a⁻¹}
rw₂ rw₃ : Eq (α := Finset α) {a⁻¹} {a⁻¹}
⊢ preimage 1 (fun (x : α) ↦ a * x) ⋯ = {a⁻¹}

Tactic:
rw [← image_mul_left', image_one, mul_one]

Premises used: Finset.image_mul_left', mul_one, Finset.image_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a : α
classical : Eq (α := Finset α) (image (fun (b : α) ↦ a⁻¹ * b) 1) {a⁻¹}
classical₁ : Eq (α := Finset α) {a⁻¹ * 1} {a⁻¹}
classical₂ classical₃ : Eq (α := Finset α) {a⁻¹} {a⁻¹}
⊢ preimage 1 (fun (x : α) ↦ a * x) ⋯ = {a⁻¹}

Tactic:
classical rw [← image_mul_left', image_one, mul_one]

Premises used: Finset.image_mul_left', mul_one, Finset.image_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
b : α
rw : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
rw₁ : Eq (α := Finset α) {1 * b⁻¹} {b⁻¹}
rw₂ rw₃ : Eq (α := Finset α) {b⁻¹} {b⁻¹}
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}

Tactic:
rw [← image_mul_right', image_one, one_mul]

Premises used: Finset.image_one, Finset.image_mul_right', one_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
b : α
classical : Eq (α := Finset α) (image (fun (x : α) ↦ x * b⁻¹) 1) {b⁻¹}
classical₁ : Eq (α := Finset α) {1 * b⁻¹} {b⁻¹}
classical₂ classical₃ : Eq (α := Finset α) {b⁻¹} {b⁻¹}
⊢ preimage 1 (fun (x : α) ↦ x * b) ⋯ = {b⁻¹}

Tactic:
classical rw [← image_mul_right', image_one, one_mul]

Premises used: Finset.image_one, Finset.image_mul_right', one_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
a : α
rw : Eq (α := Finset α) {a⁻¹⁻¹} {a}
rw₁ rw₂ : Eq (α := Finset α) {a} {a}
⊢ preimage 1 (fun (x : α) ↦ a⁻¹ * x) ⋯ = {a}

Tactic:
rw [preimage_mul_left_one, inv_inv]

Premises used: Finset.preimage_mul_left_one, inv_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
b : α
rw : Eq (α := Finset α) {b⁻¹⁻¹} {b}
rw₁ rw₂ : Eq (α := Finset α) {b} {b}
⊢ preimage 1 (fun (x : α) ↦ x * b⁻¹) ⋯ = {b}

Tactic:
rw [preimage_mul_right_one, inv_inv]

Premises used: Finset.preimage_mul_right_one, inv_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Monoid α
inst_3 : Monoid β
inst_4 : FunLike F α β
inst_5 : MulHomClass F α β
h : Ne (α := ℕ) 1 0
⊢ ∀ (f : F) (s : Finset α),
    image (⇑f : (a : α) → β) (HPow.hPow (β := ℕ) s 1) =
      HPow.hPow (α := Finset β) (β := ℕ) (image (⇑f : (a : α) → β) s) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Monoid α
inst_3 : Monoid β
inst_4 : FunLike F α β
inst_5 : MulHomClass F α β
n : ℕ
h : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Finset α),
    image (⇑f : (a : α) → β) (s ^ (n + 2)) = HPow.hPow (α := Finset β) (image (⇑f : (a : α) → β) s) (n + 2)

Tactic:
simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Premises used: pow_succ, Finset.image_mul, Nat.succ
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Monoid α
inst_3 : Monoid β
inst_4 : FunLike F α β
inst_5 : MonoidHomClass F α β
f : F
s : Finset α
⊢ image (⇑f : (a : α) → β) (HPow.hPow (β := ℕ) s 0) = HPow.hPow (α := Finset β) (β := ℕ) (image (⇑f : (a : α) → β) s) 0

Tactic:
simp [singleton_one]

Premises used: Finset.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s t : Finset α
a : α
ha : a ∈ (↑t : Set α)
b : α
hb : b ∈ (↑t : Set α)
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s t : Finset α
a : α
ha : a ∈ (↑t : Set α)
b : α
hb : b ∈ (↑t : Set α)
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial

Tactic:
exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s t : Finset α
hs : s.Nontrivial
ht : t.Nontrivial
⊢ (s * t).Nontrivial

Tactic:
ht.mul_left hs.nonempty

Premises used: Finset.Nontrivial.nonempty, Finset.Nontrivial.mul_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
a : α
t : Finset α
⊢ #({a} * t) = #t

Tactic:
card_image₂_singleton_left _ <| mul_right_injective _

Premises used: Finset.card_image₂_singleton_left, mul_right_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
a : α
s t : Finset α
⊢ {a} * (s ∩ t) = {a} * s ∩ ({a} * t)

Tactic:
image₂_singleton_inter _ _ <| mul_right_injective _

Premises used: mul_right_injective, Finset.image₂_singleton_inter
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
t s : Finset α
hs : s.Nonempty
⊢ #t ≤ #(s * t)

Tactic:
have ⟨_, ha⟩ := hs; card_le_card_mul_left_of_injective ha (mul_right_injective _)

Premises used: HMul.hMul, LE.le, Finset.card_le_card_mul_left_of_injective, Finset.card, mul_right_injective, _private.0.Finset.Nonempty.one_mem_div.match_1
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s : Finset α
inl : s = ∅ → #s ≤ #(s * s)
inr : s.Nonempty → #s ≤ #(s * s)
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s : Finset α
h : s = ∅
⊢ #s ≤ #(s * s)

Tactic:
simp [card_le_card_mul_left, *]

Premises used: Finset.card_le_card_mul_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
inst_2 : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ #s ≤ #(s * s)

Tactic:
simp [card_le_card_mul_left, *]

Premises used: Finset.card_le_card_mul_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s t : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s t : Finset α
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Tactic:
exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s : Finset α
a : α
⊢ #(s * {a}) = #s

Tactic:
card_image₂_singleton_right _ <| mul_left_injective _

Premises used: Finset.card_image₂_singleton_right, mul_left_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s t : Finset α
a : α
⊢ s ∩ t * {a} = s * {a} ∩ (t * {a})

Tactic:
image₂_inter_singleton _ _ <| mul_left_injective _

Premises used: Finset.image₂_inter_singleton, mul_left_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s t : Finset α
ht : t.Nonempty
⊢ #s ≤ #(s * t)

Tactic:
have ⟨_, ha⟩ := ht; card_le_card_mul_right_of_injective ha (mul_left_injective _)

Premises used: HMul.hMul, LE.le, mul_left_injective, Finset.card_le_card_mul_right_of_injective, Finset.card, _private.0.Finset.Nonempty.one_mem_div.match_1
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s : Finset α
inl : s = ∅ → #s ≤ #(s * s)
inr : s.Nonempty → #s ≤ #(s * s)
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s : Finset α
h : s = ∅
⊢ #s ≤ #(s * s)

Tactic:
simp [card_le_card_mul_right, *]

Premises used: Finset.card_le_card_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
inst_2 : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ #s ≤ #(s * s)

Tactic:
simp [card_le_card_mul_right, *]

Premises used: Finset.card_le_card_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
hs : s.Nontrivial
h : Ne (α := ℕ) 1 0
⊢ (HPow.hPow (β := ℕ) s 1).Nontrivial

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
hs : s.Nontrivial
n : ℕ
h : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Premises used: pow_succ, Nat.succ_ne_zero, Finset.Nontrivial.mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
rw : #(s ^ n) ≤ #(s ^ n * s)
⊢ #(s ^ n) ≤ #(s ^ (n + 1))

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ n * s)

Tactic:
card_le_card_mul_right hs

Premises used: Finset.card_le_card_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ n * s)

Tactic:
exact card_le_card_mul_right hs

Premises used: Finset.card_le_card_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
inl : #(HPow.hPow (α := Finset α) ∅ m) ≤ #(HPow.hPow (α := Finset α) ∅ n)
inr : ∀ (hs : s.Nonempty), #(s ^ m) ≤ #(s ^ n)
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(HPow.hPow (α := Finset α) ∅ m) ≤ #(HPow.hPow (α := Finset α) ∅ n)

Tactic:
simp [hm]
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
hs.card_pow_mono hmn

Premises used: Finset.Nonempty.card_pow_mono
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
exact hs.card_pow_mono hmn

Premises used: Finset.Nonempty.card_pow_mono
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelMonoid α
s : Finset α
n : ℕ
hn : n ≠ 0
⊢ #s ≤ #(s ^ n)

Tactic:
simpa using card_pow_mono (s := s) one_ne_zero (Nat.one_le_iff_ne_zero.2 hn)

Premises used: Iff.mpr, Finset.card_pow_mono, Nat.one_le_iff_ne_zero, one_ne_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
⊢ #t ≤ #(s / t)

Tactic:
have ⟨_, ha⟩ := hs; card_le_card_image₂_left _ ha div_right_injective

Premises used: HDiv.hDiv, div_right_injective, LE.le, Finset.card, Finset.card_le_card_image₂_left, _private.0.Finset.Nonempty.one_mem_div.match_1
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
ht : t.Nonempty
⊢ #s ≤ #(s / t)

Tactic:
have ⟨_, ha⟩ := ht; card_le_card_image₂_right _ ha div_left_injective

Premises used: div_left_injective, HDiv.hDiv, LE.le, Finset.card_le_card_image₂_right, Finset.card, _private.0.Finset.Nonempty.one_mem_div.match_1
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s : Finset α
inl : s = ∅ → #s ≤ #(s / s)
inr : s.Nonempty → #s ≤ #(s / s)
⊢ #s ≤ #(s / s)

Tactic:
cases s.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s : Finset α
h : s = ∅
⊢ #s ≤ #(s / s)

Tactic:
simp [card_le_card_div_left, *]

Premises used: Finset.card_le_card_div_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ #s ≤ #(s / s)

Tactic:
simp [card_le_card_div_left, *]

Premises used: Finset.card_le_card_div_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
ι : Type u_5
α : ι → Type u_6
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → Mul (α i)
s t : (i : ι) → Finset (α i)
⊢ (piFinset (δ := α) fun (i : ι) ↦ s i * t i) = piFinset (δ := α) s * piFinset (δ := α) t

Tactic:
piFinset_image₂ _ _ _

Premises used: Fintype.piFinset_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
ι : Type u_5
α : ι → Type u_6
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → Div (α i)
s t : (i : ι) → Finset (α i)
⊢ (piFinset (δ := α) fun (i : ι) ↦ s i / t i) = piFinset (δ := α) s / piFinset (δ := α) t

Tactic:
piFinset_image₂ _ _ _

Premises used: Fintype.piFinset_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
ι : Type u_5
α : ι → Type u_6
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → Inv (α i)
s : (i : ι) → Finset (α i)
⊢ (piFinset (δ := α) fun (i : ι) ↦ (s i)⁻¹) = (piFinset (δ := α) s)⁻¹

Tactic:
piFinset_image _ _

Premises used: Fintype.piFinset_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
⊢ Eq.{u_2 + 1} (α := Finset α) (toFinset 1) 1

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.cons, Set.toFinset, Multiset.ofList, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : One α
h : Set.Finite.{u_2} (α := α) 1
⊢ h.toFinset (s := 1) = 1

Tactic:
Finite.toFinset_singleton _

Premises used: Set.Finite.toFinset_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Set α
inst_2 : Fintype (↑s : Type u_2)
inst_3 : Fintype (↑t : Type u_2)
inst_4 : Fintype (↑(s * t) : Type u_2)
⊢ (s * t).toFinset = s.toFinset * t.toFinset

Tactic:
toFinset_image2 _ _ _

Premises used: Set.toFinset_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Set α
hs : s.Finite
ht : t.Finite
hf : (s * t).Finite
⊢ hf.toFinset (s := s * t) = hs.toFinset (s := s) * ht.toFinset (s := t)

Tactic:
Finite.toFinset_image2 _ _ _

Premises used: Set.Finite.image2, Set.Finite.toFinset_image2
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Goal:
α : Type u_1
ι : Type u_2
inst : CommMonoid α
inst_1 : DecidableEq α
s : Finset ι
f : ι → Finset α
⊢ (↑(∏ i ∈ s, f i) : Set α) = ∏ i ∈ s, (↑(f i) : Set α)

Tactic:
map_prod (coeMonoidHom : Finset α →* Set α) _ _

Premises used: setOf, map_prod, Multiset.Mem, Finset.coeMonoidHom
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Goal:
α : Type u_1
ι : Type u_2
inst : CommMonoid α
inst_1 : DecidableEq ι
inst_2 : InvolutiveInv ι
s : Finset ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (∏ i ∈ s⁻¹, f i) (∏ i ∈ s, f i⁻¹)

Tactic:
prod_image inv_injective.injOn

Premises used: Function.Injective.injOn, inv_injective, Finset.prod_image