LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Set.Pointwise.Basic

`Set.mul_subset_mul_left` theorem Set.mul_subset_mul_left : ∀ {α : Type u_2} [inst : Mul α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂ := by sorry The theorem `Set.mul_subset_mul_left` states that for any type `α` that has a multiplication operation (`Mul α`), and any given sets `s`, `t₁`, and `t₂` of this type, if `t₁` is a subset of `t₂`, then the set of all products of elements in `s` with elements in `t₁` is also a subset of the set of all products of elements in `s` with elements in `t₂`. In other words, if we multiply the elements of a smaller set `t₁` by a set `s`, the resulting set will be contained within the set resulting from multiplying the larger set `t₂` by the same set `s`. More concisely: For any type `α` with multiplication and sets `s` and `t₁` being subsets of `t₂` in `α`, the set {x₁ * y₁ \| x₁ ∈ s, y₁ ∈ t₁} is contained in the set {x₂ * y₂ \| x₂ ∈ s, y₂ ∈ t₂}.
`Set.add_singleton` theorem Set.add_singleton : ∀ {α : Type u_2} [inst : Add α] {s : Set α} {b : α}, s + {b} = (fun x => x + b) '' s := by sorry The theorem `Set.add_singleton` states that for any type `α` equipped with an addition operation, any set `s` of elements of type `α`, and any element `b` of type `α`, the addition of the set `s` with the singleton set containing `b` is equal to the image of the set `s` under the function `fun x => x + b`. That is, each element of the set `s` is mapped to an element that is obtained by adding `b` to it. Here the `''` symbol represents the image of a set under a function. More concisely: For any type `α` with addition, set `s ⊆ α`, and element `b ∈ α`, the set `s ∪ {b} = {x \| ∃ y ∈ s, x = y + b}`.
`Set.neg_preimage` theorem Set.neg_preimage : ∀ {α : Type u_2} [inst : Neg α] {s : Set α}, Neg.neg ⁻¹' s = -s The theorem `Set.neg_preimage` states that for any type `α` which has a negation operation defined, and any set `s` of elements of type `α`, the preimage of the set `s` under the negation operation is equal to the negative of the set `s`. In simpler terms, for any element of the type `α`, the negation of that element belongs to the set `s` if and only if the original element belongs to the negative of the set `s`. This theorem bridges the world of set operations and negation operations in the type `α`. More concisely: For any set `s` of type `α` with negation operation defined, `Set.neg (s.image neg) = s.complement`.
`Set.image_inv` theorem Set.image_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, Inv.inv '' s = s⁻¹ This theorem, named `Set.image_inv`, states that for any type `α` equipped with an involutive inverse operation, and for any set `s` of elements of type `α`, the image of `s` under the inverse operation (`Inv.inv '' s`) is equal to the inverse of `s` (`s⁻¹`). Here, an "involutive" operation is one where applying the operation twice returns the original value (i.e., for all `x` in `α`, `inv(inv(x)) = x`). The symbol `''` in `Inv.inv '' s` denotes the image of a set under a function. So `Inv.inv '' s` represents the set of all elements obtained by applying the inverse operation to each element of `s`. And `s⁻¹` represents the inverse of the set `s`. More concisely: For any set `s` of elements in a type `α` equipped with an involutive inverse operation, `Inv.image s (inv : α → α) = s⁻¹`.
`Set.neg_singleton` theorem Set.neg_singleton : ∀ {α : Type u_2} [inst : InvolutiveNeg α] (a : α), -{a} = {-a} The theorem `Set.neg_singleton` asserts that for all types `α` and for all elements `a` of type `α`, where `α` has an involutive negation operation (i.e., applying the negation operation twice yields the original element), the negation of the singleton set containing `a` is the singleton set containing the negation of `a`. In simpler terms, it states that negating the set containing only `a` is equivalent to creating a set that contains only the negation of `a`. More concisely: For any type `α` with an involutive negation operation, the negation of a singleton set `{a : α}` is the singleton set `{−a : α}`.
`Set.mul_subset_mul_right` theorem Set.mul_subset_mul_right : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t := by sorry This theorem states that for any type `α` that supports multiplication, and for any three sets `s₁`, `s₂` and `t` of elements of type `α`, if set `s₁` is a subset of set `s₂`, then the multiplication of set `s₁` and set `t` is a subset of the multiplication of set `s₂` and set `t`. In other words, multiplying by a set on the right preserves the subset relationship. More concisely: For any types `α` supporting multiplication and sets `s₁`, `s₂`, and `t` of elements from `α`, if `s₁ ⊆ s₂`, then `s₁ t ⊆ s₂ * t`.*
`Set.zero_nonempty` theorem Set.zero_nonempty : ∀ {α : Type u_2} [inst : Zero α], Set.Nonempty 0 The theorem `Set.zero_nonempty` states that for every type `α` that has an instance of the `Zero` typeclass, the set containing the zero element is nonempty. In other words, no matter what type `α` we are working with, if it has a zero element then the singleton set containing just this zero element is not empty. This is expressed in Lean 4 by saying that `Set.Nonempty 0` holds for these types `α`. More concisely: For every type `α` with a zero element, the singleton set `{0 : α}` is nonempty.
`Set.image_mul_right` theorem Set.image_mul_right : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t This theorem states that for any type `α` that has a group structure, any subset `t` of `α`, and any element `b` of `α`, the image of `t` under the function that multiplies by `b` is the same as the preimage of `t` under the function that multiplies by the inverse of `b`. In other words, if you multiply every element of a set by some fixed group element, you get the same result as if you took all the elements that, when multiplied by the inverse of that group element, are in the original set. More concisely: For any group `α` and subset `t` of `α`, and for all `b` in `α`, the sets `{x : α \| b x ∈ t}` and `{x : α \| x ∈ t ∧ x * b^(-1) ∈ α}` are equal.*
`Set.add_mem_add` theorem Set.add_mem_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a + b ∈ s + t := by sorry The theorem `Set.add_mem_add` states that for any type `α` that has an addition operation, given two sets `s` and `t` of elements of type `α`, and any two elements `a` and `b` such that `a` is in `s` and `b` is in `t`, then the sum `a + b` is in the sum set `s + t`. This essentially formalizes the intuitive idea that the sum of two elements, one from each of two sets, is in the set of all sums of elements from the two sets. More concisely: For any type `α` with addition and sets `s` and `t` of its elements, if `a` is in `s` and `b` is in `t`, then `a + b` is in `s + t`.
`Set.zero_mem_zero` theorem Set.zero_mem_zero : ∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0 This theorem states that, for any type 'α' which has a zero element, this zero element is a member of the singleton set that contains only zero. In mathematical terms, it says that for all 'α', if 'α' has a zero, then 0 is an element of the set {0}. This is a special case of the general rule that every element is a member of the singleton set which contains only that element. More concisely: For any type 'α' with a zero element, the zero element is an element of the singleton set {0}.
`Set.singleton_one` theorem Set.singleton_one : ∀ {α : Type u_2} [inst : One α], {1} = 1 This theorem states that for any type `α` that has an instance of the `One` typeclass (meaning it has a well-defined "one" or multiplicative identity), the set that contains only the element "one" (`{1}`) is equivalent to the "one" element itself (`1`). In mathematical terms, for any type with a multiplicative identity, the singleton set containing only the identity is equivalent to the identity. More concisely: For any type `α` with a multiplicative identity, the singleton set `{1 : α}` is equal to the identity `1 : α`.
`Set.mem_add` theorem Set.mem_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a : α}, a ∈ s + t ↔ ∃ x ∈ s, ∃ y ∈ t, x + y = a This theorem states that for any type `α` that has an addition operation, given two sets `s` and `t` of type `α` and an element `a` of type `α`, `a` belongs to the set resulting from the addition of `s` and `t` if and only if there exists an element `x` in `s` and an element `y` in `t` such that `x + y = a`. In other words, an element is in the sum of two sets if it can be written as the sum of an element from each set. More concisely: For any type `α` with addition and sets `s` and `t` of type `α`, an element `a` belongs to the sum `s ++ t` if and only if there exist `x ∈ s` and `y ∈ t` such that `x + y = a`.
`Set.one_mem_div_iff` theorem Set.one_mem_div_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, 1 ∈ s / t ↔ ¬Disjoint s t This theorem states that for any type `α` that forms a group, and any two sets `s` and `t` of elements from this group, the multiplicative identity `1` is an element of the quotient set `s / t` if and only if the sets `s` and `t` are not disjoint. Here, the quotient set `s / t` is defined as the set of all elements `x` such that there exists an element in `s` and an element in `t` whose product equals `x`. The sets `s` and `t` are said to be disjoint if their infimum (greatest lower bound) is the bottom element of their lattice structure. More concisely: For any group `α`, the multiplicative identity `1` belongs to the quotient set `s / t` of `α` if and only if sets `s` and `t` are not disjoint.
`Disjoint.one_not_mem_div_set` theorem Disjoint.one_not_mem_div_set : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, Disjoint s t → 1 ∉ s / t := by sorry This theorem, `Disjoint.one_not_mem_div_set`, states that for any type `α` that forms a group, given two sets `s` and `t` of elements of type `α`, if `s` and `t` are disjoint (in the sense that any element that is less than or equal to both `s` and `t` is necessarily less than or equal to the bottom element of the lattice), then the element `1` is not an element of the set derived from dividing every element of `s` by every element of `t`. In the context of groups, this division operation is more formally known as the quotient of `s` by `t`. More concisely: For any group `α`, if sets `s` and `t` are disjoint, then `1` is not an element of the set of quotients of `s` by `t`.
`Set.singleton_mul_singleton` theorem Set.singleton_mul_singleton : ∀ {α : Type u_2} [inst : Mul α] {a b : α}, {a} * {b} = {a * b} This theorem states that for any two elements `a` and `b` from a multiplication-equipped type `α`, the result of the set multiplication operation on the singleton sets `{a}` and `{b}` is equal to the singleton set `{a * b}`. In other words, it says that the singleton set of the product of `a` and `b` is the same as the product of the singleton sets of `a` and `b`. More concisely: For any multiplication-equipped type `α` and elements `a, b` from `α`, the singleton sets `{a}` and `{b}` have product equal to the singleton set of their product, i.e., {a} {b} = {a * b}.*
`Set.inv_singleton` theorem Set.inv_singleton : ∀ {α : Type u_2} [inst : InvolutiveInv α] (a : α), {a}⁻¹ = {a⁻¹} This theorem states that for any type `α` with an involutive inverse operation (a function which is its own inverse), the inverse of a singleton set containing an element `a` of type `α` is equal to the singleton set containing the inverse of `a`. In mathematical terms, this can be written as `({a}^-1 = {a^-1})` for all `a` in `α`, where `α` is equipped with an involutive inverse operation. More concisely: For any type `α` with an involutive inverse operation, the singleton set with inverse element equals the singleton set with the original element: {a^-1} = {x \| x = a^-1}.
`Set.neg_subset_neg` theorem Set.neg_subset_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ -t ↔ s ⊆ t This theorem, `Set.neg_subset_neg`, states that for any type `α` that has an `InvolutiveNeg` (i.e., a negation operation that is its own inverse), and for any two sets `s` and `t` of this type, the set of negations of elements in `s` is a subset of the set of negations of elements in `t` if and only if `s` is a subset of `t`. This essentially means that the subset relation is preserved under the operation of taking negations of elements in these sets. More concisely: For sets `s` and `t` of a type `α` with an `InvolutiveNeg`, `neg s ⊆ neg t` if and only if `s ⊆ t`.
`Set.mul_mem_mul` theorem Set.mul_mem_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a * b ∈ s * t := by sorry The theorem `Set.mul_mem_mul` states that for any type `α` that has a multiplication operation, given two sets `s` and `t` of type `α`, and two elements `a` and `b` from `α`, if `a` is an element of set `s` and `b` is an element of set `t`, then the product `a * b` is an element of the set formed by the multiplication of sets `s` and `t`. More concisely: For any types `α` with multiplication and sets `s` and `t` of `α`, if `a ∈ s` and `b ∈ t`, then `a b ∈ s × t`. (Assuming `×` denotes the set product.)*
`Set.image_add_right'` theorem Set.image_add_right' : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {b : α}, (fun x => x + -b) '' t = (fun x => x + b) ⁻¹' t := by sorry This theorem, `Set.image_add_right'`, states that for any type `α` with an `AddGroup` structure, for any set `t` of type `α`, and any element `b` of type `α`, the image of the set `t` under the function `x ↦ x + (-b)` is equal to the preimage of the set `t` under the function `x ↦ x + b`. In other words, adding `-b` to each element in a set gives the same result as the set of elements that would result in an element of the original set when `b` is added to them. More concisely: For any set `t` of an additive group `α`, and any element `b` in `α`, the sets `{x : α \| x + (-b) ∈ t}` and `{x : α \| x + b ∈ t}` are equal.
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.13` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.13 : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, (-s ⊆ -t) = (s ⊆ t) This theorem states that for every type `α` that has an operation of involution through negation, given any two sets `s` and `t` of type `α`, the statement that the negated set `-s` is a subset of the negated set `-t` is equivalent to the statement that the original set `s` is a subset of the original set `t`. This holds true regardless of the specific elements within the sets `s` and `t`. More concisely: For any type `α` with negation involution, sets `s` and `t` of type `α`, the sets `-s` and `-t` are equal if and only if `s` is a subset of `t`.
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.28` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.28 : ∀ {α : Type u_2} [inst : Div α] {s t : Set α} {a : α}, (a ∈ s / t) = ∃ x ∈ s, ∃ y ∈ t, x / y = a This theorem is stating that for any type `α` that has a division operation, given two sets `s` and `t` of type `α`, and an element `a` of type `α`, the element `a` is in the quotient set `s / t` if and only if there exist elements `x` in `s` and `y` in `t` such that `x / y` equals `a`. In mathematical terms, for any element `a`, `a` is in the set `s / t` if and only if there exist elements `x` in `s` and `y` in `t` such that `x / y = a`. More concisely: For any type `α` with division, and sets `s` and `t` of `α`, an element `a` is in the quotient `s / t` if and only if there exist `x ∈ s` and `y ∈ t` such that `x / y = a`.
`Set.image_neg` theorem Set.image_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, Neg.neg '' s = -s This theorem, `Set.image_neg`, states that for any set `s` of elements of some type `α`, which has an associated operation `Neg.neg` that computes the negative or opposite of its members (i.e., `α` has an involutive negation operation), the image of `s` under this negation operation (`Neg.neg '' s`) is equal to the negative of set `s` (`-s`). The meaning of "negative of a set" is defined in the context of the theorem. Essentially, this theorem establishes a relationship between operations applied to individual elements of a set and operations applied to the set as a whole. More concisely: For any set `s` of elements in a type `α` with an involutive negation operation, `Neg.neg s` equals the negative of `s`, denoted `-s`.
`Set.Nonempty.neg` theorem Set.Nonempty.neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, s.Nonempty → (-s).Nonempty The theorem `Set.Nonempty.neg` states that for any type `α` with an `InvolutiveNeg` instance (meaning that it's a type with a negation operation such that negating twice gives the original element), if a set `s` of this type is nonempty (i.e., `Set.Nonempty s`), then the set obtained by applying the negation operation to each element of `s` (denoted by `-s`) is also nonempty. In other words, if we have at least one element in a set, the set of their negations will also have at least one element. More concisely: If `α` is a type with an `InvolutiveNeg` instance and `s : Set α` is nonempty, then `-s` is also nonempty.
`Set.add_subset_add` theorem Set.add_subset_add : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂ The theorem `Set.add_subset_add` states that for any type `α` that has an addition operation, given two sets `s₁` and `s₂` of type `α`, and two other sets `t₁` and `t₂` of the same type, if `s₁` is a subset of `t₁` and `s₂` is a subset of `t₂`, then the set of all elements obtained by adding an element of `s₁` to an element of `s₂` is a subset of the set of all elements obtained by adding an element of `t₁` to an element of `t₂`. In mathematical terms, if $s₁ ⊆ t₁$ and $s₂ ⊆ t₂$, then $s₁ + s₂ ⊆ t₁ + t₂$. More concisely: If sets $s\_1$ and $s\_2$ are subsets of $t\_1$ and $t\_2$, respectively, then $s\_1 + s\_2 \subseteq t\_1 + t\_2$, where $+$ denotes addition of elements of a type with defined addition operation.
`Set.singleton_mul` theorem Set.singleton_mul : ∀ {α : Type u_2} [inst : Mul α] {t : Set α} {a : α}, {a} * t = (fun x => a * x) '' t := by sorry The theorem `Set.singleton_mul` states that for any type `α` that has a multiplication operation (`Mul α`), and for any set `t` of this type, and any element `a` of this type, the result of multiplying the singleton set containing `a` and the set `t` is equivalent to the image of the set `t` under the function that multiplies each element by `a`. In mathematical terms, this is saying that `{a} * t = {a * x \| x ∈ t}`. More concisely: The theorem asserts that for any type `α` with multiplication and for any set `t` of `α`, the singleton set `{a}` multiplied by `t` equals the image of `t` under the function `x => a x`.*
`Set.image_one` theorem Set.image_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {f : α → β}, f '' 1 = {f 1} This theorem states that for any types `α` and `β`, given a one instance for `α` and a function `f` from `α` to `β`, the image of `1` under `f` is equal to the set containing `f(1)`. In other words, if you apply the function `f` to the element `1` in type `α`, the result will be a set that contains just the image of `1` under `f`. More concisely: For any types `α` and `β` and function `f` from `α` to `β`, `image_singleton 1 f = {f 1}`.
`Set.Nonempty.add` theorem Set.Nonempty.add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, s.Nonempty → t.Nonempty → (s + t).Nonempty This theorem states that for any type `α` that has an addition operation, given two sets `s` and `t` of that type, if both `s` and `t` are nonempty (i.e., each set contains at least one element), then their sum set `s + t` is also nonempty. The sum set `s + t` is defined as the set of all elements that can be obtained by adding an element of `s` to an element of `t`. More concisely: If `α` is a type with an addition operation and `s` and `t` are nonempty sets of `α`, then `s + t` is a nonempty set.
`Set.image_mul_right'` theorem Set.image_mul_right' : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t The theorem `Set.image_mul_right'` states that, for all types `α` that form a group, for any set `t` of `α` and any element `b` of `α`, the set obtained by taking every element `x` in `t` and multiplying it by the inverse of `b` is the same as the preimage of `t` under the function that multiplies each element by `b`. In other words, multiplying each element of a set by the inverse of a chosen element results in the same set as taking those elements that would land in the original set when multiplied by the chosen element. More concisely: For any group type `α`, set `t` of `α`, and element `b` of `α`, the sets {x : α \| ∃ (x' : α), x = x' b^(-1) ∧ x' ∈ t} and {x : α \| x ∈ t ∧ x * b ∈ α} are equal.*
`Set.zero_mem_sub_iff` theorem Set.zero_mem_sub_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, 0 ∈ s - t ↔ ¬Disjoint s t This theorem states that for any type `α` that forms an additive group, given any two sets `s` and `t` of elements of this type, the additive identity `0` is an element of the difference set `s - t` if and only if the sets `s` and `t` are not disjoint. Here, a difference set `s - t` refers to the set of all elements `x` such that `x` is in `s` and `x` is not in `t`. Two sets are disjoint if every element `x` that is less than or equal to both `s` and `t` is also less than or equal to the bottom element `⊥`. More concisely: For any additive group `α`, the additive identity `0` is an element of the difference `s - t` of sets `s` and `t` if and only if `s` and `t` have non-empty intersection.
`Set.Nonempty.mul` theorem Set.Nonempty.mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, s.Nonempty → t.Nonempty → (s * t).Nonempty The theorem `Set.Nonempty.mul` states that for any two sets `s` and `t` of elements from a type `α` that supports multiplication, if both `s` and `t` are nonempty (i.e., each contains at least one element), then the set `s * t` is also nonempty. Here, `s * t` represents the set obtained by multiplying all possible pairs of elements where the first element is from `s` and the second element is from `t`. More concisely: If sets `s` and `t` over type `α` are nonempty, then their Cartesian product `s × t` is nonempty.
`Set.singleton_add` theorem Set.singleton_add : ∀ {α : Type u_2} [inst : Add α] {t : Set α} {a : α}, {a} + t = (fun x => a + x) '' t := by sorry This theorem states that for any type `α` which has an addition operation, given a set `t` of elements of type `α` and an element `a` of type `α`, the sum of the singleton set containing `a` and the set `t` is equal to the image of the set `t` under the function that adds `a` to each element. In other words, every element in the resultant set is formed by adding `a` to some element in set `t`. More concisely: For any set `t` of elements from a type `α` with addition, the set `t ∪ {a}` is equal to the image of `t` under the function `x => x + a`.
`Set.zero_subset` theorem Set.zero_subset : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, 0 ⊆ s ↔ 0 ∈ s This theorem states that for any type `α` that has a zero element (denoted as `0`), and for any set `s` of elements of type `α`, the set containing only the zero element is a subset of `s` if and only if the zero element is an element of `s`. In other words, it states a condition under which a set containing only the zero element is considered a subset of another set in terms of membership of the zero element in the other set. This theorem essentially connects the notion of subset with the notion of element membership for the specific case of the zero element. More concisely: For any type `α` with a zero element `0`, the set `{0}` is a subset of `s` if and only if `0` is an element of `s`.
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.5` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.5 : ∀ {α : Type u_2} [inst : Inv α] {s : Set α} {a : α}, (a ∈ s⁻¹) = (a⁻¹ ∈ s) This theorem, named `Mathlib.Data.Set.Pointwise.Basic._auxLemma.5`, states that for any type `α` that has an operation `Inv` (which signifies that elements of `α` can be inverted) and any set `s` of type `α`, and any element `a` of type `α`, the element `a` is in the inverse of the set `s` if and only if the inverse of `a` is in the set `s`. In other words, it deals with the membership of an element and its inverse in a set and its inverse. More concisely: For any type `α` with an operation `Inv` and any set `s` of type `α`, an element `a` is in the inverse of `s` if and only if the inverse of `a` is in `s`.
`Set.neg_mem_neg` theorem Set.neg_mem_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α} {a : α}, -a ∈ -s ↔ a ∈ s The theorem `Set.neg_mem_neg` states that for any type `α` equipped with an involutive negation operation (i.e., a negation operation that when applied twice gives the original element back) and any set `s` of elements of type `α`, the negation of an element `a` of type `α` is in the negation of the set `s` if and only if `a` is in `s`. This theorem essentially tells us that the negation operation on elements is compatible with the negation operation on sets in this given context. More concisely: For any type `α` with an involutive negation operation and any set `s` of `α`, an element `a` is in the negation of `s` if and only if the negation of `a` is in `s`.
`Set.image_mul_left` theorem Set.image_mul_left : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {a : α}, (fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t This theorem states that for any type `α` that forms a group, a given set `t` of elements of type `α`, and a specific element `a` of type `α`, the image of the set `t` under the left-multiplication function by `a` (`a * x` for each `x` in `t`) is equal to the preimage of the set `t` under the function of left-multiplication by the inverse of `a` (`a⁻¹ * x`). In other words, multiplying each element of a set by a group element and taking the preimage of a set by multiplying each element by the inverse of the same group element gives the same result. More concisely: For any group `α` and its element `a`, the sets `{a x \| x ∈ t}` and `{x \| x ∈ t ∧ a⁻¹ * x = x}` are equal.*
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.26` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.26 : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a : α}, (a ∈ s * t) = ∃ x ∈ s, ∃ y ∈ t, x * y = a The theorem `Mathlib.Data.Set.Pointwise.Basic._auxLemma.26` states that for any type `α` that has a multiplication operation, and any sets `s` and `t` of this type, and any element `a` of the same type, `a` is in the set-theoretic product of `s` and `t` if and only if there exists an element `x` in `s` and an element `y` in `t` such that the multiplication of `x` and `y` equals `a`. This set-theoretic product operation is analogous to the Cartesian product of two sets, but with the pairing operation replaced by multiplication. More concisely: For any type `α` with multiplication, and sets `s` and `t` of `α`, an element `a` is in the product `s ∘ t` if and only if there exist `x ∈ s` and `y ∈ t` such that `x y = a`.*
`Set.neg_subset` theorem Set.neg_subset : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ t ↔ s ⊆ -t This theorem, `Set.neg_subset`, states that for any type `α` equipped with an `InvolutiveNeg` operation (that is, a negation operation which satisfies `neg (neg x) = x`), and for any two sets `s` and `t` of type `α`, the negation of set `s` is a subset of set `t` if and only if set `s` is a subset of the negation of set `t`. Here, the negation of a set `s` is defined as the set of all negated elements of `s`, and the subset relation `⊆` is defined in its usual sense: a set `s` is a subset of a set `t` if every element of `s` is also an element of `t`. More concisely: For sets `s` and `t` of an type `α` equipped with an `InvolutiveNeg` operation, `s ⊆ t` if and only if `neg t ⊆ neg s`.
`Set.add_image_prod` theorem Set.add_image_prod : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, (fun x => x.1 + x.2) '' s ×ˢ t = s + t := by sorry This theorem, `Set.add_image_prod`, states that for any type `α` equipped with an addition operation, and any sets `s` and `t` of this type, the image of the Cartesian product `s ×ˢ t` under the function `(x.1 + x.2)` is equal to the sum of the sets `s` and `t`. In other words, if you take every pair of elements from `s` and `t`, add them together, and collect all the results into a set, you end up with the same set as if you just added `s` and `t` together directly. More concisely: For any set `α` equipped with an addition operation, the image of the Cartesian product `s × t` under the function `λ (x, y) => x + y` is equal to the set `s ∪ t`.
`Set.mul_singleton` theorem Set.mul_singleton : ∀ {α : Type u_2} [inst : Mul α] {s : Set α} {b : α}, s * {b} = (fun x => x * b) '' s := by sorry The theorem `Set.mul_singleton` states that for any type `α` equipped with a multiplication operation, and for any set `s` of elements of type `α` and an element `b` of type `α`, the multiplication of the set `s` and the singleton set `{b}` results in a set that contains the product of each element of `s` with `b`. Here `s * {b}` denotes the set that contains the product of each element of `s` with `b`, and `(fun x => x * b) '' s` is the image of the set `s` under the function that multiplies each element by `b`. More concisely: For any type `α` with multiplication and any set `s �ябряα` and element `b ∈ α`, `s {b} = {x * b \| x ∈ s}`.*
`Set.mem_mul` theorem Set.mem_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a : α}, a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a This theorem, named `Set.mem_mul`, is a statement about sets and multiplication in some type `α` which is equipped with a multiplication operation. It states that for any fixed type `α` that has multiplication, and any two sets `s` and `t` of elements of this type, alongside any element `a` from `α`, `a` is an element of the product of `s` and `t` if and only if there exist elements `x` in `s` and `y` in `t` such that the product of `x` and `y` equals `a`. In other words, this theorem defines the notion of membership in the product of two sets in the context of a type with multiplication. More concisely: For any sets $S, T$ of elements from a type $\alpha$ with multiplication, and any $a \in \alpha$, $a \in S \times T$ if and only if there exist $x \in S$ and $y \in T$ such that $x \cdot y = a$.
`Set.singleton_zero` theorem Set.singleton_zero : ∀ {α : Type u_2} [inst : Zero α], {0} = 0 This theorem, `Set.singleton_zero`, states that for any type `α` that has a `Zero` instance, the singleton set containing just the `0` element (denoted as `{0}`) is equal to `0`. In other words, it expresses the equivalence between the singleton set of the zero element and the zero element itself in the context of any type that has a zero instance. More concisely: For any type `α` with a `Zero` instance, the singleton set `{0}` is equal to the zero element `0`.
`Set.mem_neg` theorem Set.mem_neg : ∀ {α : Type u_2} [inst : Neg α] {s : Set α} {a : α}, a ∈ -s ↔ -a ∈ s This theorem, named as `Set.mem_neg`, states that for any type `α` that has a negation operation, and for any set `s` of elements of type `α`, and for any element `a` of type `α`, the element `a` belongs to the negation of set `s` if and only if the negation of `a` belongs to set `s`. This theorem essentially establishes a relationship between an element and its negation in relation to their membership in a set and its negation. More concisely: For any set `s` of type `α` and any element `a` of type `α` in a type with negation, `a` is in the negation of `s` if and only if the negation of `a` is in `s`.
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.6` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.6 : ∀ {α : Type u_2} [inst : Neg α] {s : Set α} {a : α}, (a ∈ -s) = (-a ∈ s) This theorem, `Mathlib.Data.Set.Pointwise.Basic._auxLemma.6`, states that for any type `α` which has a negation operation, any set `s` of type `α`, and any element `a` of type `α`, the element `a` is in the negation of the set `s` if and only if the negation of `a` is in the set `s`. In other words, an element is in the negation of a set if and only if its negation is in the original set. More concisely: For any type `α` with negation and set `s` of type `α`, element `a` is in the complement of `s` if and only if the negation of `a` is in `s`.
`Set.image_add_right` theorem Set.image_add_right : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {b : α}, (fun x => x + b) '' t = (fun x => x + -b) ⁻¹' t := by sorry The `Set.image_add_right` theorem states the following: for any type `α` that forms an additive group, any set `t` of `α`, and any element `b` of `α`, the image of set `t` under the function that adds `b` to each element of `t` (`(fun x => x + b) '' t`) is equal to the preimage of set `t` under the function that subtracts `b` from each element (`(fun x => x + -b) ⁻¹' t`). Essentially, it illustrates the relationship between set transformation by addition and its corresponding transformation by subtraction in the context of an additive group. More concisely: For any additive group `α`, set `t` of `α`, and element `b` of `α`, the set `(fun x => x + b) '' t` equals the set `(fun x => x + -b) ⁻¹' t`.
`Set.add_subset_add_left` theorem Set.add_subset_add_left : ∀ {α : Type u_2} [inst : Add α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂ := by sorry This theorem states that for any type `α` that supports addition, and any sets `s`, `t₁`, and `t₂` of elements of type `α`, if `t₁` is a subset of `t₂`, then the set of elements obtained by adding each element of `s` to each element of `t₁` is a subset of the set obtained by adding each element of `s` to each element of `t₂`. In other words, for all `α` in `Type u_2` with an addition operation and for all sets `s`, `t₁`, `t₂` of `α`, set addition preserves subset relationships. More concisely: For any type `α` with an addition operation and for all sets `s` and `t₁` subset `t₂` of `α`, the set `{a + b \| a ∈ s, b ∈ t₁}` is a subset of `{a + b \| a ∈ s, b ∈ t₂}`.
`Set.mul_subset_mul` theorem Set.mul_subset_mul : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂ This theorem, named `Set.mul_subset_mul`, states that for any type `α` that has a multiplication operation (`Mul α`), if we have four sets of elements of type `α` (denoted by `s₁`, `s₂`, `t₁`, and `t₂`), and if `s₁` is a subset of `t₁` and `s₂` is a subset of `t₂`, then the set formed by multiplying elements from `s₁` and `s₂` is a subset of the set formed by multiplying elements from `t₁` and `t₂`. This is expressed in the language of set theory using the subset symbol `⊆` and the multiplication operation on sets ``. More concisely: If `s₁ ⊆ t₁` and `s₂ ⊆ t₂`, then `s₁ * s₂ ⊆ t₁ * t₂`, where `` denotes set multiplication over types with a defined multiplication operation.
`Set.image_add_left` theorem Set.image_add_left : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {a : α}, (fun x => a + x) '' t = (fun x => -a + x) ⁻¹' t := by sorry This theorem, `Set.image_add_left`, states that for any type `α` that forms an additive group, for any set `t` of elements of type `α`, and for any element `a` from `α`, the image of `t` under the function that adds `a` to each element is the same as the preimage of `t` under the function that subtracts `a` from each element. In other words, if you take a set, add `a` to each element, you obtain the same set as if you took the original set and found the set of all elements that would give you an element in the original set if `a` were subtracted from them. More concisely: For any additive group `α`, the image of a set `t` under the successor function `x => x + a` is equal to the preimage of `t` under the subtraction function `x => x - a`.
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.2` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.2 : ∀ {α : Type u_2} [inst : Zero α] {a : α}, (a ∈ 0) = (a = 0) := by sorry This theorem, `Mathlib.Data.Set.Pointwise.Basic._auxLemma.2`, states that for any type `α` that has a zero element (denoted by `0`), for any element `a` of type `α`, the assertion that `a` is in `0` is equivalent to the assertion that `a` equals `0`. This is typically applied in the context of algebraic structures like rings and fields where `0` represents the additive identity. More concisely: For any type `α` with a zero element `0`, the equality `a = 0` is equivalent to `a ∈ 0` for any `a` in `α`.
`Set.mem_inv` theorem Set.mem_inv : ∀ {α : Type u_2} [inst : Inv α] {s : Set α} {a : α}, a ∈ s⁻¹ ↔ a⁻¹ ∈ s This theorem states that for any type `α` that has an inverse operation, a set `s` of elements of type `α`, and an element `a` of type `α`, `a` is in the inverse of the set `s` if and only if the inverse of `a` is in the set `s`. Here, the inverse of a set is defined as the set of inverses of all elements in the original set. More concisely: For any type `α` with an inverse operation, a set `s ⊆ α`, and an element `a ∈ α`, `a ∈ s^∘` if and only if `a^⁻¹ ∈ s`, where `s^∘` denotes the set of inverses of `s`.
`Set.image_mul` theorem Set.image_mul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β] [inst_3 : MulHomClass F α β] (m : F) {s t : Set α}, ⇑m '' (s * t) = ⇑m '' s * ⇑m '' t This theorem, `Set.image_mul`, states that for any types `F`, `α`, and `β` where `α` and `β` have multiplication defined on them (`Mul α` and `Mul β`), and `F` is a function-like structure from `α` to `β` (`FunLike F α β`), and moreover `F` respects the multiplication (`MulHomClass F α β`), then the image via `m` (a term of type `F`) of the product of two sets `s` and `t` of type `α` (`s * t`) is equal to the product of the images of `s` and `t` via `m` (`m '' s * m '' t`). In mathematical terms, this theorem establishes that a function (or more generally, a term of type `F`) that preserves multiplication also preserves the multiplication operation when applied to sets of elements, i.e., for all sets `s` and `t`, `m(st) = m(s) m(t)`. More concisely: Given functions `F` from type `α` to type `β` that preserve multiplication, the image of the product of two sets under `F` is equal to the product of the images of the sets. In other words, `m(s * t) = m(s) * m(t)` for sets `s` and `t` of type `α` and function `m` of type `F`.
`Set.singleton_add_singleton` theorem Set.singleton_add_singleton : ∀ {α : Type u_2} [inst : Add α] {a b : α}, {a} + {b} = {a + b} This theorem states that for any two elements `a` and `b` of a type `α` that is equipped with an addition operation, the sum of the sets containing `a` and `b` individually equals the set containing the sum of `a` and `b`. Symbolically, this is expressed as `{a} + {b} = {a + b}`. This theorem is valid for any type that supports addition, not just the usual numbers. More concisely: For any type `α` with an addition operation, the set of an element `a` is equal to the set containing the sum of `a` and another element `b`, i.e., {a} = {a + b}.
`Mathlib.Data.Set.Pointwise.Basic._auxLemma.4` theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.4 : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, (0 ⊆ s) = (0 ∈ s) This theorem states that for any type `α` that has a zero element (as indicated by the `inst : Zero α`), and for any set `s` of elements of type `α` (`s : Set α`), the statement "zero is a subset of `s`" (denoted `0 ⊆ s`) is equivalent to the statement "zero is an element of `s`" (denoted `0 ∈ s`). Thus, in this specific context, being a subset and being an element are equivalent concepts for zero. More concisely: For any type `α` with a zero element `0`, the subset inclusion `0 ⊆ s` and element membership `0 ∈ s` are equivalent for any set `s` of elements of type `α`.
`Set.image_mul_prod` theorem Set.image_mul_prod : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, (fun x => x.1 * x.2) '' s ×ˢ t = s * t := by sorry The theorem `Set.image_mul_prod` states that for any type `α` that has a multiplication operation, and any two sets `s` and `t` of this type, the set of all products of pairs of elements, where the first element is from `s` and the second is from `t`, is equal to the set obtained by multiplying `s` and `t` (where multiplication of sets is defined elementwise). In other words, forming the Cartesian product of `s` and `t`, then mapping each pair `(x, y)` to `x * y`, gives the same set as directly multiplying the sets `s` and `t`. More concisely: For any type `α` with multiplication and sets `s` and `t` of this type, the sets `s × t` and `{x y \| x ∈ s, y ∈ t}` are equal.*

LeanAide GPT-4 documentation

Module: Mathlib.Data.Set.Pointwise.Basic

Set.mul_subset_mul_left

theorem Set.mul_subset_mul_left : ∀ {α : Type u_2} [inst : Mul α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂ := by sorry

Set.add_singleton

theorem Set.add_singleton : ∀ {α : Type u_2} [inst : Add α] {s : Set α} {b : α}, s + {b} = (fun x => x + b) '' s := by sorry

Set.neg_preimage

theorem Set.neg_preimage : ∀ {α : Type u_2} [inst : Neg α] {s : Set α}, Neg.neg ⁻¹' s = -s

Set.image_inv

theorem Set.image_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, Inv.inv '' s = s⁻¹

Set.neg_singleton

theorem Set.neg_singleton : ∀ {α : Type u_2} [inst : InvolutiveNeg α] (a : α), -{a} = {-a}

Set.mul_subset_mul_right

theorem Set.mul_subset_mul_right : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t := by sorry

Set.zero_nonempty

theorem Set.zero_nonempty : ∀ {α : Type u_2} [inst : Zero α], Set.Nonempty 0

Set.image_mul_right

theorem Set.image_mul_right : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t

Set.add_mem_add

theorem Set.add_mem_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a + b ∈ s + t := by sorry

Set.zero_mem_zero

theorem Set.zero_mem_zero : ∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0

Set.singleton_one

theorem Set.singleton_one : ∀ {α : Type u_2} [inst : One α], {1} = 1

Set.mem_add

theorem Set.mem_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a : α}, a ∈ s + t ↔ ∃ x ∈ s, ∃ y ∈ t, x + y = a

Set.one_mem_div_iff

theorem Set.one_mem_div_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, 1 ∈ s / t ↔ ¬Disjoint s t

Disjoint.one_not_mem_div_set

theorem Disjoint.one_not_mem_div_set : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, Disjoint s t → 1 ∉ s / t := by sorry

Set.singleton_mul_singleton

theorem Set.singleton_mul_singleton : ∀ {α : Type u_2} [inst : Mul α] {a b : α}, {a} * {b} = {a * b}

Set.inv_singleton

theorem Set.inv_singleton : ∀ {α : Type u_2} [inst : InvolutiveInv α] (a : α), {a}⁻¹ = {a⁻¹}

Set.neg_subset_neg

theorem Set.neg_subset_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ -t ↔ s ⊆ t

Set.mul_mem_mul

theorem Set.mul_mem_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a * b ∈ s * t := by sorry

Set.image_add_right'

theorem Set.image_add_right' : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {b : α}, (fun x => x + -b) '' t = (fun x => x + b) ⁻¹' t := by sorry

Mathlib.Data.Set.Pointwise.Basic._auxLemma.13

theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.13 : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, (-s ⊆ -t) = (s ⊆ t)

Mathlib.Data.Set.Pointwise.Basic._auxLemma.28

theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.28 : ∀ {α : Type u_2} [inst : Div α] {s t : Set α} {a : α}, (a ∈ s / t) = ∃ x ∈ s, ∃ y ∈ t, x / y = a

Set.image_neg

theorem Set.image_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, Neg.neg '' s = -s

Set.Nonempty.neg

theorem Set.Nonempty.neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, s.Nonempty → (-s).Nonempty

Set.add_subset_add

theorem Set.add_subset_add : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂

Set.singleton_mul

theorem Set.singleton_mul : ∀ {α : Type u_2} [inst : Mul α] {t : Set α} {a : α}, {a} * t = (fun x => a * x) '' t := by sorry

Set.image_one

theorem Set.image_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {f : α → β}, f '' 1 = {f 1}

Set.Nonempty.add

theorem Set.Nonempty.add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, s.Nonempty → t.Nonempty → (s + t).Nonempty

Set.image_mul_right'

theorem Set.image_mul_right' : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t

Set.zero_mem_sub_iff

theorem Set.zero_mem_sub_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, 0 ∈ s - t ↔ ¬Disjoint s t

Set.Nonempty.mul

theorem Set.Nonempty.mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, s.Nonempty → t.Nonempty → (s * t).Nonempty

Set.singleton_add

theorem Set.singleton_add : ∀ {α : Type u_2} [inst : Add α] {t : Set α} {a : α}, {a} + t = (fun x => a + x) '' t := by sorry

Set.zero_subset

theorem Set.zero_subset : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, 0 ⊆ s ↔ 0 ∈ s

Mathlib.Data.Set.Pointwise.Basic._auxLemma.5

theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.5 : ∀ {α : Type u_2} [inst : Inv α] {s : Set α} {a : α}, (a ∈ s⁻¹) = (a⁻¹ ∈ s)

Set.neg_mem_neg

theorem Set.neg_mem_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α} {a : α}, -a ∈ -s ↔ a ∈ s

Set.image_mul_left

theorem Set.image_mul_left : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {a : α}, (fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t

Mathlib.Data.Set.Pointwise.Basic._auxLemma.26

theorem Mathlib.Data.Set.Pointwise.Basic._auxLemma.26 : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a : α}, (a ∈ s * t) = ∃ x ∈ s, ∃ y ∈ t, x * y = a

Set.neg_subset

theorem Set.neg_subset : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ t ↔ s ⊆ -t

Set.add_image_prod

theorem Set.add_image_prod : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, (fun x => x.1 + x.2) '' s ×ˢ t = s + t := by sorry

Set.mul_singleton

theorem Set.mul_singleton : ∀ {α : Type u_2} [inst : Mul α] {s : Set α} {b : α}, s * {b} = (fun x => x * b) '' s := by sorry

`Set.mul_subset_mul_left`

`Set.add_singleton`

`Set.neg_preimage`

`Set.image_inv`

`Set.neg_singleton`

`Set.mul_subset_mul_right`

`Set.zero_nonempty`

`Set.image_mul_right`

`Set.add_mem_add`

`Set.zero_mem_zero`

`Set.singleton_one`

`Set.mem_add`

`Set.one_mem_div_iff`

`Disjoint.one_not_mem_div_set`

`Set.singleton_mul_singleton`

`Set.inv_singleton`

`Set.neg_subset_neg`

`Set.mul_mem_mul`

`Set.image_add_right'`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.13`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.28`

`Set.image_neg`

`Set.Nonempty.neg`

`Set.add_subset_add`

`Set.singleton_mul`

`Set.image_one`

`Set.Nonempty.add`

`Set.image_mul_right'`

`Set.zero_mem_sub_iff`

`Set.Nonempty.mul`

`Set.singleton_add`

`Set.zero_subset`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.5`

`Set.neg_mem_neg`

`Set.image_mul_left`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.26`

`Set.neg_subset`

`Set.add_image_prod`

`Set.mul_singleton`

`Set.mem_mul`

`Set.singleton_zero`

`Set.mem_neg`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.6`

`Set.image_add_right`

`Set.add_subset_add_left`

`Set.mul_subset_mul`

`Set.image_add_left`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.2`

`Set.mem_inv`

`Set.image_mul`

`Set.singleton_add_singleton`

`Mathlib.Data.Set.Pointwise.Basic._auxLemma.4`

`Set.image_mul_prod`