awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
simp_rw : (↑s : Set α) • (↑t : Set β) • (↑u : Set γ) = (↑t : Set β) • (↑s : Set α) • (↑u : Set γ)
⊢ (↑(s • t • u) : Set γ) = (↑(t • s • u) : Set γ)

Tactic:
simp_rw [coe_smul, smul_comm]

Premises used: SMulCommClass.smul_comm, Finset.coe_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : SMul α β
inst_2 : SMul α γ
inst_3 : SMul β γ
inst_4 : IsScalarTower α β γ
a : α
b : β
s : Finset γ
⊢ (a • b) • s = a • b • s

Tactic:
simp only [← image_smul, image_image, smul_assoc, Function.comp_def]

Premises used: smul_assoc, Finset.image_smul, Function.comp_def, Finset.image_image
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : DecidableEq β
inst_2 : SMul α β
inst_3 : SMul α γ
inst_4 : SMul β γ
inst_5 : IsScalarTower α β γ
a : α
s : Finset β
t : Finset γ
⊢ (↑((a • s) • t) : Set γ) = (↑(a • s • t) : Set γ)

Tactic:
simp only [coe_smul_finset, coe_smul, smul_assoc]

Premises used: smul_assoc, Finset.coe_smul_finset, Finset.coe_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : DecidableEq β
inst_2 : SMul α β
inst_3 : SMul α γ
inst_4 : SMul β γ
inst_5 : IsScalarTower α β γ
a : Finset α
s : Finset β
t : Finset γ
⊢ (↑((a • s) • t) : Set γ) = (↑(a • s • t) : Set γ)

Tactic:
simp only [coe_smul, smul_assoc]

Premises used: smul_assoc, Finset.coe_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : DecidableEq β
inst_2 : SMul α β
inst_3 : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_4 : IsCentralScalar α β
a : α
s : Finset β
⊢ (↑(op a • s) : Set β) = (↑(a • s) : Set β)

Tactic:
simp only [coe_smul_finset, op_smul_eq_smul]

Premises used: Finset.coe_smul_finset, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : DecidableEq β
inst_2 : DecidableEq α
inst_3 : Monoid α
inst_4 : MulAction α β
s : Finset β
simp_rw : image (fun (b : β) ↦ b) s = s
⊢ image (fun (b : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 b) s = s

Tactic:
simp_rw [one_smul, image_id']

Premises used: one_smul, Finset.image_id'
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s : Finset α
a : α
⊢ s * {a} = s <• a

Tactic:
image₂_singleton_right

Premises used: Finset.image₂_singleton_right, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s : Finset α
a : α
⊢ {a} * s = a • s

Tactic:
image₂_singleton_left

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s t : Finset α
a : α
⊢ 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.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ t → op a • s ⊆ s * t

Tactic:
image_subset_image₂_left

Premises used: Set.Mem, setOf, Finset.image_subset_image₂_left, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s t : Finset α
⊢ (t.biUnion fun (a : α) ↦ op a • s) = s * t

Tactic:
biUnion_image_right

Premises used: Finset.biUnion_image_right, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s t u : Finset α
⊢ s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u

Tactic:
image₂_subset_iff_left

Premises used: Set.Mem, setOf, Finset.image₂_subset_iff_left
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Mul α
inst_1 : DecidableEq α
s t u : Finset α
⊢ s * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u

Tactic:
image₂_subset_iff_right

Premises used: Finset.image₂_subset_iff_right, Set.Mem, setOf, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Semigroup α
inst_1 : DecidableEq α
a : α
s t : Finset α
⊢ op a • s * t = s * a • t

Tactic:
op_smul_finset_smul_eq_smul_smul_finset _ _ _ fun _ _ _ => mul_assoc _ _ _

Premises used: mul_assoc, Finset.op_smul_finset_smul_eq_smul_smul_finset, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
inst_1 : IsLeftCancelSMul α β
inst_2 : DecidableEq β
s : Set α
t : Finset β
simp_rw :
  (Set.PairwiseDisjoint.{u_3, u_2} (α := Set β) s fun (i : α) ↦ (↑(i • t) : Set β)) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
simp_rw₁ :
  (Set.PairwiseDisjoint.{u_3, u_2} (α := Set β) s fun (i : α) ↦ i • (↑t : Set β)) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
⊢ (Set.PairwiseDisjoint.{u_3, u_2} (α := Finset β) s fun (x : α) ↦ x • t) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))

Tactic:
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]

Premises used: Finset.pairwiseDisjoint_coe, Finset.coe_smul_finset, Set.pairwiseDisjoint_smul_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Mul α
inst_3 : Mul β
inst_4 : FunLike F α β
inst_5 : MulHomClass F α β
f : F
a : α
s : Finset α
⊢ image (⇑f : (a : α) → β) (a • s) =
    HSMul.hSMul (α := β) (β := Finset β) ((f : (a : α) → β) a : β) (image (⇑f : (a : α) → β) s)

Tactic:
image_comm <| map_mul _ _

Premises used: Finset.image_comm, map_mul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
b : β
a : α
⊢ a • b ∈ a • s ↔ b ∈ s

Tactic:
(MulAction.injective _).mem_finset_image

Premises used: Set.Mem, setOf, Function.Injective.mem_finset_image, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a b : α
s : Finset α
⊢ a * b ∈ a • s ↔ b ∈ s

Tactic:
smul_mem_smul_finset_iff _

Premises used: Set.Mem, Finset.smul_mem_smul_finset_iff, setOf
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
rw : a • a⁻¹ • b ∈ a • s ↔ b ∈ a • s
rw₁ rw₂ : b ∈ a • s ↔ b ∈ a • s
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s

Tactic:
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

Premises used: Finset.smul_mem_smul_finset_iff, smul_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
rw : a • b ∈ a • a⁻¹ • s ↔ a • b ∈ s
rw₁ rw₂ : a • b ∈ s ↔ a • b ∈ s
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s

Tactic:
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

Premises used: Finset.smul_mem_smul_finset_iff, smul_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ a • s ⊆ a • t ↔ s ⊆ t

Tactic:
image_subset_image_iff <| MulAction.injective _

Premises used: Set.Mem, Finset.image_subset_image_iff, setOf, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
push_cast : a • (↑s : Set β) ⊆ (↑t : Set β) ↔ (↑s : Set β) ⊆ a⁻¹ • (↑t : Set β)
⊢ (↑(a • s) : Set β) ⊆ (↑t : Set β) ↔ (↑s : Set β) ⊆ (↑(a⁻¹ • t) : Set β)

Tactic:
push_cast
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ a • (↑s : Set β) ⊆ (↑t : Set β) ↔ (↑s : Set β) ⊆ a⁻¹ • (↑t : Set β)

Tactic:
Set.smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ a • (↑s : Set β) ⊆ (↑t : Set β) ↔ (↑s : Set β) ⊆ a⁻¹ • (↑t : Set β)

Tactic:
exact Set.smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
push_cast : (↑s : Set β) ⊆ a • (↑t : Set β) ↔ a⁻¹ • (↑s : Set β) ⊆ (↑t : Set β)
⊢ (↑s : Set β) ⊆ (↑(a • t) : Set β) ↔ (↑(a⁻¹ • s) : Set β) ⊆ (↑t : Set β)

Tactic:
push_cast
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ (↑s : Set β) ⊆ a • (↑t : Set β) ↔ a⁻¹ • (↑s : Set β) ⊆ (↑t : Set β)

Tactic:
Set.subset_smul_set_iff

Premises used: Set.subset_smul_set_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ (↑s : Set β) ⊆ a • (↑t : Set β) ↔ a⁻¹ • (↑s : Set β) ⊆ (↑t : Set β)

Tactic:
exact Set.subset_smul_set_iff

Premises used: Set.subset_smul_set_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ a • (s ∩ t) = a • s ∩ a • t

Tactic:
image_inter _ _ <| MulAction.injective a

Premises used: Finset.image_inter, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ a • (s \ t) = a • s \ a • t

Tactic:
image_sdiff _ _ <| MulAction.injective a

Premises used: MulAction.injective, Finset.image_sdiff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s t : Finset β
a : α
⊢ a • s ∆ t = (a • s) ∆ (a • t)

Tactic:
image_symmDiff _ _ <| MulAction.injective a

Premises used: MulAction.injective, Finset.image_symmDiff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
a : α
inst_3 : Fintype β
⊢ HSMul.hSMul (β := Finset β) a univ = univ

Tactic:
image_univ_of_surjective <| MulAction.surjective a

Premises used: Finset.image_univ_of_surjective, MulAction.surjective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
s : Finset β
a : α
inst_3 : Fintype β
rw : s = HSMul.hSMul (β := Finset β) a⁻¹ univ ↔ s = univ
rw₁ rw₂ : s = univ ↔ s = univ
⊢ a • s = univ ↔ s = univ

Tactic:
rw [smul_eq_iff_eq_inv_smul, smul_finset_univ]

Premises used: Finset.smul_finset_univ, smul_eq_iff_eq_inv_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nonempty
push_cast : HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)

Tactic:
push_cast
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nonempty
⊢ HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ

Tactic:
Set.smul_univ hs

Premises used: Set.smul_univ
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nonempty
⊢ HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ

Tactic:
exact Set.smul_univ hs

Premises used: Set.smul_univ
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
a : α
s : Finset β
⊢ #(a • s) = #s

Tactic:
card_image_of_injective _ <| MulAction.injective _

Premises used: Finset.card_image_of_injective, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Group α
inst_2 : MulAction α β
t : Finset β
s : Finset α
⊢ Set.PairwiseDisjoint.{u_3, u_3} (α := Finset β) ((fun (x : α) ↦ x • t) '' (↑s : Set α)) id → #t ∣ #(s • t)

Tactic:
card_dvd_card_image₂_right fun _ _ => MulAction.injective _

Premises used: Finset.card_dvd_card_image₂_right, MulAction.injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
⊢ Set.PairwiseDisjoint (α := Finset α) ((fun (b : α) ↦ image (fun (a : α) ↦ a * b) s) '' (↑t : Set α)) id →
    #s ∣ #(s * t)

Tactic:
card_dvd_card_image₂_left fun _ _ => mul_left_injective _

Premises used: Finset.card_dvd_card_image₂_left, mul_left_injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
⊢ Set.PairwiseDisjoint (α := Finset α) ((fun (x : α) ↦ x • t) '' (↑s : Set α)) id → #t ∣ #(s * t)

Tactic:
card_dvd_card_image₂_right fun _ _ => mul_right_injective _

Premises used: Finset.card_dvd_card_image₂_right, mul_right_injective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a : α
s : Finset α
h : ∀ (a_1 : α), a_1 ∈ (a • s)⁻¹ ↔ a_1 ∈ op a⁻¹ • s⁻¹
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a : α
s : Finset α
a_1 : α
⊢ a_1 ∈ (a • s)⁻¹ ↔ a_1 ∈ op a⁻¹ • s⁻¹

Tactic:
simp [← inv_smul_mem_iff]

Premises used: Finset.inv_smul_mem_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a : α
s : Finset α
h : ∀ (a_1 : α), a_1 ∈ (op a • s)⁻¹ ↔ a_1 ∈ a⁻¹ • s⁻¹
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
a : α
s : Finset α
a_1 : α
⊢ a_1 ∈ (op a • s)⁻¹ ↔ a_1 ∈ a⁻¹ • s⁻¹

Tactic:
simp [← inv_smul_mem_iff]

Premises used: Finset.inv_smul_mem_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
ι : Type u_5
α : ι → Type u_6
β : ι → Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (β i)
inst_3 : (i : ι) → SMul.{u_6, u_7} (α i) (β i)
s : (i : ι) → Finset (α i)
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.Action.Pointwise.Finset
Goal:
ι : Type u_5
α : ι → Type u_6
β : ι → Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (β i)
inst_3 : (i : ι) → SMul.{u_6, u_7} (α i) (β i)
a : (i : ι) → α i
s : (i : ι) → Finset (β i)
⊢ (piFinset (δ := β) fun (i : ι) ↦ a i • s i) = a • piFinset (δ := β) s

Tactic:
piFinset_image _ _

Premises used: Fintype.piFinset_image
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ s
a n : ℕ
⊢ (∃ y ∈ s, a + y = n) ↔ a ≤ n ∧ n - a ∈ s

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
β : Type u_3
M : Type u_5
α : Type u_6
inst : SMul M α
inst_1 : SMul M β
c : M
s : Set α
t : Set β
⊢ c • s ×ˢ t = (c • s) ×ˢ (c • t)

Tactic:
prodMap_image_prod (c • ·) (c • ·) s t

Premises used: Set.prodMap_image_prod, Prod.map, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
G : Type u_5
ι : Type u_6
α : ι → Type u_7
inst : Group G
inst_1 : (i : ι) → MulAction.{u_5, u_7} G (α i)
c : G
I : Set ι
s : (i : ι) → Set (α i)
⊢ c • I.pi (α := α) s = I.pi (α := α) (c • s)

Tactic:
smul_set_pi_of_surjective c I s fun _ _ ↦ (MulAction.bijective c).surjective

Premises used: MulAction.bijective, Set.smul_set_pi_of_surjective, Function.Bijective.surjective
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst : Monoid M
inst_1 : (i : ι) → MulAction.{u_5, u_7} M (α i)
c : M
hc : IsUnit c
I : Set ι
s : (i : ι) → Set (α i)
⊢ IsUnit c

Tactic:
hc
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst : Monoid M
inst_1 : (i : ι) → MulAction.{u_5, u_7} M (α i)
c : M
hc : IsUnit c
I : Set ι
s : (i : ι) → Set (α i)
lift : ∀ (c : Mˣ), (↑c : M) • I.pi (α := α) s = I.pi (α := α) ((↑c : M) • s)
⊢ c • I.pi (α := α) s = I.pi (α := α) (c • s)

Tactic:
lift c to Mˣ using hc
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst : Monoid M
inst_1 : (i : ι) → MulAction.{u_5, u_7} M (α i)
I : Set ι
s : (i : ι) → Set (α i)
c : Mˣ
⊢ (↑c : M) • I.pi (α := α) s = I.pi (α := α) ((↑c : M) • s)

Tactic:
smul_set_pi c I s

Premises used: Set.smul_set_pi
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst : Monoid M
inst_1 : (i : ι) → MulAction.{u_5, u_7} M (α i)
I : Set ι
s : (i : ι) → Set (α i)
c : Mˣ
⊢ (↑c : M) • I.pi (α := α) s = I.pi (α := α) ((↑c : M) • s)

Tactic:
exact smul_set_pi c I s

Premises used: Set.smul_set_pi
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
a : α
⊢ a ∈ s → a • t ⊆ s * t

Tactic:
image_subset_image2_right

Premises used: Set.image_subset_image2_right
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
a : α
⊢ a ∈ t → s <• a ⊆ s * t

Tactic:
image_subset_image2_left

Premises used: Set.image_subset_image2_left, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
rw : Eq (α := Set α) (image2 (fun (a b : α) ↦ op b • a) t s) (image2 (fun (x1 x2 : α) ↦ x1 * x2) t s)
⊢ op '' s • t = t * s

Tactic:
rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]

Premises used: Set.image2_image_left, Set.image2_mul, Set.image2_smul, Set.image2_swap
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ Eq (α := Set α) (image2 (fun (a b : α) ↦ op b • a) t s) (image2 (fun (x1 x2 : α) ↦ x1 * x2) t s)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t : Set α
⊢ ⋃ a ∈ t, op a • s = s * t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t u : Set α
⊢ s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u

Tactic:
image2_subset_iff_left

Premises used: Set.image2_subset_iff_left
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s t u : Set α
⊢ s * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u

Tactic:
image2_subset_iff_right

Premises used: Set.image2_subset_iff_right, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
a b : α
s : Set α
rw : (fun (x : α) ↦ a * x) '' s ∪ (fun (x : α) ↦ b * x) '' s = a • s ∪ b • s
⊢ {a, b} * s = a • s ∪ b • s

Tactic:
rw [insert_eq, union_mul, singleton_mul, singleton_mul]

Premises used: Set.union_mul, Set.insert_eq, Set.singleton_mul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
a b : α
s : Set α
⊢ (fun (x : α) ↦ a * x) '' s ∪ (fun (x : α) ↦ b * x) '' s = a • s ∪ b • s

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s : Set α
a b : α
rw : (fun (x : α) ↦ x * a) '' s ∪ (fun (x : α) ↦ x * b) '' s = s <• a ∪ s <• b
⊢ s * {a, b} = s <• a ∪ s <• b

Tactic:
rw [insert_eq, mul_union, mul_singleton, mul_singleton]

Premises used: Set.insert_eq, Set.mul_singleton, Set.mul_union
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
s : Set α
a b : α
⊢ (fun (x : α) ↦ x * a) '' s ∪ (fun (x : α) ↦ x * b) '' s = s <• a ∪ s <• b

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Mul α
ι : Sort u_7
a : α
f : ι → α
⊢ (range fun (i : ι) ↦ a * f i) = a •> range f

Tactic:
range_smul a f

Premises used: Set.range_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
a : α
s : Set α
⊢ (⇑f : (a : α) → β) '' (a • s) = HSMul.hSMul (α := β) (β := Set β) ((f : (a : α) → β) a : β) ((⇑f : (a : α) → β) '' s)

Tactic:
image_comm <| map_mul _ _

Premises used: map_mul, Set.image_comm
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
f : F
a : α
s : Set α
⊢ (⇑f : (a : α) → β) '' (s <• a) = (⇑f : (a : α) → β) '' s <• (f : (a : α) → β) a

Tactic:
image_comm fun _ ↦ map_mul ..

Premises used: map_mul, MulOpposite.unop, MulOpposite.op, Set.image_comm
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
inst : Semigroup α
a : α
s t : Set α
⊢ op a • s * t = s * a • t

Tactic:
op_smul_set_smul_eq_smul_smul_set _ _ _ fun _ _ _ => mul_assoc _ _ _

Premises used: Set.op_smul_set_smul_eq_smul_smul_set, mul_assoc, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
inst_1 : IsLeftCancelSMul α β
s : Set α
t : Set β
⊢ (PairwiseDisjoint.{u_3, u_2} (α := Set β) s fun (x : α) ↦ x • t) ↔
    InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ t)

Tactic:
pairwiseDisjoint_image_right_iff fun a _ _ _ h ↦ IsLeftCancelSMul.left_cancel a _ _ h

Premises used: IsLeftCancelSMul.left_cancel, Set.pairwiseDisjoint_image_right_iff
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} α β (Set γ)

Tactic:
⟨fun _ _ ↦ Commute.set_image <| smul_comm _ _⟩

Premises used: Function.Commute.set_image, SMulCommClass.smul_comm, SMulCommClass.mk
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} α (Set β) (Set γ)

Tactic:
⟨fun _ _ _ ↦ image_image2_distrib_right <| smul_comm _⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Set.image_image2_distrib_right
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} (Set α) β (Set γ)

Tactic:
haveI := SMulCommClass.symm α β γ
  SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm, Set
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} (Set α) (Set β) (Set γ)

Tactic:
⟨fun _ _ _ ↦ image2_left_comm smul_comm⟩

Premises used: Set.image2_left_comm, SMulCommClass.smul_comm, SMulCommClass.mk