awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
⊢ #s⁻¹ = #s

Tactic:
card_image_of_injective _ inv_injective

Premises used: Finset.card_image_of_injective, inv_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
rw : (fun (x : α) ↦ x⁻¹) ⁻¹' (↑s : Set α) = (↑s⁻¹ : Set α)
rw₁ : (↑s : Set α)⁻¹ = (↑s⁻¹ : Set α)
rw₂ rw₃ : (↑s : Set α)⁻¹ = (↑s : Set α)⁻¹
⊢ (↑(s.preimage (fun (x : α) ↦ x⁻¹) ⋯) : Set α) = (↑s⁻¹ : Set α)

Tactic:
rw [coe_preimage, Set.inv_preimage, coe_inv]

Premises used: Finset.coe_preimage, Finset.coe_inv, Set.inv_preimage
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
inst_2 : Fintype α
h : ∀ (a : α), Membership.mem (γ := Finset α) univ⁻¹ a ↔ Membership.mem (γ := Finset α) univ a
⊢ Eq.{u_2 + 1} (α := Finset α) univ⁻¹ univ

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
inst_2 : Fintype α
a : α
⊢ Membership.mem (γ := Finset α) univ⁻¹ a ↔ Membership.mem (γ := Finset α) univ a

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s t : Finset α
⊢ (↑(s ∩ t)⁻¹ : Set α) = (↑(s⁻¹ ∩ t⁻¹) : Set α)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : InvolutiveInv α
inst_2 : DecidableEq β
inst_3 : InvolutiveInv β
s : Finset α
t : Finset β
⊢ (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹

Tactic:
mod_cast (s : Set α).inv_prod (t : Set β)

Premises used: SProd.sprod, congrArg, SetLike.coe_set_eq._simp_1, cast, Set.inv_prod, Inv.inv, SetLike.coe, congr, Finset.coe_inv._simp_1, Finset.coe_product._simp_1, Eq, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ s * t = image (fun (p : α × α) ↦ p.1 * p.2) (s ×ˢ t)

Tactic:
rfl

Premises used: Multiset.toFinset, Finset.image, rfl, Finset.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ image (fun (x : α × α) ↦ x.1 * x.2) (s ×ˢ t) = s * t

Tactic:
rfl

Premises used: Multiset.toFinset, Finset.image, rfl, Finset.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
x : α
⊢ x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
mem_image₂

Premises used: Set.Mem, setOf, Finset.mem_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ (↑(s * t) : Set α) = (↑s : Set α) * (↑t : Set α)

Tactic:
coe_image₂ _ _ _

Premises used: setOf, Finset.coe_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
a b : α
⊢ a ∈ s → b ∈ t → a * b ∈ s * t

Tactic:
mem_image₂_of_mem

Premises used: Set.Mem, setOf, Finset.mem_image₂_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ #(s * t) ≤ #s * #t

Tactic:
card_image₂_le _ _ _

Premises used: Finset.card_image₂_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ #(s * t) = #s * #t ↔ Set.InjOn (β := α) (fun (p : α × α) ↦ p.1 * p.2) ((↑s : Set α) ×ˢ (↑t : Set α))

Tactic:
card_image₂_iff

Premises used: Finset.card_image₂_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
⊢ ∅ * s = ∅

Tactic:
image₂_empty_left

Premises used: Finset.image₂_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
⊢ s * ∅ = ∅

Tactic:
image₂_empty_right

Premises used: Finset.image₂_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ s * t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image₂_eq_empty_iff

Premises used: Finset.image₂_eq_empty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image₂_nonempty_iff

Premises used: Finset.image₂_nonempty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ s.Nonempty → t.Nonempty → (s * t).Nonempty

Tactic:
Nonempty.image₂

Premises used: Finset.Nonempty.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ (s * t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image₂_left

Premises used: Finset.Nonempty.of_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ (s * t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image₂_right

Premises used: Finset.Nonempty.of_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
a b : α
⊢ HMul.hMul (α := Finset α) {a} {b} = {a * b}

Tactic:
image₂_singleton

Premises used: Finset.image₂_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t₁ t₂ : Finset α
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ * t₁ ⊆ s₂ * t₂

Tactic:
image₂_subset

Premises used: Set.Mem, setOf, Finset.image₂_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t₁ t₂ : Finset α
⊢ t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂

Tactic:
image₂_subset_left

Premises used: Set.Mem, setOf, Finset.image₂_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t : Finset α
⊢ s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t

Tactic:
image₂_subset_right

Premises used: Set.Mem, setOf, Finset.image₂_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
⊢ s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u

Tactic:
image₂_subset_iff

Premises used: Set.Mem, setOf, Finset.image₂_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t : Finset α
⊢ (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t

Tactic:
image₂_union_left

Premises used: Finset.image₂_union_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t₁ t₂ : Finset α
⊢ s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂

Tactic:
image₂_union_right

Premises used: Finset.image₂_union_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t : Finset α
⊢ s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)

Tactic:
image₂_inter_subset_left

Premises used: Set.Mem, setOf, Finset.image₂_inter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t₁ t₂ : Finset α
⊢ s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)

Tactic:
image₂_inter_subset_right

Premises used: Set.Mem, setOf, Finset.image₂_inter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t₁ t₂ : Finset α
⊢ s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

Tactic:
image₂_inter_union_subset_union

Premises used: Set.Mem, setOf, Finset.image₂_inter_union_subset_union
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t₁ t₂ : Finset α
⊢ (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

Tactic:
image₂_union_inter_subset_union

Premises used: Set.Mem, setOf, Finset.image₂_union_inter_subset_union
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
u : Finset α
s t : Set α
⊢ (↑u : Set α) ⊆ s * t → ∃ (s' : Finset α) (t' : Finset α), (↑s' : Set α) ⊆ s ∧ (↑t' : Set α) ⊆ t ∧ u ⊆ s' * t'

Tactic:
subset_set_image₂

Premises used: Set.Mem, setOf, Finset.subset_set_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Mul α
inst_2 : Mul β
inst_3 : FunLike F α β
inst_4 : MulHomClass F α β
f : F
s t : Finset α
inst_5 : DecidableEq β
⊢ image (⇑f : (a : α) → β) (s * t) = HMul.hMul (α := Finset β) (image (⇑f : (a : α) → β) s) (image (⇑f : (a : α) → β) t)

Tactic:
image_image₂_distrib <| map_mul f

Premises used: map_mul, Finset.image_image₂_distrib
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ image op (s * t) = image op t * image op s

Tactic:
image_image₂_antidistrib op_mul

Premises used: Finset.image_image₂_antidistrib, MulOpposite.op_mul
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Mul α
inst_2 : Mul β
inst_3 : DecidableEq β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
mod_cast (s₁ : Set α).prod_mul_prod_comm s₂ (t₁ : Set β) t₂

Premises used: HMul.hMul, SProd.sprod, congrArg, SetLike.coe_set_eq._simp_1, cast, Set.prod_mul_prod_comm, Finset.coe_mul._simp_1, SetLike.coe, congr, Finset.coe_product._simp_1, Eq, Eq.trans
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ map (Equiv.toEmbedding opEquiv) (s * t) = map (Equiv.toEmbedding opEquiv) t * map (Equiv.toEmbedding opEquiv) s

Tactic:
simp [map_eq_image, image_op_mul]

Premises used: Finset.image_op_mul, Finset.map_eq_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
⊢ Eq (α := (a : α) → Finset α) (⇑singletonMulHom : (a : α) → Finset α) singleton

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
a : α
⊢ Eq (α := Finset α) ((singletonMulHom : (a : α) → Finset α) a : Finset α) ({a} : Finset α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
β : Type u_5
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s t : Finset α
f : α → β
a : β
⊢ (s * t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a

Tactic:
sup_image₂_le

Premises used: Finset.sup_image₂_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
β : Type u_5
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s t : Finset α
f : α → β
⊢ (s * t).sup f = s.sup fun (x : α) ↦ t.sup fun (x_1 : α) ↦ f (x * x_1)

Tactic:
sup_image₂_left ..

Premises used: Finset.sup_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
β : Type u_5
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s t : Finset α
f : α → β
⊢ (s * t).sup f = t.sup fun (y : α) ↦ s.sup fun (x : α) ↦ f (x * y)

Tactic:
sup_image₂_right ..

Premises used: Finset.sup_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
β : Type u_5
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s t : Finset α
f : α → β
a : β
⊢ a ≤ (s * t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)

Tactic:
le_inf_image₂

Premises used: Finset.le_inf_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
β : Type u_5
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s t : Finset α
f : α → β
⊢ (s * t).inf f = s.inf fun (x : α) ↦ t.inf fun (x_1 : α) ↦ f (x * x_1)

Tactic:
inf_image₂_left ..

Premises used: Finset.inf_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
β : Type u_5
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s t : Finset α
f : α → β
⊢ (s * t).inf f = t.inf fun (y : α) ↦ s.inf fun (x : α) ↦ f (x * y)

Tactic:
inf_image₂_right ..

Premises used: Finset.inf_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
a : α
has : a ∈ s
ha : IsLeftRegular a
⊢ #t ≤ #(s * t)

Tactic:
card_le_card_image₂_left _ has ha

Premises used: Finset.card_le_card_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
a : α
hat : a ∈ t
ha : IsRightRegular a
⊢ #s ≤ #(s * t)

Tactic:
card_le_card_image₂_right _ hat ha

Premises used: Finset.card_le_card_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ s / t = image (fun (p : α × α) ↦ p.1 / p.2) (s ×ˢ t)

Tactic:
rfl

Premises used: Multiset.toFinset, Finset.image, rfl, Finset.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ image (fun (x : α × α) ↦ x.1 / x.2) (s ×ˢ t) = s / t

Tactic:
rfl

Premises used: Multiset.toFinset, Finset.image, rfl, Finset.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
a : α
⊢ a ∈ s / t ↔ ∃ b ∈ s, ∃ c ∈ t, b / c = a

Tactic:
mem_image₂

Premises used: Set.Mem, setOf, Finset.mem_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ (↑(s / t) : Set α) = (↑s : Set α) / (↑t : Set α)

Tactic:
coe_image₂ _ _ _

Premises used: setOf, Finset.coe_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
a b : α
⊢ a ∈ s → b ∈ t → a / b ∈ s / t

Tactic:
mem_image₂_of_mem

Premises used: Set.Mem, setOf, Finset.mem_image₂_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ #(s / t) ≤ #s * #t

Tactic:
card_image₂_le _ _ _

Premises used: Finset.card_image₂_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s : Finset α
⊢ ∅ / s = ∅

Tactic:
image₂_empty_left

Premises used: Finset.image₂_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s : Finset α
⊢ s / ∅ = ∅

Tactic:
image₂_empty_right

Premises used: Finset.image₂_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ s / t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image₂_eq_empty_iff

Premises used: Finset.image₂_eq_empty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image₂_nonempty_iff

Premises used: Finset.image₂_nonempty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ s.Nonempty → t.Nonempty → (s / t).Nonempty

Tactic:
Nonempty.image₂

Premises used: Finset.Nonempty.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ (s / t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image₂_left

Premises used: Finset.Nonempty.of_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t : Finset α
⊢ (s / t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image₂_right

Premises used: Finset.Nonempty.of_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s : Finset α
a : α
⊢ s / {a} = image (fun (x : α) ↦ x / a) s

Tactic:
image₂_singleton_right

Premises used: Finset.image₂_singleton_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s : Finset α
a : α
⊢ {a} / s = image (fun (x : α) ↦ a / x) s

Tactic:
image₂_singleton_left

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
a b : α
⊢ HDiv.hDiv (α := Finset α) {a} {b} = {a / b}

Tactic:
image₂_singleton

Premises used: Finset.image₂_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s₁ s₂ t₁ t₂ : Finset α
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ / t₁ ⊆ s₂ / t₂

Tactic:
image₂_subset

Premises used: Set.Mem, setOf, Finset.image₂_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t₁ t₂ : Finset α
⊢ t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂

Tactic:
image₂_subset_left

Premises used: Set.Mem, setOf, Finset.image₂_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s₁ s₂ t : Finset α
⊢ s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t

Tactic:
image₂_subset_right

Premises used: Set.Mem, setOf, Finset.image₂_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t u : Finset α
⊢ s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u

Tactic:
image₂_subset_iff

Premises used: Set.Mem, setOf, Finset.image₂_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s₁ s₂ t : Finset α
⊢ (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t

Tactic:
image₂_union_left

Premises used: Finset.image₂_union_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t₁ t₂ : Finset α
⊢ s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂

Tactic:
image₂_union_right

Premises used: Finset.image₂_union_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s₁ s₂ t : Finset α
⊢ s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)

Tactic:
image₂_inter_subset_left

Premises used: Set.Mem, setOf, Finset.image₂_inter_subset_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s t₁ t₂ : Finset α
⊢ s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)

Tactic:
image₂_inter_subset_right

Premises used: Set.Mem, setOf, Finset.image₂_inter_subset_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s₁ s₂ t₁ t₂ : Finset α
⊢ s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

Tactic:
image₂_inter_union_subset_union

Premises used: Set.Mem, setOf, Finset.image₂_inter_union_subset_union
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
s₁ s₂ t₁ t₂ : Finset α
⊢ (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

Tactic:
image₂_union_inter_subset_union

Premises used: Set.Mem, setOf, Finset.image₂_union_inter_subset_union
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Div α
u : Finset α
s t : Set α
⊢ (↑u : Set α) ⊆ s / t → ∃ (s' : Finset α) (t' : Finset α), (↑s' : Set α) ⊆ s ∧ (↑t' : Set α) ⊆ t ∧ u ⊆ s' / t'

Tactic:
subset_set_image₂

Premises used: Set.Mem, setOf, Finset.subset_set_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Div α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s t : Finset α
f : α → β
a : β
⊢ (s / t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x / y) ≤ a

Tactic:
sup_image₂_le

Premises used: Finset.sup_image₂_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Div α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s t : Finset α
f : α → β
⊢ (s / t).sup f = s.sup fun (x : α) ↦ t.sup fun (x_1 : α) ↦ f (x / x_1)

Tactic:
sup_image₂_left ..

Premises used: Finset.sup_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Div α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
s t : Finset α
f : α → β
⊢ (s / t).sup f = t.sup fun (y : α) ↦ s.sup fun (x : α) ↦ f (x / y)

Tactic:
sup_image₂_right ..

Premises used: Finset.sup_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Div α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s t : Finset α
f : α → β
a : β
⊢ a ≤ (s / t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y)

Tactic:
le_inf_image₂

Premises used: Finset.le_inf_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Div α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s t : Finset α
f : α → β
⊢ (s / t).inf f = s.inf fun (x : α) ↦ t.inf fun (x_1 : α) ↦ f (x / x_1)

Tactic:
inf_image₂_left ..

Premises used: Finset.inf_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Div α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
s t : Finset α
f : α → β
⊢ (s / t).inf f = t.inf fun (y : α) ↦ s.inf fun (x : α) ↦ f (x / y)

Tactic:
inf_image₂_right ..

Premises used: Finset.inf_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CommSemigroup α
s t : Finset α
⊢ s ∩ t * (s ∪ t) ⊆ s * t

Tactic:
image₂_inter_union_subset mul_comm

Premises used: Set.Mem, setOf, Finset.image₂_inter_union_subset, mul_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CommSemigroup α
s t : Finset α
⊢ (s ∪ t) * (s ∩ t) ⊆ s * t

Tactic:
image₂_union_inter_subset mul_comm

Premises used: Set.Mem, setOf, Finset.image₂_union_inter_subset, mul_comm
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : MulOneClass α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s * t

Tactic:
fun a ha =>
  mem_mul.2 ⟨a, ha, 1, ht, mul_one _⟩

Premises used: Iff.mpr, 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 : MulOneClass α
s t : Finset α
hs : 1 ∈ s
⊢ t ⊆ s * t

Tactic:
fun a ha =>
  mem_mul.2 ⟨1, hs, a, ha, one_mul _⟩

Premises used: Iff.mpr, 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 : MulOneClass α
⊢ Eq (α := (a : α) → Finset α) (⇑singletonMonoidHom : (a : α) → Finset α) singleton

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : MulOneClass α
a : α
⊢ Eq (α := Finset α) ((singletonMonoidHom : (a : α) → Finset α) a : Finset α) ({a} : Finset α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : MulOneClass α
⊢ Eq (α := (a : Finset α) → Set α) (⇑coeMonoidHom : (a : Finset α) → Set α) SetLike.coe

Tactic:
rfl

Premises used: setOf, Multiset.Mem, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : MulOneClass α
s : Finset α
⊢ (coeMonoidHom : (a : Finset α) → Set α) s = (↑s : Set α)

Tactic:
rfl

Premises used: setOf, Multiset.Mem, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
zero : (↑1 : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
zero₁ : (↑1 : Set α) = 1
zero₂ zero₃ : Eq.{u_2 + 1} (α := Set α) 1 1
⊢ (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0

Tactic:
rw [npowRec, pow_zero, coe_one]

Premises used: Finset.coe_one, npowRec, pow_zero