doc-next-gen

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Module docstring

{"# Pointwise actions on sets

This file proves that several kinds of actions of a type α on another type β transfer to actions of α/Set α on Set β.

Implementation notes

  • We put all instances in the locale Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp. ","### Translation/scaling of sets "}
Set.smul_set_prod theorem
{M α : Type*} [SMul M α] [SMul M β] (c : M) (s : Set α) (t : Set β) : c • (s ×ˢ t) = (c • s) ×ˢ (c • t)
Full source 
@[to_additive vadd_set_prod]
lemma smul_set_prod {M α : Type*} [SMul M α] [SMul M β] (c : M) (s : Set α) (t : Set β) :
    c • (s ×ˢ t) = (c • s) ×ˢ (c • t) :=
  prodMap_image_prod (c • ·) (c • ·) s t
Scalar Multiplication Distributes Over Cartesian Product of Sets
Informal description
Let $M$ be a type with a scalar multiplication action on types $\alpha$ and $\beta$. For any element $c \in M$, and any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the scalar multiplication of $c$ on the product set $s \times t$ is equal to the product of the scalar multiplications: $c \cdot (s \times t) = (c \cdot s) \times (c \cdot t)$.
Set.smul_set_pi theorem
{G ι : Type*} {α : ι → Type*} [Group G] [∀ i, MulAction G (α i)] (c : G) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s)
Full source 
@[to_additive]
lemma smul_set_pi {G ι : Type*} {α : ι → Type*} [Group G] [∀ i, MulAction G (α i)]
    (c : G) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s) :=
  smul_set_pi_of_surjective c I s fun _ _ ↦ (MulAction.bijective c).surjective
Scalar Multiplication Commutes with Product of Sets under Group Action
Informal description
Let $G$ be a group acting on a family of types $\alpha_i$ for $i \in \iota$. For any element $c \in G$, any subset $I \subseteq \iota$, and any family of subsets $s_i \subseteq \alpha_i$ for $i \in I$, the scalar multiplication of $c$ on the product set $\prod_{i \in I} s_i$ is equal to the product of the scalar multiplications: $c \cdot \prod_{i \in I} s_i = \prod_{i \in I} (c \cdot s_i)$.
Set.smul_set_pi_of_isUnit theorem
{M ι : Type*} {α : ι → Type*} [Monoid M] [∀ i, MulAction M (α i)] {c : M} (hc : IsUnit c) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s)
Full source 
@[to_additive]
lemma smul_set_pi_of_isUnit {M ι : Type*} {α : ι → Type*} [Monoid M] [∀ i, MulAction M (α i)]
    {c : M} (hc : IsUnit c) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s) := by
  lift c to Mˣ using hc
  exact smul_set_pi c I s
Scalar Multiplication Commutes with Product of Sets for Unit Elements
Informal description
Let $M$ be a monoid acting on a family of types $\alpha_i$ for $i \in \iota$. For any unit element $c \in M$ (i.e., $c$ is invertible), any subset $I \subseteq \iota$, and any family of subsets $s_i \subseteq \alpha_i$ for $i \in I$, the scalar multiplication of $c$ on the product set $\prod_{i \in I} s_i$ is equal to the product of the scalar multiplications: $c \cdot \prod_{i \in I} s_i = \prod_{i \in I} (c \cdot s_i)$.
Set.smul_set_subset_mul theorem
: a ∈ s → a • t ⊆ s * t
Full source 
@[to_additive] lemma smul_set_subset_mul : a ∈ s → a • t ⊆ s * t := image_subset_image2_right
Inclusion of Scalar Multiplication in Set Product: $a \in s \implies a \cdot t \subseteq s \cdot t$
Informal description
For any element $a$ in a set $s$ and any set $t$, the pointwise scalar multiplication $a \cdot t$ is a subset of the product set $s \cdot t$.
Set.image_op_smul theorem
: (op '' s) • t = t * s
Full source 
@[to_additive]
theorem image_op_smul : (opop '' s) • t = t * s := by
  rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]
  rfl
Equality between Opposite Scalar Multiplication and Set Multiplication
Informal description
For any sets $s$ and $t$ in a multiplicative structure, the image of $s$ under the opposite multiplication operation acting on $t$ is equal to the product $t * s$. That is, $(op \ '' \ s) \bullet t = t * s$.
Set.iUnion_op_smul_set theorem
(s t : Set α) : ⋃ a ∈ t, MulOpposite.op a • s = s * t
Full source 
@[to_additive (attr := simp)]
theorem iUnion_op_smul_set (s t : Set α) : ⋃ a ∈ t, MulOpposite.op a • s = s * t :=
  iUnion_image_right _
Union of Opposite Scalar Multiplications Equals Product Set
Informal description
For any sets $s$ and $t$ in a type $\alpha$ with a multiplicative action, the union over all $a \in t$ of the opposite scalar multiplication $\text{op}\, a \bullet s$ equals the product set $s * t$. In other words: \[ \bigcup_{a \in t} \text{op}\, a \bullet s = s * t \]
Set.mul_subset_iff_left theorem
: s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u
Full source 
@[to_additive]
theorem mul_subset_iff_left : s * t ⊆ us * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u :=
  image2_subset_iff_left
Left Multiplicative Subset Criterion: $s * t \subseteq u \iff \forall a \in s, a \bullet t \subseteq u$
Informal description
For sets $s, t, u$ in a type $\alpha$ with a multiplicative action, the product set $s * t$ is contained in $u$ if and only if for every element $a \in s$, the scaled set $a \bullet t$ is contained in $u$.
Set.mul_subset_iff_right theorem
: s * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u
Full source 
@[to_additive]
theorem mul_subset_iff_right : s * t ⊆ us * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u :=
  image2_subset_iff_right
Right Multiplicative Subset Criterion: $s * t \subseteq u \iff \forall b \in t, \text{op}\, b \bullet s \subseteq u$
Informal description
For sets $s, t, u$ in a type $\alpha$ with a multiplicative action, the product set $s * t$ is contained in $u$ if and only if for every element $b \in t$, the opposite scaled set $\text{op}\, b \bullet s$ is contained in $u$.
Set.pair_mul theorem
(a b : α) (s : Set α) : { a, b } * s = a • s ∪ b • s
Full source 
@[to_additive] lemma pair_mul (a b : α) (s : Set α) : {a, b} * s = a • s ∪ b • s := by
  rw [insert_eq, union_mul, singleton_mul, singleton_mul]; rfl
Product of Two-Element Set with Subset Equals Union of Scaled Sets
Informal description
For any elements $a, b$ in a type $\alpha$ and any subset $s \subseteq \alpha$, the product of the two-element set $\{a, b\}$ with $s$ is equal to the union of the scaled sets $a \bullet s$ and $b \bullet s$, i.e., $$ \{a, b\} * s = a \bullet s \cup b \bullet s. $$
Set.mul_pair theorem
(s : Set α) (a b : α) : s * { a, b } = s <• a ∪ s <• b
Full source 
@[to_additive] lemma mul_pair (s : Set α) (a b : α) : s * {a, b} = s <• as <• a ∪ s <• b := by
  rw [insert_eq, mul_union, mul_singleton, mul_singleton]; rfl
Pointwise multiplication of a set with a pair equals union of scalar multiplications
Informal description
For any set $s$ in a multiplicative structure $\alpha$ and any two elements $a, b \in \alpha$, the product of $s$ with the pair $\{a, b\}$ is equal to the union of the left scalar multiplication of $s$ by $a$ and the left scalar multiplication of $s$ by $b$. That is, $$ s * \{a, b\} = s \cdot a \cup s \cdot b $$ where $*$ denotes the pointwise multiplication of sets and $\cdot$ denotes the left scalar multiplication.
Set.range_mul theorem
{ι : Sort*} (a : α) (f : ι → α) : range (fun i ↦ a * f i) = a • range f
Full source 
@[to_additive] lemma range_mul {ι : Sort*} (a : α) (f : ι → α) :
    range (fun i ↦ a * f i) = a • range f := range_smul a f
Range of Scalar Multiplication Equals Scalar Multiplication of Range
Informal description
For any type $\alpha$ with a multiplication operation, any element $a \in \alpha$, and any function $f \colon \iota \to \alpha$, the range of the function $i \mapsto a \cdot f(i)$ is equal to the left scalar multiplication of $a$ on the range of $f$. That is, \[ \text{range} (\lambda i, a \cdot f(i)) = a \cdot \text{range}(f). \]
Set.image_smul_distrib theorem
[Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s : Set α) : f '' (a • s) = f a • f '' s
Full source 
@[to_additive]
lemma image_smul_distrib [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β]
    (f : F) (a : α) (s : Set α) :
    f '' (a • s) = f a • f '' s :=
  image_comm <| map_mul _ _
Image of Scalar Multiplication under Homomorphism Equals Scalar Multiplication of Image
Informal description
Let $\alpha$ and $\beta$ be types with multiplication operations, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve multiplication. For any homomorphism $f \in F$, any element $a \in \alpha$, and any subset $s \subseteq \alpha$, the image of the left scalar multiplication $a \cdot s$ under $f$ equals the left scalar multiplication of $f(a)$ on the image of $s$ under $f$. That is, $$ f(a \cdot s) = f(a) \cdot f(s). $$
Set.image_op_smul_distrib theorem
[Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s : Set α) : f '' (s <• a) = f '' s <• f a
Full source 
@[to_additive]
lemma image_op_smul_distrib [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β]
    (f : F) (a : α) (s : Set α) : f '' (s <• a) = f '' sf '' s <• f a := image_comm fun _ ↦ map_mul ..
Image of Right Scalar Multiplication under Homomorphism Equals Right Scalar Multiplication of Image
Informal description
Let $\alpha$ and $\beta$ be types equipped with multiplication operations, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve multiplication. For any homomorphism $f \colon \alpha \to \beta$ in $F$, any element $a \in \alpha$, and any subset $s \subseteq \alpha$, the image of the right scalar multiplication $s <\bullet a$ under $f$ is equal to the right scalar multiplication of the image $f(s)$ by $f(a)$. That is, \[ f(s <\bullet a) = f(s) <\bullet f(a). \]
Set.op_smul_set_mul_eq_mul_smul_set theorem
(a : α) (s : Set α) (t : Set α) : op a • s * t = s * a • t
Full source 
@[to_additive]
lemma op_smul_set_mul_eq_mul_smul_set (a : α) (s : Set α) (t : Set α) :
    op a • s * t = s * a • t :=
  op_smul_set_smul_eq_smul_smul_set _ _ _ fun _ _ _ => mul_assoc _ _ _
Equality of Opposite Scalar Action and Scalar Multiplication on Sets
Informal description
For any element $a$ in a type $\alpha$ with multiplication, and for any subsets $s$ and $t$ of $\alpha$, the left action of the opposite of $a$ on the product set $s \cdot t$ is equal to the product set $s \cdot (a \cdot t)$. In symbols, this is expressed as $(\text{op } a) \cdot (s \cdot t) = s \cdot (a \cdot t)$.
Set.pairwiseDisjoint_smul_iff theorem
: s.PairwiseDisjoint (· • t) ↔ (s ×ˢ t).InjOn fun p ↦ p.1 * p.2
Full source 
@[to_additive]
theorem pairwiseDisjoint_smul_iff :
    s.PairwiseDisjoint (· • t) ↔ (s ×ˢ t).InjOn fun p ↦ p.1 * p.2 :=
  pairwiseDisjoint_image_right_iff fun _ _ ↦ mul_right_injective _
Equivalence of Pairwise Disjoint Scalar Multiplications and Injectivity on Product Set
Informal description
Let $s$ be a set in a type $\alpha$ with a multiplication operation, and let $t$ be a set in $\alpha$. Then the following are equivalent: 1. The family of sets $\{a \cdot t\}_{a \in s}$ is pairwise disjoint. 2. The function $(a, b) \mapsto a \cdot b$ is injective on the product set $s \times t$.
Set.smulCommClass_set instance
[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Set γ)
Full source 
@[to_additive]
instance smulCommClass_set [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass α β (Set γ) :=
  ⟨fun _ _ ↦ Commute.set_image <| smul_comm _ _⟩
Commutativity of Scalar Actions on Sets
Informal description
For types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations $[\text{SMul } \alpha \gamma]$ and $[\text{SMul } \beta \gamma]$, if $\alpha$ and $\beta$ commute in their action on $\gamma$ (i.e., $[\text{SMulCommClass } \alpha \beta \gamma]$), then $\alpha$ and $\beta$ also commute in their action on sets of $\gamma$ (i.e., $\text{SMulCommClass } \alpha \beta (\text{Set } \gamma)$). This means that for any $a \in \alpha$, $b \in \beta$, and $S \subseteq \gamma$, we have $a \cdot (b \cdot S) = b \cdot (a \cdot S)$.
Set.smulCommClass_set' instance
[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Set β) (Set γ)
Full source 
@[to_additive]
instance smulCommClass_set' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass α (Set β) (Set γ) :=
  ⟨fun _ _ _ ↦ image_image2_distrib_right <| smul_comm _⟩
Commutation of Scalar Multiplication between $\alpha$ and $\text{Set } \beta$ on $\text{Set } \gamma$
Informal description
For types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations $[\text{SMul } \alpha \gamma]$ and $[\text{SMul } \beta \gamma]$, if $\alpha$ and $\beta$ commute in their action on $\gamma$ (i.e., $[\text{SMulCommClass } \alpha \beta \gamma]$), then $\alpha$ commutes with $\text{Set } \beta$ in their action on $\text{Set } \gamma$.
Set.smulCommClass_set'' instance
[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Set α) β (Set γ)
Full source 
@[to_additive]
instance smulCommClass_set'' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass (Set α) β (Set γ) :=
  haveI := SMulCommClass.symm α β γ
  SMulCommClass.symm _ _ _
Commutation of Scalar Multiplication between $\text{Set } \alpha$ and $\beta$ on $\text{Set } \gamma$
Informal description
For types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations $[\text{SMul } \alpha \gamma]$ and $[\text{SMul } \beta \gamma]$, if $\alpha$ and $\beta$ commute in their action on $\gamma$ (i.e., $[\text{SMulCommClass } \alpha \beta \gamma]$), then $\text{Set } \alpha$ commutes with $\beta$ in their action on $\text{Set } \gamma$.
Set.smulCommClass instance
[SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Set α) (Set β) (Set γ)
Full source 
@[to_additive]
instance smulCommClass [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass (Set α) (Set β) (Set γ) :=
  ⟨fun _ _ _ ↦ image2_left_comm smul_comm⟩
Commutation of Scalar Multiplication between Sets $\alpha$ and $\beta$ on Sets $\gamma$
Informal description
For types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations $[\text{SMul } \alpha \gamma]$ and $[\text{SMul } \beta \gamma]$, if $\alpha$ and $\beta$ commute in their action on $\gamma$ (i.e., $[\text{SMulCommClass } \alpha \beta \gamma]$), then $\text{Set } \alpha$ commutes with $\text{Set } \beta$ in their action on $\text{Set } \gamma$.
Set.isScalarTower instance
[SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Set γ)
Full source 
@[to_additive]
instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower α β (Set γ) where
  smul_assoc a b T := by simp only [← image_smul, image_image, smul_assoc]
Scalar Tower Action on Sets of $\gamma$
Informal description
For types $\alpha$, $\beta$, and $\gamma$ equipped with scalar multiplication operations, if $\alpha$ acts on $\beta$ and $\gamma$, and $\beta$ acts on $\gamma$ in a compatible way (forming a scalar tower), then $\alpha$ also acts on the set of $\gamma$ in a compatible way with the action of $\beta$ on $\gamma$.
Set.isScalarTower' instance
[SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Set β) (Set γ)
Full source 
@[to_additive]
instance isScalarTower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower α (Set β) (Set γ) :=
  ⟨fun _ _ _ ↦ image2_image_left_comm <| smul_assoc _⟩
Scalar Multiplication Tower Property for Power Sets
Informal description
For types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations $[\cdot : \alpha \times \beta \to \beta]$, $[\cdot : \alpha \times \gamma \to \gamma]$, and $[\cdot : \beta \times \gamma \to \gamma]$, if $\alpha$ acts on $\gamma$ through $\beta$ (i.e., the scalar multiplications satisfy the tower property $a \cdot (b \cdot c) = (a \cdot b) \cdot c$ for all $a \in \alpha$, $b \in \beta$, $c \in \gamma$), then $\alpha$ also acts on the power set of $\gamma$ through the power set of $\beta$ with the same tower property.
Set.isScalarTower'' instance
[SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Set α) (Set β) (Set γ)
Full source 
@[to_additive]
instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower (Set α) (Set β) (Set γ) where
  smul_assoc _ _ _ := image2_assoc smul_assoc
Tower Property for Set-valued Scalar Multiplication
Informal description
Given types $\alpha$, $\beta$, and $\gamma$ with scalar multiplication operations $[\cdot : \alpha \to \beta \to \beta]$, $[\cdot : \alpha \to \gamma \to \gamma]$, and $[\cdot : \beta \to \gamma \to \gamma]$, if $\alpha$ acts on $\gamma$ through $\beta$ (i.e., the scalar multiplication satisfies the tower property $a \cdot (b \cdot c) = (a \cdot b) \cdot c$ for all $a \in \alpha$, $b \in \beta$, $c \in \gamma$), then the induced scalar multiplications on sets $\text{Set } \alpha$, $\text{Set } \beta$, and $\text{Set } \gamma$ also satisfy the tower property.
Set.isCentralScalar instance
[SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Set β)
Full source 
@[to_additive]
instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :
    IsCentralScalar α (Set β) :=
  ⟨fun _ S ↦ (congr_arg fun f ↦ f '' S) <| funext fun _ ↦ op_smul_eq_smul _ _⟩
Central Scalar Multiplication on Power Sets
Informal description
For any scalar multiplication operation $\alpha$ on $\beta$ with an opposite scalar multiplication $\alpha^{\text{op}}$ on $\beta$ that is central (i.e., $a \cdot b = b \cdot a$ for all $a \in \alpha$ and $b \in \beta$), the induced scalar multiplication of $\alpha$ on the power set of $\beta$ is also central.
Set.mulAction definition
[Monoid α] [MulAction α β] : MulAction (Set α) (Set β)
Full source 
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of `Set α`
on `Set β`. -/
@[to_additive
"An additive action of an additive monoid `α` on a type `β` gives an additive action of `Set α`
on `Set β`"]
protected def mulAction [Monoid α] [MulAction α β] : MulAction (Set α) (Set β) where
  mul_smul _ _ _ := image2_assoc mul_smul
  one_smul s := image2_singleton_left.trans <| by simp_rw [one_smul, image_id']
Action of sets under a monoid action
Informal description
Given a monoid $\alpha$ acting on a type $\beta$, the set of elements of $\alpha$ acts on the set of elements of $\beta$ via the action defined by $A \cdot B = \{a \cdot b \mid a \in A, b \in B\}$ for any subsets $A \subseteq \alpha$ and $B \subseteq \beta$. This action satisfies the properties: 1. $(A \cdot B) \cdot C = A \cdot (B \cdot C)$ for any subsets $A, B \subseteq \alpha$ and $C \subseteq \beta$ 2. $\{1\} \cdot B = B$ for any subset $B \subseteq \beta$ (where $1$ is the identity element of $\alpha$)
Set.mulActionSet definition
[Monoid α] [MulAction α β] : MulAction α (Set β)
Full source 
/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Set β`. -/
@[to_additive
      "An additive action of an additive monoid on a type `β` gives an additive action on `Set β`."]
protected def mulActionSet [Monoid α] [MulAction α β] : MulAction α (Set β) where
  mul_smul _ _ _ := by simp only [← image_smul, image_image, ← mul_smul]
  one_smul _ := by simp only [← image_smul, one_smul, image_id']
Pointwise multiplicative action on power sets
Informal description
Given a monoid $\alpha$ acting on a type $\beta$, this defines a multiplicative action of $\alpha$ on the power set $\mathcal{P}(\beta)$ (the set of all subsets of $\beta$). The action is defined by pointwise multiplication: for $a \in \alpha$ and $S \subseteq \beta$, the action $a \cdot S$ is the set $\{a \cdot x \mid x \in S\}$.
Set.smul_mem_smul_set_iff theorem
: a • x ∈ a • s ↔ x ∈ s
Full source 
@[to_additive (attr := simp)]
theorem smul_mem_smul_set_iff : a • x ∈ a • sa • x ∈ a • s ↔ x ∈ s :=
  (MulAction.injective _).mem_set_image
Membership in Scaled Set: $a \cdot x \in a \cdot s \leftrightarrow x \in s$
Informal description
For any element $a$ in a monoid $\alpha$ acting on a type $\beta$, and for any element $x \in \beta$ and subset $s \subseteq \beta$, the element $a \cdot x$ belongs to the scaled set $a \cdot s$ if and only if $x$ belongs to $s$.
Set.mem_smul_set_iff_inv_smul_mem theorem
: x ∈ a • A ↔ a⁻¹ • x ∈ A
Full source 
@[to_additive]
theorem mem_smul_set_iff_inv_smul_mem : x ∈ a • Ax ∈ a • A ↔ a⁻¹ • x ∈ A :=
  show x ∈ MulAction.toPerm a '' Ax ∈ MulAction.toPerm a '' A ↔ _ from mem_image_equiv
Characterization of Membership in Scaled Set via Inverse Action: $x \in a \cdot A \leftrightarrow a^{-1} \cdot x \in A$
Informal description
For any element $a$ in a group $\alpha$ acting on a type $\beta$, any element $x \in \beta$, and any subset $A \subseteq \beta$, we have: \[ x \in a \cdot A \leftrightarrow a^{-1} \cdot x \in A. \]
Set.mem_inv_smul_set_iff theorem
: x ∈ a⁻¹ • A ↔ a • x ∈ A
Full source 
@[to_additive]
theorem mem_inv_smul_set_iff : x ∈ a⁻¹ • Ax ∈ a⁻¹ • A ↔ a • x ∈ A := by
  simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]
Characterization of Membership in Inversely Scaled Set: $x \in a^{-1} \cdot A \leftrightarrow a \cdot x \in A$
Informal description
For any element $a$ in a group $\alpha$ acting on a type $\beta$, and for any element $x \in \beta$ and subset $A \subseteq \beta$, the element $x$ belongs to the scaled set $a^{-1} \cdot A$ if and only if $a \cdot x$ belongs to $A$.
Set.mem_smul_set_inv theorem
{s : Set α} : a ∈ b • s⁻¹ ↔ b ∈ a • s
Full source 
@[to_additive (attr := simp)]
lemma mem_smul_set_inv {s : Set α} : a ∈ b • s⁻¹a ∈ b • s⁻¹ ↔ b ∈ a • s := by
  simp [mem_smul_set_iff_inv_smul_mem]
Membership in Scaled Inverse Set Equivalency
Informal description
For any elements $a, b$ in a division monoid $\alpha$ and any subset $s$ of $\alpha$, the element $a$ belongs to the scaled set $b \cdot s^{-1}$ if and only if $b$ belongs to the scaled set $a \cdot s$.
Set.preimage_smul theorem
(a : α) (t : Set β) : (fun x ↦ a • x) ⁻¹' t = a⁻¹ • t
Full source 
@[to_additive]
theorem preimage_smul (a : α) (t : Set β) : (fun x ↦ a • x) ⁻¹' t = a⁻¹ • t :=
  ((MulAction.toPerm a).symm.image_eq_preimage _).symm
Preimage of Scalar Multiplication Equals Inverse Scalar Multiplication of Set
Informal description
For any element $a$ in a group $\alpha$ acting on a type $\beta$, and for any subset $t \subseteq \beta$, the preimage of $t$ under the left scalar multiplication by $a$ is equal to the left scalar multiplication of $t$ by $a^{-1}$, i.e., \[ \{x \in \beta \mid a \cdot x \in t\} = a^{-1} \cdot t. \]
Set.preimage_smul_inv theorem
(a : α) (t : Set β) : (fun x ↦ a⁻¹ • x) ⁻¹' t = a • t
Full source 
@[to_additive]
theorem preimage_smul_inv (a : α) (t : Set β) : (fun x ↦ a⁻¹ • x) ⁻¹' t = a • t :=
  preimage_smul (toUnits a)⁻¹ t
Preimage of Inverse Scalar Multiplication Equals Scalar Multiplication of Set
Informal description
For any element $a$ in a group $\alpha$ acting on a type $\beta$, and for any subset $t \subseteq \beta$, the preimage of $t$ under the left scalar multiplication by $a^{-1}$ is equal to the left scalar multiplication of $t$ by $a$, i.e., \[ \{x \in \beta \mid a^{-1} \cdot x \in t\} = a \cdot t. \]
Set.smul_set_subset_smul_set_iff theorem
: a • A ⊆ a • B ↔ A ⊆ B
Full source 
@[to_additive (attr := simp)]
theorem smul_set_subset_smul_set_iff : a • A ⊆ a • Ba • A ⊆ a • B ↔ A ⊆ B :=
  image_subset_image_iff <| MulAction.injective _
Scalar Multiplication Preserves Subset Relation: $a \cdot A \subseteq a \cdot B \leftrightarrow A \subseteq B$
Informal description
For any element $a$ of a type $\alpha$ and any subsets $A, B$ of a type $\beta$, the subset relation $a \cdot A \subseteq a \cdot B$ holds if and only if $A \subseteq B$.
Set.smul_set_subset_iff_subset_inv_smul_set theorem
: a • A ⊆ B ↔ A ⊆ a⁻¹ • B
Full source 
@[to_additive]
theorem smul_set_subset_iff_subset_inv_smul_set : a • A ⊆ Ba • A ⊆ B ↔ A ⊆ a⁻¹ • B :=
  image_subset_iff.trans <|
    iff_of_eq <| congr_arg _ <| preimage_equiv_eq_image_symm _ <| MulAction.toPerm _
Scalar Multiplication Subset Relation: $a \cdot A \subseteq B \leftrightarrow A \subseteq a^{-1} \cdot B$
Informal description
For any element $a$ of a type $\alpha$ and any subsets $A \subseteq \beta$, $B \subseteq \beta$, the subset relation $a \cdot A \subseteq B$ holds if and only if $A \subseteq a^{-1} \cdot B$.
Set.subset_smul_set_iff theorem
: A ⊆ a • B ↔ a⁻¹ • A ⊆ B
Full source 
@[to_additive]
theorem subset_smul_set_iff : A ⊆ a • BA ⊆ a • B ↔ a⁻¹ • A ⊆ B :=
  Iff.symm <|
    image_subset_iff.trans <|
      Iff.symm <| iff_of_eq <| congr_arg _ <| image_equiv_eq_preimage_symm _ <| MulAction.toPerm _
Subset relation under scalar multiplication: $A \subseteq a \cdot B \leftrightarrow a^{-1} \cdot A \subseteq B$
Informal description
For any element $a$ of a type $\alpha$ and any subsets $A, B$ of a type $\beta$, the subset relation $A \subseteq a \cdot B$ holds if and only if $a^{-1} \cdot A \subseteq B$.
Set.smul_set_inter theorem
: a • (s ∩ t) = a • s ∩ a • t
Full source 
@[to_additive]
theorem smul_set_inter : a • (s ∩ t) = a • s ∩ a • t :=
  image_inter <| MulAction.injective a
Scalar Multiplication Distributes Over Set Intersection: $a \cdot (s \cap t) = (a \cdot s) \cap (a \cdot t)$
Informal description
For any scalar $a$ and sets $s$ and $t$ in a type $\beta$, the scalar multiplication of $a$ on the intersection $s \cap t$ is equal to the intersection of the scalar multiplications of $a$ on $s$ and $t$, i.e., $a \cdot (s \cap t) = (a \cdot s) \cap (a \cdot t)$.
Set.smul_set_iInter theorem
{ι : Sort*} (a : α) (t : ι → Set β) : (a • ⋂ i, t i) = ⋂ i, a • t i
Full source 
@[to_additive]
theorem smul_set_iInter {ι : Sort*}
    (a : α) (t : ι → Set β) : (a • ⋂ i, t i) = ⋂ i, a • t i :=
  image_iInter (MulAction.bijective a) t
Scalar Multiplication Distributes Over Arbitrary Intersections: $a \cdot \bigcap_i t_i = \bigcap_i (a \cdot t_i)$
Informal description
For any scalar $a$ in a type $\alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ in a type $\beta$, the scalar multiplication of $a$ with the intersection $\bigcap_{i \in \iota} t_i$ equals the intersection of the scalar multiplications $\bigcap_{i \in \iota} (a \cdot t_i)$. In other words, $a \cdot \left(\bigcap_{i \in \iota} t_i\right) = \bigcap_{i \in \iota} (a \cdot t_i)$.
Set.smul_set_sdiff theorem
: a • (s \ t) = a • s \ a • t
Full source 
@[to_additive]
theorem smul_set_sdiff : a • (s \ t) = a • s \ a • t :=
  image_diff (MulAction.injective a) _ _
Scalar Multiplication Distributes Over Set Difference: $a \cdot (s \setminus t) = (a \cdot s) \setminus (a \cdot t)$
Informal description
For any element $a$ of type $\alpha$ and any sets $s$ and $t$ of type $\beta$, the scalar multiplication of $a$ with the set difference $s \setminus t$ equals the set difference of the scalar multiplications $a \cdot s$ and $a \cdot t$, i.e., $a \cdot (s \setminus t) = (a \cdot s) \setminus (a \cdot t)$.
Set.smul_set_symmDiff theorem
: a • s ∆ t = (a • s) ∆ (a • t)
Full source 
@[to_additive]
theorem smul_set_symmDiff : a • s ∆ t = (a • s) ∆ (a • t) :=
  image_symmDiff (MulAction.injective a) _ _
Pointwise scalar multiplication distributes over symmetric difference of sets
Informal description
For any element $a$ of type $\alpha$ and any two sets $s, t$ of type $\beta$, the pointwise scalar multiplication of $a$ with the symmetric difference $s \mathbin{\Delta} t$ is equal to the symmetric difference of the pointwise scalar multiplications $a \cdot s$ and $a \cdot t$, i.e., \[ a \cdot (s \mathbin{\Delta} t) = (a \cdot s) \mathbin{\Delta} (a \cdot t). \]
Set.smul_set_univ theorem
: a • (univ : Set β) = univ
Full source 
@[to_additive (attr := simp)]
theorem smul_set_univ : a • (univ : Set β) = univ :=
  image_univ_of_surjective <| MulAction.surjective a
Scalar Multiplication Preserves Universal Set
Informal description
For any element $a$ of a type $\alpha$ and the universal set $\text{univ}$ of a type $\beta$, the scalar multiplication of $a$ with $\text{univ}$ equals $\text{univ}$, i.e., $a \cdot \text{univ} = \text{univ}$.
Set.smul_univ theorem
{s : Set α} (hs : s.Nonempty) : s • (univ : Set β) = univ
Full source 
@[to_additive (attr := simp)]
theorem smul_univ {s : Set α} (hs : s.Nonempty) : s • (univ : Set β) = univ :=
  let ⟨a, ha⟩ := hs
  eq_univ_of_forall fun b ↦ ⟨a, ha, a⁻¹ • b, trivial, smul_inv_smul _ _⟩
Pointwise Multiplication with Universal Set Preserves Universality
Informal description
For any nonempty set $s$ of type $\alpha$, the pointwise multiplication of $s$ with the universal set $\text{univ}$ of type $\beta$ equals $\text{univ}$, i.e., $s \cdot \text{univ} = \text{univ}$.
Set.smul_set_compl theorem
: a • sᶜ = (a • s)ᶜ
Full source 
@[to_additive]
theorem smul_set_compl : a • sᶜ = (a • s)ᶜ := by
  simp_rw [Set.compl_eq_univ_diff, smul_set_sdiff, smul_set_univ]
Scalar Multiplication Commutes with Set Complement: $a \cdot s^c = (a \cdot s)^c$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ of type $\beta$, the scalar multiplication of $a$ with the complement of $s$ equals the complement of the scalar multiplication of $a$ with $s$, i.e., $a \cdot s^c = (a \cdot s)^c$.
Set.smul_inter_ne_empty_iff theorem
{s t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Full source 
@[to_additive]
theorem smul_inter_ne_empty_iff {s t : Set α} {x : α} :
    x • s ∩ tx • s ∩ t ≠ ∅x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x := by
  rw [← nonempty_iff_ne_empty]
  constructor
  · rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩
  · rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
    exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩
Non-empty intersection condition for scaled set: $x \cdot s \cap t \neq \emptyset \leftrightarrow \exists a \in t, b \in s, a \cdot b^{-1} = x$
Informal description
For sets $s, t \subseteq \alpha$ and an element $x \in \alpha$, the intersection $x \cdot s \cap t$ is non-empty if and only if there exist elements $a \in t$ and $b \in s$ such that $a \cdot b^{-1} = x$.
Set.smul_inter_ne_empty_iff' theorem
{s t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
Full source 
@[to_additive]
theorem smul_inter_ne_empty_iff' {s t : Set α} {x : α} :
    x • s ∩ tx • s ∩ t ≠ ∅x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x := by
  simp_rw [smul_inter_ne_empty_iff, div_eq_mul_inv]
Nonempty Intersection Condition for Scaled Sets via Division
Informal description
For any sets $s, t \subseteq \alpha$ and any element $x \in \alpha$, the intersection of the scaled set $x \cdot s$ with $t$ is nonempty if and only if there exist elements $a \in t$ and $b \in s$ such that $a / b = x$.
Set.op_smul_inter_ne_empty_iff theorem
{s t : Set α} {x : αᵐᵒᵖ} : x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x
Full source 
@[to_additive]
theorem op_smul_inter_ne_empty_iff {s t : Set α} {x : αᵐᵒᵖ} :
    x • s ∩ tx • s ∩ t ≠ ∅x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x := by
  rw [← nonempty_iff_ne_empty]
  constructor
  · rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩
  · rintro ⟨a, b, ⟨ha, hb⟩, H⟩
    have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
    exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩
Nonempty Intersection Condition for Opposite Monoid Action: $x • s ∩ t \neq \emptyset \leftrightarrow \exists a \in s, b \in t, a^{-1}b = \text{unop}(x)$
Informal description
For any sets $s, t \subseteq \alpha$ and any element $x$ in the opposite monoid $\alpha^\text{op}$, the following are equivalent: 1. The intersection of the left action of $x$ on $s$ with $t$ is nonempty. 2. There exist elements $a \in s$ and $b \in t$ such that $a^{-1} * b = \text{unop}(x)$, where $\text{unop}$ is the operation that converts an element of $\alpha^\text{op}$ back to $\alpha$.
Set.iUnion_inv_smul theorem
: ⋃ g : α, g⁻¹ • s = ⋃ g : α, g • s
Full source 
@[to_additive (attr := simp)]
theorem iUnion_inv_smul : ⋃ g : α, g⁻¹ • s = ⋃ g : α, g • s :=
  (Function.Surjective.iSup_congr _ inv_surjective) fun _ ↦ rfl
Union of Inverse Translates Equals Union of Translates in Group Action
Informal description
For any set $s$ in a type $\alpha$ with a group action, the union of all translates $g^{-1} \cdot s$ for $g \in \alpha$ is equal to the union of all translates $g \cdot s$ for $g \in \alpha$. In other words: \[ \bigcup_{g \in \alpha} g^{-1} \cdot s = \bigcup_{g \in \alpha} g \cdot s \]
Set.iUnion_smul_eq_setOf_exists theorem
{s : Set β} : ⋃ g : α, g • s = {a | ∃ g : α, g • a ∈ s}
Full source 
@[to_additive]
theorem iUnion_smul_eq_setOf_exists {s : Set β} : ⋃ g : α, g • s = { a | ∃ g : α, g • a ∈ s } := by
  simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]
Union of Translates Equals Set of Elements with Preimage in Original Set
Informal description
For any set $s$ in a type $\beta$ acted upon by a type $\alpha$, the union of all translates $g \cdot s$ for $g \in \alpha$ is equal to the set of all elements $a \in \beta$ such that there exists $g \in \alpha$ with $g \cdot a \in s$. In other words: \[ \bigcup_{g \in \alpha} g \cdot s = \{a \in \beta \mid \exists g \in \alpha, g \cdot a \in s\} \]
Set.inv_smul_set_distrib theorem
(a : α) (s : Set α) : (a • s)⁻¹ = op a⁻¹ • s⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_smul_set_distrib (a : α) (s : Set α) : (a • s)⁻¹ = op a⁻¹ • s⁻¹ := by
  ext; simp [mem_smul_set_iff_inv_smul_mem]
Inverse of Scalar Multiplication on Sets in a Division Monoid
Informal description
For any element $a$ in a division monoid $\alpha$ and any subset $s$ of $\alpha$, the inverse of the set $a \cdot s$ is equal to the set $a^{-1} \cdot s^{-1}$ under the opposite multiplication operation. That is, $(a \cdot s)^{-1} = a^{-1} \cdot s^{-1}$.
Set.inv_op_smul_set_distrib theorem
(a : α) (s : Set α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_op_smul_set_distrib (a : α) (s : Set α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹ := by
  ext; simp [mem_smul_set_iff_inv_smul_mem]
Inverse of Opposite Action on Set Equals Inverse Action on Inverse Set
Informal description
For any element $a$ in a division monoid $\alpha$ and any subset $s$ of $\alpha$, the inverse of the set obtained by acting on $s$ with the opposite of $a$ is equal to the set obtained by acting on the inverse of $s$ with the inverse of $a$. In symbols: $$(a^{\text{op}} \cdot s)^{-1} = a^{-1} \cdot s^{-1}$$
Set.disjoint_smul_set theorem
: Disjoint (a • s) (a • t) ↔ Disjoint s t
Full source 
@[to_additive (attr := simp)]
lemma disjoint_smul_set : DisjointDisjoint (a • s) (a • t) ↔ Disjoint s t :=
  disjoint_image_iff <| MulAction.injective _
Disjointness Preservation under Scalar Multiplication: $a \cdot s \cap a \cdot t = \emptyset \iff s \cap t = \emptyset$
Informal description
For any element $a$ in a monoid $\alpha$ and any subsets $s, t$ of $\alpha$, the scalar multiple sets $a \cdot s$ and $a \cdot t$ are disjoint if and only if the original sets $s$ and $t$ are disjoint. That is: $$a \cdot s \cap a \cdot t = \emptyset \iff s \cap t = \emptyset$$
Set.disjoint_smul_set_left theorem
: Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)
Full source 
@[to_additive]
lemma disjoint_smul_set_left : DisjointDisjoint (a • s) t ↔ Disjoint s (a⁻¹ • t) := by
  simpa using disjoint_smul_set (a := a) (t := a⁻¹ • t)
Disjointness Equivalence under Left Scalar Multiplication and Inverse Action
Informal description
For any element $a$ in a division monoid $\alpha$ and any subsets $s, t$ of $\alpha$, the scalar multiple set $a \cdot s$ is disjoint from $t$ if and only if $s$ is disjoint from the scalar multiple set $a^{-1} \cdot t$. That is: $$a \cdot s \cap t = \emptyset \iff s \cap a^{-1} \cdot t = \emptyset$$
Set.disjoint_smul_set_right theorem
: Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t
Full source 
@[to_additive]
lemma disjoint_smul_set_right : DisjointDisjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t := by
  simpa using disjoint_smul_set (a := a) (s := a⁻¹ • s)
Disjointness Equivalence under Right Scalar Multiplication and Inverse Action
Informal description
For any element $a$ in a division monoid $\alpha$ and any subsets $s, t$ of $\alpha$, the set $s$ is disjoint from the scalar multiple set $a \cdot t$ if and only if the scalar multiple set $a^{-1} \cdot s$ is disjoint from $t$. That is: $$s \cap (a \cdot t) = \emptyset \iff (a^{-1} \cdot s) \cap t = \emptyset$$
Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul theorem
(s t : Set α) (a b : α) : ∃ z : α, a • s ∩ b • t ⊆ z • ((s⁻¹ * s) ∩ (t⁻¹ * t))
Full source 
/-- Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(s⁻¹ * s) ∩ (t⁻¹ * t)`.

This is useful to show that the intersection of approximate subgroups is an approximate subgroup. -/
@[to_additive
"Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(-s + s) ∩ (-t + t)`.

This is useful to show that the intersection of approximate subgroups is an approximate subgroup."]
lemma exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul (s t : Set α) (a b : α) :
    ∃ z : α, a • s ∩ b • t ⊆ z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by
  obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty
  · exact ⟨1, by simp [hAB]⟩
  refine ⟨z, ?_⟩
  calc
    a • s ∩ b • ta • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]
Covering Property for Intersections of Translated Sets: $a \cdot s \cap b \cdot t \subseteq z \cdot \big((s^{-1} \cdot s) \cap (t^{-1} \cdot t)\big)$
Informal description
For any subsets $s, t$ of a division monoid $\alpha$ and any elements $a, b \in \alpha$, there exists an element $z \in \alpha$ such that the intersection of the translates $a \cdot s$ and $b \cdot t$ is contained in the translate $z \cdot \big((s^{-1} \cdot s) \cap (t^{-1} \cdot t)\big)$.
Set.mem_invOf_smul_set theorem
[Invertible a] : b ∈ ⅟ a • s ↔ a • b ∈ s
Full source 
@[simp] lemma mem_invOf_smul_set [Invertible a] : b ∈ ⅟a • sb ∈ ⅟a • s ↔ a • b ∈ s :=
  mem_inv_smul_set_iff (a := unitOfInvertible a)
Characterization of Membership in Inversely Scaled Set via Invertible Element: $b \in \text{⅟}a \cdot s \leftrightarrow a \cdot b \in s$
Informal description
For an invertible element $a$ in a monoid $\alpha$ acting on a type $\beta$, and for any element $b \in \beta$ and subset $s \subseteq \beta$, the element $b$ belongs to the scaled set $\text{⅟}a \cdot s$ if and only if $a \cdot b$ belongs to $s$.
Set.smul_graphOn theorem
(x : α × β) (s : Set α) (f : F) : x • s.graphOn f = (x.1 • s).graphOn fun a ↦ x.2 / f x.1 * f a
Full source 
@[to_additive]
lemma smul_graphOn (x : α × β) (s : Set α) (f : F) :
    x • s.graphOn f = (x.1 • s).graphOn fun a ↦ x.2 / f x.1 * f a := by
  ext ⟨a, b⟩
  simp [mem_smul_set_iff_inv_smul_mem, Prod.ext_iff, and_comm (a := _ = a), inv_mul_eq_iff_eq_mul,
    mul_left_comm _ _⁻¹, eq_inv_mul_iff_mul_eq, ← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]
Action on Graph of Function over Scaled Set: $x \cdot \text{graph}(f|_s) = \text{graph}\left(a \mapsto \frac{x_2}{f(x_1)} \cdot f(a)\right)|_{x_1 \cdot s}$
Informal description
Let $\alpha$ and $\beta$ be types, $s \subseteq \alpha$ a subset, and $f \colon \alpha \to \beta$ a function. For any pair $x = (x_1, x_2) \in \alpha \times \beta$, the action of $x$ on the graph of $f$ over $s$ (i.e., $\{(a, f(a)) \mid a \in s\}$) is equal to the graph of the function $a \mapsto \frac{x_2}{f(x_1)} \cdot f(a)$ over the scaled set $x_1 \cdot s$.
Set.smul_graphOn_univ theorem
(x : α × β) (f : F) : x • univ.graphOn f = univ.graphOn fun a ↦ x.2 / f x.1 * f a
Full source 
@[to_additive]
lemma smul_graphOn_univ (x : α × β) (f : F) :
    x • univ.graphOn f = univ.graphOn fun a ↦ x.2 / f x.1 * f a := by simp [smul_graphOn]
Action on Graph of Function over Universal Set: $x \cdot \text{graph}(f|_{\text{univ}}) = \text{graph}\left(a \mapsto \frac{x_2}{f(x_1)} \cdot f(a)\right)|_{\text{univ}}$
Informal description
For any pair $x = (x_1, x_2) \in \alpha \times \beta$ and any function $f \colon \alpha \to \beta$, the action of $x$ on the graph of $f$ over the universal set $\text{univ} \subseteq \alpha$ is equal to the graph of the function $a \mapsto \frac{x_2}{f(x_1)} \cdot f(a)$ over $\text{univ}$. In other words: \[ x \cdot \text{graph}(f|_{\text{univ}}) = \text{graph}\left(a \mapsto \frac{x_2}{f(x_1)} \cdot f(a)\right)|_{\text{univ}}. \]
Set.smul_div_smul_comm theorem
(a : α) (s : Set α) (b : α) (t : Set α) : a • s / b • t = (a / b) • (s / t)
Full source 
@[to_additive] lemma smul_div_smul_comm (a : α) (s : Set α) (b : α) (t : Set α) :
    a • s / b • t = (a / b) • (s / t) := by
  simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]
Commutative Property of Pointwise Scaling and Division of Sets: $a \cdot s / b \cdot t = (a / b) \cdot (s / t)$
Informal description
For any elements $a, b$ in a group $\alpha$ and subsets $s, t$ of $\alpha$, the following equality holds: \[ a \cdot s / b \cdot t = (a / b) \cdot (s / t), \] where $a \cdot s$ denotes the pointwise multiplication of $a$ with each element of $s$, and $s / t$ denotes the pointwise division of elements in $s$ by elements in $t$.