awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Goal:
α : Type u_1
ι : Type u_2
inst : CommMonoid α
inst_1 : DecidableEq ι
inst_2 : InvolutiveNeg ι
s : Finset ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (∏ i ∈ -s, f i) (∏ i ∈ s, f (-i))

Tactic:
prod_image neg_injective.injOn

Premises used: Function.Injective.injOn, neg_injective, Finset.prod_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : DecidableEq ι
inst_2 : InvolutiveInv ι
s : Finset ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (∑ i ∈ s⁻¹, f i) (∑ i ∈ s, f i⁻¹)

Tactic:
sum_image inv_injective.injOn

Premises used: Function.Injective.injOn, Finset.sum_image, inv_injective
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Density
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : InvolutiveInv α
inst_2 : Fintype α
s : Finset α
⊢ s⁻¹.dens = s.dens

Tactic:
simp [dens]

Premises used: Finset.dens
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Density
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
inst_3 : Fintype β
a : α
s : Finset β
⊢ (a • s).dens = s.dens

Tactic:
simp [dens]

Premises used: Finset.dens
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : DecidableEq α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
inst_5 : LocallyFiniteOrder α
a b c d : α
⊢ (↑(Icc a b * Icc c d) : Set α) ⊆ (↑(Icc (a * c) (b * d)) : Set α)

Tactic:
simpa using Set.Icc_mul_Icc_subset' _ _ _ _

Premises used: Set.Icc_mul_Icc_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : DecidableEq α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
inst_5 : LocallyFiniteOrderBot α
a b : α
⊢ (↑(Iic a * Iic b) : Set α) ⊆ (↑(Iic (a * b)) : Set α)

Tactic:
simpa using Set.Iic_mul_Iic_subset' _ _

Premises used: Set.Iic_mul_Iic_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : DecidableEq α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
inst_5 : LocallyFiniteOrderTop α
a b : α
⊢ (↑(Ici a * Ici b) : Set α) ⊆ (↑(Ici (a * b)) : Set α)

Tactic:
simpa using Set.Ici_mul_Ici_subset' _ _

Premises used: Set.Ici_mul_Ici_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrder α
a b c d : α
⊢ (↑(Icc a b * Ico c d) : Set α) ⊆ (↑(Ico (a * c) (b * d)) : Set α)

Tactic:
simpa using Set.Icc_mul_Ico_subset' _ _ _ _

Premises used: Set.Icc_mul_Ico_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrder α
a b c d : α
⊢ (↑(Ico a b * Icc c d) : Set α) ⊆ (↑(Ico (a * c) (b * d)) : Set α)

Tactic:
simpa using Set.Ico_mul_Icc_subset' _ _ _ _

Premises used: Set.Ico_mul_Icc_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrder α
a b c d : α
⊢ (↑(Ioc a b * Ico c d) : Set α) ⊆ (↑(Ioo (a * c) (b * d)) : Set α)

Tactic:
simpa using Set.Ioc_mul_Ico_subset' _ _ _ _

Premises used: Set.Ioc_mul_Ico_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrder α
a b c d : α
⊢ (↑(Ico a b * Ioc c d) : Set α) ⊆ (↑(Ioo (a * c) (b * d)) : Set α)

Tactic:
simpa using Set.Ico_mul_Ioc_subset' _ _ _ _

Premises used: Set.Ico_mul_Ioc_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrderBot α
a b : α
⊢ (↑(Iic a * Iio b) : Set α) ⊆ (↑(Iio (a * b)) : Set α)

Tactic:
simpa using Set.Iic_mul_Iio_subset' _ _

Premises used: Set.Iic_mul_Iio_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrderBot α
a b : α
⊢ (↑(Iio a * Iic b) : Set α) ⊆ (↑(Iio (a * b)) : Set α)

Tactic:
simpa using Set.Iio_mul_Iic_subset' _ _

Premises used: Set.Iio_mul_Iic_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrderTop α
a b : α
⊢ (↑(Ioi a * Ici b) : Set α) ⊆ (↑(Ioi (a * b)) : Set α)

Tactic:
simpa using Set.Ioi_mul_Ici_subset' _ _

Premises used: Set.Ioi_mul_Ici_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : DecidableEq α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
inst_5 : LocallyFiniteOrderTop α
a b : α
⊢ (↑(Ici a * Ioi b) : Set α) ⊆ (↑(Ioi (a * b)) : Set α)

Tactic:
simpa using Set.Ici_mul_Ioi_subset' _ _

Premises used: Set.Ici_mul_Ioi_subset'
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ (↑(s • t) : Set β) = (↑s : Set α) • (↑t : Set β)

Tactic:
coe_image₂ ..

Premises used: setOf, Finset.coe_image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ #(s • t) ≤ #s * #t

Tactic:
card_image₂_le ..

Premises used: Finset.card_image₂_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
t : Finset β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Finset α) ∅ t = ∅

Tactic:
image₂_empty_left

Premises used: Finset.image₂_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
⊢ HSMul.hSMul (β := Finset β) s ∅ = ∅

Tactic:
image₂_empty_right

Premises used: Finset.image₂_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ s • t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image₂_eq_empty_iff

Premises used: Finset.image₂_eq_empty_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ s.Nonempty → t.Nonempty → (s • t).Nonempty

Tactic:
.image₂

Premises used: Finset.Nonempty.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ (s • t).Nonempty → s.Nonempty

Tactic:
.of_image₂_left

Premises used: Finset.Nonempty.of_image₂_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ (s • t).Nonempty → t.Nonempty

Tactic:
.of_image₂_right

Premises used: Finset.Nonempty.of_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
b : β
⊢ HSMul.hSMul (β := Finset β) s {b} = image (fun (x : α) ↦ x • b) s

Tactic:
image₂_singleton_right

Premises used: Finset.image₂_singleton_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
b : β
⊢ HSMul.hSMul (α := Finset α) (β := Finset β) {a} {b} = {a • b}

Tactic:
image₂_singleton

Premises used: Finset.image₂_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t u : Finset β
⊢ s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u

Tactic:
image₂_subset_iff

Premises used: Set.Mem, setOf, Finset.image₂_subset_iff
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset α
t : Finset β
inst_2 : DecidableEq α
⊢ (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t

Tactic:
image₂_union_left

Premises used: Finset.image₂_union_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset α
t : Finset β
inst_2 : DecidableEq α
⊢ (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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
inst_2 : DecidableEq α
⊢ (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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
inst_2 : DecidableEq α
⊢ (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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
u : Finset β
s : Set α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
⊢ a • s = image (fun (x : β) ↦ a • x) s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
⊢ image (fun (x : β) ↦ a • x) s = a • s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
x : β
⊢ x ∈ a • s ↔ ∃ y ∈ s, a • y = x

Tactic:
simp only [Finset.smul_finset_def, mem_image]

Premises used: Finset.mem_image, Finset.smul_finset_def
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
s : Finset β
⊢ (↑(a • s) : Set β) = a • (↑s : Set β)

Tactic:
coe_image

Premises used: setOf, Finset.coe_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
b : β
⊢ b ∈ s → a • b ∈ a • s

Tactic:
mem_image_of_mem _

Premises used: Set.Mem, setOf, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
⊢ #(a • s) ≤ #s

Tactic:
card_image_le

Premises used: Finset.card_image_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
⊢ HSMul.hSMul (β := Finset β) a ∅ = ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, Multiset.ofList, List.pwFilter, List.foldr, Finset.image, rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
⊢ a • s = ∅ ↔ s = ∅

Tactic:
image_eq_empty

Premises used: Finset.image_eq_empty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
⊢ (a • s).Nonempty ↔ s.Nonempty

Tactic:
image_nonempty

Premises used: Finset.image_nonempty
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset β
a : α
hs : s.Nonempty
⊢ (a • s).Nonempty

Tactic:
hs.image _

Premises used: Finset.Nonempty.image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
t : Finset β
a : α
⊢ HSMul.hSMul (α := Finset α) {a} t = a • t

Tactic:
image₂_singleton_left

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s t : Finset β
a : α
⊢ s ⊆ t → a • s ⊆ a • t

Tactic:
image_subset_image

Premises used: Set.Mem, setOf, Finset.image_subset_image
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
b : β
⊢ HSMul.hSMul (β := Finset β) a {b} = {a • b}

Tactic:
image_singleton ..

Premises used: Finset.image_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset β
a : α
⊢ a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂

Tactic:
image_union _ _

Premises used: Finset.image_union
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
a : α
b : β
s : Finset β
⊢ a • insert b s = insert (a • b) (a • s)

Tactic:
image_insert ..

Premises used: Finset.image_insert
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s₁ s₂ : Finset β
a : α
⊢ a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ a • s₂

Tactic:
image_inter_subset _ _ _

Premises used: Set.Mem, setOf, Finset.image_inter_subset
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
t : Finset β
a : α
s : Finset α
⊢ a ∈ s → a • t ⊆ s • t

Tactic:
image_subset_image₂_right

Premises used: Set.Mem, setOf, Finset.image_subset_image₂_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : SMul α β
s : Finset α
t : Finset β
⊢ (s.biUnion fun (x : α) ↦ x • t) = s • t

Tactic:
biUnion_image_left

Premises used: Finset.biUnion_image_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t : Finset β
⊢ s -ᵥ t = image₂ (fun (x1 x2 : β) ↦ x1 -ᵥ x2) s t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t : Finset β
⊢ image₂ (fun (x1 x2 : β) ↦ x1 -ᵥ x2) s t = s -ᵥ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t : Finset β
b c : β
⊢ b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t

Tactic:
mem_image₂_of_mem

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

Tactic:
card_image₂_le _ _ _

Premises used: Finset.card_image₂_le
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
t : Finset β
⊢ ∅ -ᵥ t = ∅

Tactic:
image₂_empty_left

Premises used: Finset.image₂_empty_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s : Finset β
⊢ s -ᵥ ∅ = ∅

Tactic:
image₂_empty_right

Premises used: Finset.image₂_empty_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t : Finset β
⊢ s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty

Tactic:
Nonempty.image₂

Premises used: Finset.Nonempty.image₂
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s : Finset β
b : β
⊢ s -ᵥ {b} = image (fun (x : β) ↦ x -ᵥ b) s

Tactic:
image₂_singleton_right

Premises used: Finset.image₂_singleton_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
t : Finset β
a : β
⊢ {a} -ᵥ t = image (fun (x : β) ↦ a -ᵥ x) t

Tactic:
image₂_singleton_left

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
a b : β
⊢ VSub.vsub (P := Finset β) {a} {b} = {a -ᵥ b}

Tactic:
image₂_singleton

Premises used: Finset.image₂_singleton
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t : Finset β
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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s₁ s₂ t : Finset β
inst_2 : DecidableEq β
⊢ s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)

Tactic:
image₂_union_left

Premises used: Finset.image₂_union_left
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t₁ t₂ : Finset β
inst_2 : DecidableEq β
⊢ s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)

Tactic:
image₂_union_right

Premises used: Finset.image₂_union_right
-- Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s₁ s₂ t : Finset β
inst_2 : DecidableEq β
⊢ 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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
s t₁ t₂ : Finset β
inst_2 : DecidableEq β
⊢ 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.Scalar
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
inst_1 : DecidableEq α
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.Scalar
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq β
inst_1 : DecidableEq γ
inst_2 : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_3 : SMul β γ
inst_4 : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
h₁ : ∀ (a_1 : γ), a_1 ∈ (op a • s) • t ↔ a_1 ∈ s • a • t
⊢ (op a • s) • t = s • a • t

Tactic:
ext