awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
succ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ (n + 1)
succ₁ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
succ₂ : (↑(npowRec n s) : Set α) * (↑s : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
succ₃ succ₄ : (↑s : Set α) ^ n * (↑s : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
⊢ (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)

Tactic:
rw [npowRec, pow_succ, coe_mul, ih]

Premises used: pow_succ, Finset.coe_mul, npowRec
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
zero : (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
succ :
  ∀ (n : ℕ) (ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n), (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)
⊢ (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n

Tactic:
induction n with
  | zero => rw [npowRec, pow_zero, coe_one]
  | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]

Premises used: Finset.coe_one, pow_succ, Finset.coe_mul, npowRec, pow_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
hs : 1 ∈ s
⊢ Monotone.{0, u_2} (β := Finset α) fun (x : ℕ) ↦ s ^ x

Tactic:
pow_right_monotone <| one_subset.2 hs

Premises used: Iff.mpr, Finset.one_subset, pow_right_monotone
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
hst : s ⊆ t
⊢ s ^ n ⊆ t ^ n

Tactic:
subset_of_le (pow_left_mono n hst)

Premises used: Finset.subset_of_le, pow_left_mono
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
m n : ℕ
hs : 1 ∈ s
hmn : m ≤ n
⊢ s ^ m ⊆ s ^ n

Tactic:
Finset.pow_right_monotone hs hmn

Premises used: Set.Mem, Finset.pow_right_monotone, setOf
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
m n : ℕ
hst : s ⊆ t
ht : 1 ∈ t
hmn : m ≤ n
⊢ s ^ m ⊆ t ^ n

Tactic:
(pow_subset_pow_left hst).trans (pow_subset_pow_right ht hmn)

Premises used: Finset.pow_subset_pow_right, HasSubset.Subset.trans, Finset.pow_subset_pow_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn

Premises used: Iff.mpr, Finset.pow_subset_pow_right, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
hst : HPow.hPow (β := ℕ) s 2 ⊆ t * s
hn : n ≠ 0
⊢ s ^ n ⊆ t ^ (n - 1) * s

Tactic:
subset_of_le (pow_le_pow_mul_of_sq_le_mul hst hn)

Premises used: pow_le_pow_mul_of_sq_le_mul, Finset.subset_of_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n_1 n : ℕ
hn : n + 1 ≠ 0
⊢ HPow.hPow (α := Finset α) ∅ (n + 1) = ∅

Tactic:
simp [pow_succ]

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

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
hs : s.Nonempty
n : ℕ
rw : (s ^ n * s).Nonempty
⊢ (s ^ (n + 1)).Nonempty

Tactic:
rw [pow_succ]

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

Tactic:
hs.pow.mul hs

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

Tactic:
exact hs.pow.mul hs

Premises used: Finset.Nonempty.mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
mpr : s = ∅ ∧ n ≠ 0 → s ^ n = ∅
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
mp : s.Nonempty ∨ n = 0 → (s ^ n).Nonempty
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
hs.pow

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

Tactic:
exact hs.pow

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

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

Tactic:
empty_pow hn

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

Tactic:
exact empty_pow hn

Premises used: Finset.empty_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ HPow.hPow (α := Finset α) (β := ℕ) {a} 0 = {HPow.hPow (β := ℕ) a 0}

Tactic:
simp [singleton_one]

Premises used: Finset.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
n : ℕ
⊢ HPow.hPow (α := Finset α) {a} (n + 1) = {a ^ (n + 1)}

Tactic:
simp [pow_succ, singleton_pow _ n]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

Premises used: Iff.mpr, Finset.singleton_subset_iff, Finset.pow_subset_pow_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
simpa using pow_mem_pow hs

Premises used: Finset.pow_mem_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
a : (s ∩ t) ^ n ⊆ s ^ n
a₁ : (s ∩ t) ^ n ⊆ t ^ n
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter

Premises used: Finset.subset_inter
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
a : s ∩ t ⊆ s
⊢ (s ∩ t) ^ n ⊆ s ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
a : s ∩ t ⊆ t
⊢ (s ∩ t) ^ n ⊆ t ^ n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ s

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ t

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : List (Finset α)
⊢ (↑s.prod : Set α) = (List.map SetLike.coe s).prod

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

Premises used: setOf, map_list_prod, Multiset.Mem, Finset.coeMonoidHom
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
rw :
  (∃ (f : (i : Fin n) → (↑((SetLike.coe ∘ s) i) : Type u_2)),
      List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a) ↔
    ∃ (f : (i : Fin n) → ↥(s i)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
⊢ a ∈ (List.ofFn s).prod ↔
    ∃ (f : (i : Fin n) → ↥(s i)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a

Tactic:
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]

Premises used: Set.mem_prod_list_ofFn, List.map_ofFn, Finset.coe_list_prod, Finset.mem_coe
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ (f : (i : Fin n) → (↑((SetLike.coe ∘ s) i) : Type u_2)),
      List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a) ↔
    ∃ (f : (i : Fin n) → ↥(s i)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ (f : Fin n → ↥s), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a

Tactic:
simp [← mem_coe (s := s ^ n), coe_pow, Set.mem_pow]

Premises used: Set.mem_pow, Finset.mem_coe, Finset.coe_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ #(HPow.hPow (β := ℕ) s 0) ≤ HPow.hPow (β := ℕ) (#s) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : #(s ^ n * s) ≤ #s ^ n * #s
⊢ #(s ^ (n + 1)) ≤ #s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ]

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

Tactic:
gcongr
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) ≤ #s ^ n

Tactic:
card_pow_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) ≤ #s ^ n

Tactic:
exact card_pow_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n * s) ≤ #s ^ n * #s

Tactic:
refine card_mul_le.trans (by gcongr; exact card_pow_le)

Premises used: Finset.card_mul_le, LE.le.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
inst_2 : Fintype α
hs : 1 ∈ s
⊢ s * univ = univ

Tactic:
eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, hs, _, mem_univ _, one_mul _⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.eq_univ_iff_forall, And.intro, Exists.intro, OfNat.ofNat, one_mul, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
t : Finset α
inst_2 : Fintype α
ht : 1 ∈ t
⊢ univ * t = univ

Tactic:
eq_univ_iff_forall.2 fun _ => mem_mul.2 ⟨_, mem_univ _, _, ht, mul_one _⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.eq_univ_iff_forall, And.intro, Exists.intro, mul_one, OfNat.ofNat, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : Fintype α
⊢ HMul.hMul (α := Finset α) univ univ = univ

Tactic:
mul_univ_of_one_mem <| mem_univ _

Premises used: Finset.mem_univ, Finset.mul_univ_of_one_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
n : ℕ
inst_2 : Fintype α
hn : n ≠ 0
rw : (↑univ : Set α) ^ n = (↑univ : Set α)
rw₁ : HPow.hPow (α := Set α) Set.univ n = Set.univ
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set α) Set.univ Set.univ
⊢ (↑(HPow.hPow (α := Finset α) univ n) : Set α) = (↑univ : Set α)

Tactic:
rw [coe_pow, coe_univ, Set.univ_pow hn]

Premises used: Finset.coe_univ, Set.univ_pow, Finset.coe_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ IsUnit a → IsUnit (M := Finset α) {a}

Tactic:
IsUnit.map (singletonMonoidHom : α →* Finset α)

Premises used: Finset.singletonMonoidHom, IsUnit.map
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ image op (HPow.hPow (β := ℕ) s 0) = HPow.hPow (β := ℕ) (image op s) 0

Tactic:
simp [singleton_one]

Premises used: Finset.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : image op (s ^ n * s) = image op s ^ (n + 1)
rw₁ : image op (s ^ n * s) = image op s * image op s ^ n
rw₂ : image op s * image op (s ^ n) = image op s * image op s ^ n
rw₃ rw₄ : image op s * image op s ^ n = image op s * image op s ^ n
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ', image_op_mul, image_op_pow]

Premises used: pow_succ, Finset.image_op_mul, pow_succ'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ map (Equiv.toEmbedding opEquiv) (HPow.hPow (β := ℕ) s 0) = HPow.hPow (β := ℕ) (map (Equiv.toEmbedding opEquiv) s) 0

Tactic:
simp [singleton_one]

Premises used: Finset.singleton_one
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
rw : map (Equiv.toEmbedding opEquiv) (s ^ n * s) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)
rw₁ :
  map (Equiv.toEmbedding opEquiv) (s ^ n * s) =
    map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
rw₂ :
  map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) (s ^ n) =
    map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
rw₃ rw₄ :
  map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n =
    map (Equiv.toEmbedding opEquiv) s * map (Equiv.toEmbedding opEquiv) s ^ n
⊢ map (Equiv.toEmbedding opEquiv) (s ^ (n + 1)) = map (Equiv.toEmbedding opEquiv) s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ', map_op_mul, map_op_pow]

Premises used: pow_succ, Finset.map_op_mul, pow_succ'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Monoid α
inst_3 : Monoid β
s : Finset α
t : Finset β
⊢ HPow.hPow (β := ℕ) (s ×ˢ t) 0 = HPow.hPow (β := ℕ) s 0 ×ˢ HPow.hPow (β := ℕ) t 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Monoid α
inst_3 : Monoid β
s : Finset α
t : Finset β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
simp [pow_succ, product_pow _ _ n]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℕ
⊢ (↑(s ^ Int.negSucc n) : Set α) = (↑s : Set α) ^ Int.negSucc n

Tactic:
(coe_inv _).trans ?_

Premises used: setOf, Finset.coe_inv, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℕ
refine : (↑(npowRec n.succ s) : Set α)⁻¹ = (↑s : Set α) ^ Int.negSucc n
⊢ (↑(s ^ Int.negSucc n) : Set α) = (↑s : Set α) ^ Int.negSucc n

Tactic:
refine (coe_inv _).trans ?_

Premises used: Finset.coe_inv, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℕ
⊢ (↑(npowRec n.succ s) : Set α)⁻¹ = (↑s : Set α) ^ Int.negSucc n

Tactic:
congr_arg Inv.inv (coe_pow _ _)

Premises used: Set.Mem, setOf, congr_arg, Inv.inv, Set.preimage, zpowRec, Finset.coe_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℕ
⊢ (↑(npowRec n.succ s) : Set α)⁻¹ = (↑s : Set α) ^ Int.negSucc n

Tactic:
exact congr_arg Inv.inv (coe_pow _ _)

Premises used: congr_arg, Inv.inv, Finset.coe_pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
simp_rw :
  (↑(s * t) : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
simp_rw₁ :
  (↑s : Set α) * (↑t : Set α) = (↑1 : Set α) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
simp_rw₂ :
  (↑s : Set α) * (↑t : Set α) = 1 ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
simp_rw₃ :
  (∃ (a : α) (b : α), (↑s : Set α) = {a} ∧ (↑t : Set α) = {b} ∧ a * b = 1) ↔
    ∃ (a : α) (b : α), (↑s : Set α) = (↑{a} : Set α) ∧ (↑t : Set α) = (↑{b} : Set α) ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]

Premises used: Finset.coe_one, Finset.coe_singleton, Finset.coe_mul, Finset.coe_inj, Set.mul_eq_one_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
mp : IsUnit s → ∃ (a : α), s = {a} ∧ IsUnit a
mpr : (∃ (a : α), s = {a} ∧ IsUnit a) → IsUnit s
⊢ IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
mp :
  ∀ (a b : α) (ha : (↑u : Finset α) = {a}) (hb : (↑u⁻¹ : Finset α) = {b}) (h : a * b = 1),
    ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a
⊢ ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv

Premises used: Units.mul_inv, Iff.mp, Finset.mul_eq_one_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
⊢ ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a

Tactic:
⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩

Premises used: Finset.singleton_injective, And.intro, Units.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
mp : Eq (α := Finset α) {b * a} {1}
⊢ ∃ (a : α), (↑u : Finset α) = {a} ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
mp : (↑u⁻¹ : Finset α) * (↑u : Finset α) = {1}
⊢ Eq (α := Finset α) {b * a} {1}

Tactic:
rw [← singleton_mul_singleton, ← ha, ← hb]

Premises used: Finset.singleton_mul_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
⊢ (↑u⁻¹ : Finset α) * (↑u : Finset α) = {1}

Tactic:
u.inv_mul

Premises used: Units.inv_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : (↑u : Finset α) = {a}
hb : (↑u⁻¹ : Finset α) = {b}
h : a * b = 1
⊢ (↑u⁻¹ : Finset α) * (↑u : Finset α) = {1}

Tactic:
exact u.inv_mul

Premises used: Units.inv_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (M := Finset α) {a}

Tactic:
ha.finset

Premises used: IsUnit.finset
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (M := Finset α) {a}

Tactic:
exact ha.finset

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

Tactic:
simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]

Premises used: Finset.coe_eq_singleton, Set.isUnit_iff, Finset.isUnit_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
inst_2 : Fintype α
⊢ HDiv.hDiv (α := Finset α) univ univ = univ

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
rw : s ⊆ s * t⁻¹
⊢ s ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹

Tactic:
exact subset_mul_left _ <| by simpa

Premises used: Finset.subset_mul_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
rw : t⁻¹ ⊆ s * t⁻¹
⊢ t⁻¹ ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
subset_mul_right _ hs

Premises used: Set.Mem, setOf, Finset.subset_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
exact subset_mul_right _ hs

Premises used: Finset.subset_mul_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
n : ℤ
hn : n ≠ 0
ofNat : ∀ (a : ℕ) (hn : Int.ofNat a ≠ 0), HPow.hPow (α := Finset α) ∅ (Int.ofNat a) = ∅
negSucc : ∀ (a : ℕ) (hn : Int.negSucc a ≠ 0), HPow.hPow (α := Finset α) ∅ (Int.negSucc a) = ∅
⊢ HPow.hPow (α := Finset α) ∅ n = ∅

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

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
a : ℕ
hn : Int.negSucc a ≠ 0
⊢ HPow.hPow (α := Finset α) ∅ (Int.negSucc a) = ∅

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
simpa using hs.pow

Premises used: Finset.Nonempty.pow
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℤ
mp : s ^ n = ∅ → s = ∅ ∧ n ≠ 0
mpr : s = ∅ ∧ n ≠ 0 → s ^ n = ∅
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : DivisionMonoid α
s : Finset α
n : ℤ
mp : s.Nonempty ∨ n = 0 → (s ^ n).Nonempty
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib
-- 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:
hs.zpow

Premises used: Finset.Nonempty.zpow