Pointwise.lean

/-
Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhouhang Zhou, Yaël Dillies
-/
import Mathlib.Data.Set.Pointwise.SMul
import Mathlib.Order.Filter.NAry
import Mathlib.Order.Filter.Ultrafilter

#align_import order.filter.pointwise from "leanprover-community/mathlib"@"e3d9ab8faa9dea8f78155c6c27d62a621f4c152d"

/-!
# Pointwise operations on filters

This file defines pointwise operations on filters. This is useful because usual algebraic operations
distribute over pointwise operations. For example,
* `(f₁ * f₂).map m = f₁.map m * f₂.map m`
* `𝓝 (x * y) = 𝓝 x * 𝓝 y`

## Main declarations

* `0` (`Filter.instZero`): Pure filter at `0 : α`, or alternatively principal filter at `0 : Set α`.
* `1` (`Filter.instOne`): Pure filter at `1 : α`, or alternatively principal filter at `1 : Set α`.
* `f + g` (`Filter.instAdd`): Addition, filter generated by all `s + t` where `s ∈ f` and `t ∈ g`.
* `f * g` (`Filter.instMul`): Multiplication, filter generated by all `s * t` where `s ∈ f` and
  `t ∈ g`.
* `-f` (`Filter.instNeg`): Negation, filter of all `-s` where `s ∈ f`.
* `f⁻¹` (`Filter.instInv`): Inversion, filter of all `s⁻¹` where `s ∈ f`.
* `f - g` (`Filter.instSub`): Subtraction, filter generated by all `s - t` where `s ∈ f` and
  `t ∈ g`.
* `f / g` (`Filter.instDiv`): Division, filter generated by all `s / t` where `s ∈ f` and `t ∈ g`.
* `f +ᵥ g` (`Filter.instVAdd`): Scalar addition, filter generated by all `s +ᵥ t` where `s ∈ f` and
  `t ∈ g`.
* `f -ᵥ g` (`Filter.instVSub`): Scalar subtraction, filter generated by all `s -ᵥ t` where `s ∈ f`
  and `t ∈ g`.
* `f • g` (`Filter.instSMul`): Scalar multiplication, filter generated by all `s • t` where
  `s ∈ f` and `t ∈ g`.
* `a +ᵥ f` (`Filter.instVAddFilter`): Translation, filter of all `a +ᵥ s` where `s ∈ f`.
* `a • f` (`Filter.instSMulFilter`): Scaling, filter of all `a • s` where `s ∈ f`.

For `α` a semigroup/monoid, `Filter α` is a semigroup/monoid.
As an unfortunate side effect, this means that `n • f`, where `n : ℕ`, is ambiguous between
pointwise scaling and repeated pointwise addition. See note [pointwise nat action].

## 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`).

## Tags

filter multiplication, filter addition, pointwise addition, pointwise multiplication,
-/


open Function Set Filter Pointwise

variable {F α β γ δ ε : Type*}

namespace Filter

/-! ### `0`/`1` as filters -/


section One

variable [One α] {f : Filter α} {s : Set α}

/-- `1 : Filter α` is defined as the filter of sets containing `1 : α` in locale `Pointwise`. -/
@[to_additive
      "`0 : Filter α` is defined as the filter of sets containing `0 : α` in locale `Pointwise`."]
protected def instOne : One (Filter α) :=
  ⟨pure 1⟩
#align filter.has_one Filter.instOne
#align filter.has_zero Filter.instZero

scoped[Pointwise] attribute [instance] Filter.instOne Filter.instZero

@[to_additive (attr := simp)]
theorem mem_one : s ∈ (1 : Filter α) ↔ (1 : α) ∈ s :=
  mem_pure
#align filter.mem_one Filter.mem_one
#align filter.mem_zero Filter.mem_zero

@[to_additive]
theorem one_mem_one : (1 : Set α) ∈ (1 : Filter α) :=
  mem_pure.2 Set.one_mem_one
#align filter.one_mem_one Filter.one_mem_one
#align filter.zero_mem_zero Filter.zero_mem_zero

@[to_additive (attr := simp)]
theorem pure_one : pure 1 = (1 : Filter α) :=
  rfl
#align filter.pure_one Filter.pure_one
#align filter.pure_zero Filter.pure_zero

@[to_additive (attr := simp)]
theorem principal_one : 𝓟 1 = (1 : Filter α) :=
  principal_singleton _
#align filter.principal_one Filter.principal_one
#align filter.principal_zero Filter.principal_zero

@[to_additive]
theorem one_neBot : (1 : Filter α).NeBot :=
  Filter.pure_neBot
#align filter.one_ne_bot Filter.one_neBot
#align filter.zero_ne_bot Filter.zero_neBot

scoped[Pointwise] attribute [instance] one_neBot zero_neBot

@[to_additive (attr := simp)]
protected theorem map_one' (f : α → β) : (1 : Filter α).map f = pure (f 1) :=
  rfl
#align filter.map_one' Filter.map_one'
#align filter.map_zero' Filter.map_zero'

@[to_additive (attr := simp)]
theorem le_one_iff : f ≤ 1 ↔ (1 : Set α) ∈ f :=
  le_pure_iff
#align filter.le_one_iff Filter.le_one_iff
#align filter.nonpos_iff Filter.nonpos_iff

@[to_additive]
protected theorem NeBot.le_one_iff (h : f.NeBot) : f ≤ 1 ↔ f = 1 :=
  h.le_pure_iff
#align filter.ne_bot.le_one_iff Filter.NeBot.le_one_iff
#align filter.ne_bot.nonpos_iff Filter.NeBot.nonpos_iff

@[to_additive (attr := simp)]
theorem eventually_one {p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1 :=
  eventually_pure
#align filter.eventually_one Filter.eventually_one
#align filter.eventually_zero Filter.eventually_zero

@[to_additive (attr := simp)]
theorem tendsto_one {a : Filter β} {f : β → α} : Tendsto f a 1 ↔ ∀ᶠ x in a, f x = 1 :=
  tendsto_pure
#align filter.tendsto_one Filter.tendsto_one
#align filter.tendsto_zero Filter.tendsto_zero

@[to_additive (attr := simp)]
theorem one_prod_one [One β] : (1 : Filter α) ×ˢ (1 : Filter β) = 1 :=
  prod_pure_pure
#align filter.one_prod_one Filter.one_prod_one
#align filter.zero_sum_zero Filter.zero_sum_zero

/-- `pure` as a `OneHom`. -/
@[to_additive "`pure` as a `ZeroHom`."]
def pureOneHom : OneHom α (Filter α) where
  toFun := pure; map_one' := pure_one
#align filter.pure_one_hom Filter.pureOneHom
#align filter.pure_zero_hom Filter.pureZeroHom

@[to_additive (attr := simp)]
theorem coe_pureOneHom : (pureOneHom : α → Filter α) = pure :=
  rfl
#align filter.coe_pure_one_hom Filter.coe_pureOneHom
#align filter.coe_pure_zero_hom Filter.coe_pureZeroHom

@[to_additive (attr := simp)]
theorem pureOneHom_apply (a : α) : pureOneHom a = pure a :=
  rfl
#align filter.pure_one_hom_apply Filter.pureOneHom_apply
#align filter.pure_zero_hom_apply Filter.pureZeroHom_apply

variable [One β]

@[to_additive]
-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it.
protected theorem map_one [FunLike F α β] [OneHomClass F α β] (φ : F) : map φ 1 = 1 := by
  rw [Filter.map_one', map_one, pure_one]
#align filter.map_one Filter.map_one
#align filter.map_zero Filter.map_zero

end One

/-! ### Filter negation/inversion -/


section Inv

variable [Inv α] {f g : Filter α} {s : Set α} {a : α}

/-- The inverse of a filter is the pointwise preimage under `⁻¹` of its sets. -/
@[to_additive "The negation of a filter is the pointwise preimage under `-` of its sets."]
instance instInv : Inv (Filter α) :=
  ⟨map Inv.inv⟩

@[to_additive (attr := simp)]
protected theorem map_inv : f.map Inv.inv = f⁻¹ :=
  rfl
#align filter.map_inv Filter.map_inv
#align filter.map_neg Filter.map_neg

@[to_additive]
theorem mem_inv : s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f :=
  Iff.rfl
#align filter.mem_inv Filter.mem_inv
#align filter.mem_neg Filter.mem_neg

@[to_additive]
protected theorem inv_le_inv (hf : f ≤ g) : f⁻¹ ≤ g⁻¹ :=
  map_mono hf
#align filter.inv_le_inv Filter.inv_le_inv
#align filter.neg_le_neg Filter.neg_le_neg

@[to_additive (attr := simp)]
theorem inv_pure : (pure a : Filter α)⁻¹ = pure a⁻¹ :=
  rfl
#align filter.inv_pure Filter.inv_pure
#align filter.neg_pure Filter.neg_pure

@[to_additive (attr := simp)]
theorem inv_eq_bot_iff : f⁻¹ = ⊥ ↔ f = ⊥ :=
  map_eq_bot_iff
#align filter.inv_eq_bot_iff Filter.inv_eq_bot_iff
#align filter.neg_eq_bot_iff Filter.neg_eq_bot_iff

@[to_additive (attr := simp)]
theorem neBot_inv_iff : f⁻¹.NeBot ↔ NeBot f :=
  map_neBot_iff _
#align filter.ne_bot_inv_iff Filter.neBot_inv_iff
#align filter.ne_bot_neg_iff Filter.neBot_neg_iff

@[to_additive]
protected theorem NeBot.inv : f.NeBot → f⁻¹.NeBot := fun h => h.map _
#align filter.ne_bot.inv Filter.NeBot.inv
#align filter.ne_bot.neg Filter.NeBot.neg

@[to_additive neg.instNeBot]
lemma inv.instNeBot [NeBot f] : NeBot f⁻¹ := .inv ‹_›

scoped[Pointwise] attribute [instance] inv.instNeBot neg.instNeBot

end Inv

section InvolutiveInv

variable [InvolutiveInv α] {f g : Filter α} {s : Set α}

@[to_additive (attr := simp)]
protected lemma comap_inv : comap Inv.inv f = f⁻¹ :=
  .symm <| map_eq_comap_of_inverse (inv_comp_inv _) (inv_comp_inv _)

@[to_additive]
theorem inv_mem_inv (hs : s ∈ f) : s⁻¹ ∈ f⁻¹ := by rwa [mem_inv, inv_preimage, inv_inv]
#align filter.inv_mem_inv Filter.inv_mem_inv
#align filter.neg_mem_neg Filter.neg_mem_neg

/-- Inversion is involutive on `Filter α` if it is on `α`. -/
@[to_additive "Negation is involutive on `Filter α` if it is on `α`."]
protected def instInvolutiveInv : InvolutiveInv (Filter α) :=
  { Filter.instInv with
    inv_inv := fun f => map_map.trans <| by rw [inv_involutive.comp_self, map_id] }
#align filter.has_involutive_inv Filter.instInvolutiveInv
#align filter.has_involutive_neg Filter.instInvolutiveNeg

scoped[Pointwise] attribute [instance] Filter.instInvolutiveInv Filter.instInvolutiveNeg

@[to_additive (attr := simp)]
protected theorem inv_le_inv_iff : f⁻¹ ≤ g⁻¹ ↔ f ≤ g :=
  ⟨fun h => inv_inv f ▸ inv_inv g ▸ Filter.inv_le_inv h, Filter.inv_le_inv⟩
#align filter.inv_le_inv_iff Filter.inv_le_inv_iff
#align filter.neg_le_neg_iff Filter.neg_le_neg_iff

@[to_additive]
theorem inv_le_iff_le_inv : f⁻¹ ≤ g ↔ f ≤ g⁻¹ := by rw [← Filter.inv_le_inv_iff, inv_inv]
#align filter.inv_le_iff_le_inv Filter.inv_le_iff_le_inv
#align filter.neg_le_iff_le_neg Filter.neg_le_iff_le_neg

@[to_additive (attr := simp)]
theorem inv_le_self : f⁻¹ ≤ f ↔ f⁻¹ = f :=
  ⟨fun h => h.antisymm <| inv_le_iff_le_inv.1 h, Eq.le⟩
#align filter.inv_le_self Filter.inv_le_self
#align filter.neg_le_self Filter.neg_le_self

end InvolutiveInv

@[to_additive (attr := simp)]
lemma inv_atTop {G : Type*} [OrderedCommGroup G] : (atTop : Filter G)⁻¹ = atBot :=
  (OrderIso.inv G).map_atTop

/-! ### Filter addition/multiplication -/

section Mul

variable [Mul α] [Mul β] {f f₁ f₂ g g₁ g₂ h : Filter α} {s t : Set α} {a b : α}

/-- The filter `f * g` is generated by `{s * t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
@[to_additive "The filter `f + g` is generated by `{s + t | s ∈ f, t ∈ g}` in locale `Pointwise`."]
protected def instMul : Mul (Filter α) :=
  ⟨/- This is defeq to `map₂ (· * ·) f g`, but the hypothesis unfolds to `t₁ * t₂ ⊆ s` rather
  than all the way to `Set.image2 (· * ·) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· * ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s } }⟩
#align filter.has_mul Filter.instMul
#align filter.has_add Filter.instAdd

scoped[Pointwise] attribute [instance] Filter.instMul Filter.instAdd

@[to_additive (attr := simp)]
theorem map₂_mul : map₂ (· * ·) f g = f * g :=
  rfl
#align filter.map₂_mul Filter.map₂_mul
#align filter.map₂_add Filter.map₂_add

@[to_additive]
theorem mem_mul : s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s :=
  Iff.rfl
#align filter.mem_mul Filter.mem_mul
#align filter.mem_add Filter.mem_add

@[to_additive]
theorem mul_mem_mul : s ∈ f → t ∈ g → s * t ∈ f * g :=
  image2_mem_map₂
#align filter.mul_mem_mul Filter.mul_mem_mul
#align filter.add_mem_add Filter.add_mem_add

@[to_additive (attr := simp)]
theorem bot_mul : ⊥ * g = ⊥ :=
  map₂_bot_left
#align filter.bot_mul Filter.bot_mul
#align filter.bot_add Filter.bot_add

@[to_additive (attr := simp)]
theorem mul_bot : f * ⊥ = ⊥ :=
  map₂_bot_right
#align filter.mul_bot Filter.mul_bot
#align filter.add_bot Filter.add_bot

@[to_additive (attr := simp)]
theorem mul_eq_bot_iff : f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff
#align filter.mul_eq_bot_iff Filter.mul_eq_bot_iff
#align filter.add_eq_bot_iff Filter.add_eq_bot_iff

@[to_additive (attr := simp)] -- TODO: make this a scoped instance in the `Pointwise` namespace
lemma mul_neBot_iff : (f * g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff
#align filter.mul_ne_bot_iff Filter.mul_neBot_iff
#align filter.add_ne_bot_iff Filter.add_neBot_iff

@[to_additive]
protected theorem NeBot.mul : NeBot f → NeBot g → NeBot (f * g) :=
  NeBot.map₂
#align filter.ne_bot.mul Filter.NeBot.mul
#align filter.ne_bot.add Filter.NeBot.add

@[to_additive]
theorem NeBot.of_mul_left : (f * g).NeBot → f.NeBot :=
  NeBot.of_map₂_left
#align filter.ne_bot.of_mul_left Filter.NeBot.of_mul_left
#align filter.ne_bot.of_add_left Filter.NeBot.of_add_left

@[to_additive]
theorem NeBot.of_mul_right : (f * g).NeBot → g.NeBot :=
  NeBot.of_map₂_right
#align filter.ne_bot.of_mul_right Filter.NeBot.of_mul_right
#align filter.ne_bot.of_add_right Filter.NeBot.of_add_right

@[to_additive add.instNeBot]
protected lemma mul.instNeBot [NeBot f] [NeBot g] : NeBot (f * g) := .mul ‹_› ‹_›

scoped[Pointwise] attribute [instance] mul.instNeBot add.instNeBot

@[to_additive (attr := simp)]
theorem pure_mul : pure a * g = g.map (a * ·) :=
  map₂_pure_left
#align filter.pure_mul Filter.pure_mul
#align filter.pure_add Filter.pure_add

@[to_additive (attr := simp)]
theorem mul_pure : f * pure b = f.map (· * b) :=
  map₂_pure_right
#align filter.mul_pure Filter.mul_pure
#align filter.add_pure Filter.add_pure

@[to_additive]
-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it.
theorem pure_mul_pure : (pure a : Filter α) * pure b = pure (a * b) :=
  map₂_pure
#align filter.pure_mul_pure Filter.pure_mul_pure
#align filter.pure_add_pure Filter.pure_add_pure

@[to_additive (attr := simp)]
theorem le_mul_iff : h ≤ f * g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s * t ∈ h :=
  le_map₂_iff
#align filter.le_mul_iff Filter.le_mul_iff
#align filter.le_add_iff Filter.le_add_iff

@[to_additive]
instance covariant_mul : CovariantClass (Filter α) (Filter α) (· * ·) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_left⟩
#align filter.covariant_mul Filter.covariant_mul
#align filter.covariant_add Filter.covariant_add

@[to_additive]
instance covariant_swap_mul : CovariantClass (Filter α) (Filter α) (swap (· * ·)) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_right⟩
#align filter.covariant_swap_mul Filter.covariant_swap_mul
#align filter.covariant_swap_add Filter.covariant_swap_add

@[to_additive]
protected theorem map_mul [FunLike F α β] [MulHomClass F α β] (m : F) :
    (f₁ * f₂).map m = f₁.map m * f₂.map m :=
  map_map₂_distrib <| map_mul m
#align filter.map_mul Filter.map_mul
#align filter.map_add Filter.map_add

/-- `pure` operation as a `MulHom`. -/
@[to_additive "The singleton operation as an `AddHom`."]
def pureMulHom : α →ₙ* Filter α where
  toFun := pure; map_mul' _ _ := pure_mul_pure.symm
#align filter.pure_mul_hom Filter.pureMulHom
#align filter.pure_add_hom Filter.pureAddHom

@[to_additive (attr := simp)]
theorem coe_pureMulHom : (pureMulHom : α → Filter α) = pure :=
  rfl
#align filter.coe_pure_mul_hom Filter.coe_pureMulHom
#align filter.coe_pure_add_hom Filter.coe_pureMulHom

@[to_additive (attr := simp)]
theorem pureMulHom_apply (a : α) : pureMulHom a = pure a :=
  rfl
#align filter.pure_mul_hom_apply Filter.pureMulHom_apply
#align filter.pure_add_hom_apply Filter.pureMulHom_apply

end Mul

/-! ### Filter subtraction/division -/

section Div

variable [Div α] {f f₁ f₂ g g₁ g₂ h : Filter α} {s t : Set α} {a b : α}

/-- The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
@[to_additive "The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in locale `Pointwise`."]
protected def instDiv : Div (Filter α) :=
  ⟨/- This is defeq to `map₂ (· / ·) f g`, but the hypothesis unfolds to `t₁ / t₂ ⊆ s`
  rather than all the way to `Set.image2 (· / ·) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· / ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s } }⟩
#align filter.has_div Filter.instDiv
#align filter.has_sub Filter.instSub

scoped[Pointwise] attribute [instance] Filter.instDiv Filter.instSub

@[to_additive (attr := simp)]
theorem map₂_div : map₂ (· / ·) f g = f / g :=
  rfl
#align filter.map₂_div Filter.map₂_div
#align filter.map₂_sub Filter.map₂_sub

@[to_additive]
theorem mem_div : s ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s :=
  Iff.rfl
#align filter.mem_div Filter.mem_div
#align filter.mem_sub Filter.mem_sub

@[to_additive]
theorem div_mem_div : s ∈ f → t ∈ g → s / t ∈ f / g :=
  image2_mem_map₂
#align filter.div_mem_div Filter.div_mem_div
#align filter.sub_mem_sub Filter.sub_mem_sub

@[to_additive (attr := simp)]
theorem bot_div : ⊥ / g = ⊥ :=
  map₂_bot_left
#align filter.bot_div Filter.bot_div
#align filter.bot_sub Filter.bot_sub

@[to_additive (attr := simp)]
theorem div_bot : f / ⊥ = ⊥ :=
  map₂_bot_right
#align filter.div_bot Filter.div_bot
#align filter.sub_bot Filter.sub_bot

@[to_additive (attr := simp)]
theorem div_eq_bot_iff : f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff
#align filter.div_eq_bot_iff Filter.div_eq_bot_iff
#align filter.sub_eq_bot_iff Filter.sub_eq_bot_iff

@[to_additive (attr := simp)]
theorem div_neBot_iff : (f / g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff
#align filter.div_ne_bot_iff Filter.div_neBot_iff
#align filter.sub_ne_bot_iff Filter.sub_neBot_iff

@[to_additive]
protected theorem NeBot.div : NeBot f → NeBot g → NeBot (f / g) :=
  NeBot.map₂
#align filter.ne_bot.div Filter.NeBot.div
#align filter.ne_bot.sub Filter.NeBot.sub

@[to_additive]
theorem NeBot.of_div_left : (f / g).NeBot → f.NeBot :=
  NeBot.of_map₂_left
#align filter.ne_bot.of_div_left Filter.NeBot.of_div_left
#align filter.ne_bot.of_sub_left Filter.NeBot.of_sub_left

@[to_additive]
theorem NeBot.of_div_right : (f / g).NeBot → g.NeBot :=
  NeBot.of_map₂_right
#align filter.ne_bot.of_div_right Filter.NeBot.of_div_right
#align filter.ne_bot.of_sub_right Filter.NeBot.of_sub_right

@[to_additive sub.instNeBot]
lemma div.instNeBot [NeBot f] [NeBot g] : NeBot (f / g) := .div ‹_› ‹_›

scoped[Pointwise] attribute [instance] div.instNeBot sub.instNeBot

@[to_additive (attr := simp)]
theorem pure_div : pure a / g = g.map (a / ·) :=
  map₂_pure_left
#align filter.pure_div Filter.pure_div
#align filter.pure_sub Filter.pure_sub

@[to_additive (attr := simp)]
theorem div_pure : f / pure b = f.map (· / b) :=
  map₂_pure_right
#align filter.div_pure Filter.div_pure
#align filter.sub_pure Filter.sub_pure

@[to_additive]
-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it.
theorem pure_div_pure : (pure a : Filter α) / pure b = pure (a / b) :=
  map₂_pure
#align filter.pure_div_pure Filter.pure_div_pure
#align filter.pure_sub_pure Filter.pure_sub_pure

@[to_additive]
protected theorem div_le_div : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂ :=
  map₂_mono
#align filter.div_le_div Filter.div_le_div
#align filter.sub_le_sub Filter.sub_le_sub

@[to_additive]
protected theorem div_le_div_left : g₁ ≤ g₂ → f / g₁ ≤ f / g₂ :=
  map₂_mono_left
#align filter.div_le_div_left Filter.div_le_div_left
#align filter.sub_le_sub_left Filter.sub_le_sub_left

@[to_additive]
protected theorem div_le_div_right : f₁ ≤ f₂ → f₁ / g ≤ f₂ / g :=
  map₂_mono_right
#align filter.div_le_div_right Filter.div_le_div_right
#align filter.sub_le_sub_right Filter.sub_le_sub_right

@[to_additive (attr := simp)]
protected theorem le_div_iff : h ≤ f / g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s / t ∈ h :=
  le_map₂_iff
#align filter.le_div_iff Filter.le_div_iff
#align filter.le_sub_iff Filter.le_sub_iff

@[to_additive]
instance covariant_div : CovariantClass (Filter α) (Filter α) (· / ·) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_left⟩
#align filter.covariant_div Filter.covariant_div
#align filter.covariant_sub Filter.covariant_sub

@[to_additive]
instance covariant_swap_div : CovariantClass (Filter α) (Filter α) (swap (· / ·)) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_right⟩
#align filter.covariant_swap_div Filter.covariant_swap_div
#align filter.covariant_swap_sub Filter.covariant_swap_sub

end Div

open Pointwise

/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Filter`. See
Note [pointwise nat action]. -/
protected def instNSMul [Zero α] [Add α] : SMul ℕ (Filter α) :=
  ⟨nsmulRec⟩
#align filter.has_nsmul Filter.instNSMul

/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Filter`. See Note [pointwise nat action]. -/
@[to_additive existing]
protected def instNPow [One α] [Mul α] : Pow (Filter α) ℕ :=
  ⟨fun s n => npowRec n s⟩
#align filter.has_npow Filter.instNPow

/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Filter`. See Note [pointwise nat action]. -/
protected def instZSMul [Zero α] [Add α] [Neg α] : SMul ℤ (Filter α) :=
  ⟨zsmulRec⟩
#align filter.has_zsmul Filter.instZSMul

/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Filter`. See Note [pointwise nat action]. -/
@[to_additive existing]
protected def instZPow [One α] [Mul α] [Inv α] : Pow (Filter α) ℤ :=
  ⟨fun s n => zpowRec npowRec n s⟩
#align filter.has_zpow Filter.instZPow

scoped[Pointwise] attribute [instance] Filter.instNSMul Filter.instNPow
  Filter.instZSMul Filter.instZPow

/-- `Filter α` is a `Semigroup` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddSemigroup` under pointwise operations if `α` is."]
protected def semigroup [Semigroup α] : Semigroup (Filter α) where
  mul := (· * ·)
  mul_assoc _ _ _ := map₂_assoc mul_assoc
#align filter.semigroup Filter.semigroup
#align filter.add_semigroup Filter.addSemigroup

/-- `Filter α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddCommSemigroup` under pointwise operations if `α` is."]
protected def commSemigroup [CommSemigroup α] : CommSemigroup (Filter α) :=
  { Filter.semigroup with mul_comm := fun _ _ => map₂_comm mul_comm }
#align filter.comm_semigroup Filter.commSemigroup
#align filter.add_comm_semigroup Filter.addCommSemigroup

section MulOneClass

variable [MulOneClass α] [MulOneClass β]

/-- `Filter α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddZeroClass` under pointwise operations if `α` is."]
protected def mulOneClass : MulOneClass (Filter α) where
  one := 1
  mul := (· * ·)
  one_mul := map₂_left_identity one_mul
  mul_one := map₂_right_identity mul_one
#align filter.mul_one_class Filter.mulOneClass
#align filter.add_zero_class Filter.addZeroClass

scoped[Pointwise] attribute [instance] Filter.semigroup Filter.addSemigroup
  Filter.commSemigroup Filter.addCommSemigroup Filter.mulOneClass Filter.addZeroClass

variable [FunLike F α β]

/-- If `φ : α →* β` then `mapMonoidHom φ` is the monoid homomorphism
`Filter α →* Filter β` induced by `map φ`. -/
@[to_additive "If `φ : α →+ β` then `mapAddMonoidHom φ` is the monoid homomorphism
 `Filter α →+ Filter β` induced by `map φ`."]
def mapMonoidHom [MonoidHomClass F α β] (φ : F) : Filter α →* Filter β where
  toFun := map φ
  map_one' := Filter.map_one φ
  map_mul' _ _ := Filter.map_mul φ
#align filter.map_monoid_hom Filter.mapMonoidHom
#align filter.map_add_monoid_hom Filter.mapAddMonoidHom

-- The other direction does not hold in general
@[to_additive]
theorem comap_mul_comap_le [MulHomClass F α β] (m : F) {f g : Filter β} :
    f.comap m * g.comap m ≤ (f * g).comap m := fun _ ⟨_, ⟨t₁, ht₁, t₂, ht₂, t₁t₂⟩, mt⟩ =>
  ⟨m ⁻¹' t₁, ⟨t₁, ht₁, Subset.rfl⟩, m ⁻¹' t₂, ⟨t₂, ht₂, Subset.rfl⟩,
    (preimage_mul_preimage_subset _).trans <| (preimage_mono t₁t₂).trans mt⟩
#align filter.comap_mul_comap_le Filter.comap_mul_comap_le
#align filter.comap_add_comap_le Filter.comap_add_comap_le

@[to_additive]
theorem Tendsto.mul_mul [MulHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β} :
    Tendsto m f₁ f₂ → Tendsto m g₁ g₂ → Tendsto m (f₁ * g₁) (f₂ * g₂) := fun hf hg =>
  (Filter.map_mul m).trans_le <| mul_le_mul' hf hg
#align filter.tendsto.mul_mul Filter.Tendsto.mul_mul
#align filter.tendsto.add_add Filter.Tendsto.add_add

/-- `pure` as a `MonoidHom`. -/
@[to_additive "`pure` as an `AddMonoidHom`."]
def pureMonoidHom : α →* Filter α :=
  { pureMulHom, pureOneHom with }
#align filter.pure_monoid_hom Filter.pureMonoidHom
#align filter.pure_add_monoid_hom Filter.pureAddMonoidHom

@[to_additive (attr := simp)]
theorem coe_pureMonoidHom : (pureMonoidHom : α → Filter α) = pure :=
  rfl
#align filter.coe_pure_monoid_hom Filter.coe_pureMonoidHom
#align filter.coe_pure_add_monoid_hom Filter.coe_pureAddMonoidHom

@[to_additive (attr := simp)]
theorem pureMonoidHom_apply (a : α) : pureMonoidHom a = pure a :=
  rfl
#align filter.pure_monoid_hom_apply Filter.pureMonoidHom_apply
#align filter.pure_add_monoid_hom_apply Filter.pureAddMonoidHom_apply

end MulOneClass

section Monoid

variable [Monoid α] {f g : Filter α} {s : Set α} {a : α} {m n : ℕ}

/-- `Filter α` is a `Monoid` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddMonoid` under pointwise operations if `α` is."]
protected def monoid : Monoid (Filter α) :=
  { Filter.mulOneClass, Filter.semigroup, @Filter.instNPow α _ _ with }
#align filter.monoid Filter.monoid
#align filter.add_monoid Filter.addMonoid

scoped[Pointwise] attribute [instance] Filter.monoid Filter.addMonoid

@[to_additive]
theorem pow_mem_pow (hs : s ∈ f) : ∀ n : ℕ, s ^ n ∈ f ^ n
  | 0 => by
    rw [pow_zero]
    exact one_mem_one
  | n + 1 => by
    rw [pow_succ]
    exact mul_mem_mul (pow_mem_pow hs n) hs
#align filter.pow_mem_pow Filter.pow_mem_pow
#align filter.nsmul_mem_nsmul Filter.nsmul_mem_nsmul

@[to_additive (attr := simp) nsmul_bot]
theorem bot_pow {n : ℕ} (hn : n ≠ 0) : (⊥ : Filter α) ^ n = ⊥ := by
  rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn), pow_succ', bot_mul]
#align filter.bot_pow Filter.bot_pow
#align filter.nsmul_bot Filter.nsmul_bot

@[to_additive]
theorem mul_top_of_one_le (hf : 1 ≤ f) : f * ⊤ = ⊤ := by
  refine' top_le_iff.1 fun s => _
  simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
#align filter.mul_top_of_one_le Filter.mul_top_of_one_le
#align filter.add_top_of_nonneg Filter.add_top_of_nonneg

@[to_additive]
theorem top_mul_of_one_le (hf : 1 ≤ f) : ⊤ * f = ⊤ := by
  refine' top_le_iff.1 fun s => _
  simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
#align filter.top_mul_of_one_le Filter.top_mul_of_one_le
#align filter.top_add_of_nonneg Filter.top_add_of_nonneg

@[to_additive (attr := simp)]
theorem top_mul_top : (⊤ : Filter α) * ⊤ = ⊤ :=
  mul_top_of_one_le le_top
#align filter.top_mul_top Filter.top_mul_top
#align filter.top_add_top Filter.top_add_top

@[to_additive nsmul_top]
theorem top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : Filter α) ^ n = ⊤
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
#align filter.top_pow Filter.top_pow
#align filter.nsmul_top Filter.nsmul_top

@[to_additive]
protected theorem _root_.IsUnit.filter : IsUnit a → IsUnit (pure a : Filter α) :=
  IsUnit.map (pureMonoidHom : α →* Filter α)
#align is_unit.filter IsUnit.filter
#align is_add_unit.filter IsAddUnit.filter

end Monoid

/-- `Filter α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive "`Filter α` is an `AddCommMonoid` under pointwise operations if `α` is."]
protected def commMonoid [CommMonoid α] : CommMonoid (Filter α) :=
  { Filter.mulOneClass, Filter.commSemigroup with }
#align filter.comm_monoid Filter.commMonoid
#align filter.add_comm_monoid Filter.addCommMonoid

open Pointwise

section DivisionMonoid

variable [DivisionMonoid α] {f g : Filter α}

@[to_additive]
protected theorem mul_eq_one_iff : f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1 := by
  refine' ⟨fun hfg => _, _⟩
  · obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm.subst one_mem_one
    have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
    rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
    obtain ⟨a, b, rfl, rfl, h⟩ := h
    refine' ⟨a, b, _, _, h⟩
    · rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
    · rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
  · rintro ⟨a, b, rfl, rfl, h⟩
    rw [pure_mul_pure, h, pure_one]
#align filter.mul_eq_one_iff Filter.mul_eq_one_iff
#align filter.add_eq_zero_iff Filter.add_eq_zero_iff

/-- `Filter α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionMonoid "`Filter α` is a subtraction monoid under pointwise operations if
 `α` is."]
-- Porting note: `to_additive` guessed `divisionAddMonoid`
protected def divisionMonoid : DivisionMonoid (Filter α) :=
  { Filter.monoid, Filter.instInvolutiveInv, Filter.instDiv, Filter.instZPow (α := α) with
    mul_inv_rev := fun s t => map_map₂_antidistrib mul_inv_rev
    inv_eq_of_mul := fun s t h => by
      obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
      rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
    div_eq_mul_inv := fun f g => map_map₂_distrib_right div_eq_mul_inv }
#align filter.division_monoid Filter.divisionMonoid
#align filter.subtraction_monoid Filter.subtractionMonoid

@[to_additive]
theorem isUnit_iff : IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a := by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
    refine' ⟨a, ha, ⟨a, b, h, pure_injective _⟩, rfl⟩
    rw [← pure_mul_pure, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.filter
#align filter.is_unit_iff Filter.isUnit_iff
#align filter.is_add_unit_iff Filter.isAddUnit_iff

end DivisionMonoid

/-- `Filter α` is a commutative division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionCommMonoid
      "`Filter α` is a commutative subtraction monoid under pointwise operations if `α` is."]
protected def divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (Filter α) :=
  { Filter.divisionMonoid, Filter.commSemigroup with }
#align filter.division_comm_monoid Filter.divisionCommMonoid
#align filter.subtraction_comm_monoid Filter.subtractionCommMonoid

/-- `Filter α` has distributive negation if `α` has. -/
protected def instDistribNeg [Mul α] [HasDistribNeg α] : HasDistribNeg (Filter α) :=
  { Filter.instInvolutiveNeg with
    neg_mul := fun _ _ => map₂_map_left_comm neg_mul
    mul_neg := fun _ _ => map_map₂_right_comm mul_neg }
#align filter.has_distrib_neg Filter.instDistribNeg

scoped[Pointwise] attribute [instance] Filter.commMonoid Filter.addCommMonoid Filter.divisionMonoid
  Filter.subtractionMonoid Filter.divisionCommMonoid Filter.subtractionCommMonoid
  Filter.instDistribNeg

section Distrib

variable [Distrib α] {f g h : Filter α}

/-!
Note that `Filter α` is not a `Distrib` because `f * g + f * h` has cross terms that `f * (g + h)`
lacks.
-/

theorem mul_add_subset : f * (g + h) ≤ f * g + f * h :=
  map₂_distrib_le_left mul_add
#align filter.mul_add_subset Filter.mul_add_subset

theorem add_mul_subset : (f + g) * h ≤ f * h + g * h :=
  map₂_distrib_le_right add_mul
#align filter.add_mul_subset Filter.add_mul_subset

end Distrib

section MulZeroClass

variable [MulZeroClass α] {f g : Filter α}

/-! Note that `Filter` is not a `MulZeroClass` because `0 * ⊥ ≠ 0`. -/

theorem NeBot.mul_zero_nonneg (hf : f.NeBot) : 0 ≤ f * 0 :=
  le_mul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, mul_zero _⟩
#align filter.ne_bot.mul_zero_nonneg Filter.NeBot.mul_zero_nonneg

theorem NeBot.zero_mul_nonneg (hg : g.NeBot) : 0 ≤ 0 * g :=
  le_mul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_mul _⟩
#align filter.ne_bot.zero_mul_nonneg Filter.NeBot.zero_mul_nonneg

end MulZeroClass

section Group

variable [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β]
  (m : F) {f g f₁ g₁ : Filter α} {f₂ g₂ : Filter β}

/-! Note that `Filter α` is not a group because `f / f ≠ 1` in general -/

-- Porting note: increase priority to appease `simpNF` so left-hand side doesn't simplify
@[to_additive (attr := simp 1100)]
protected theorem one_le_div_iff : 1 ≤ f / g ↔ ¬Disjoint f g := by
  refine' ⟨fun h hfg => _, _⟩
  · obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
    exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)
  · rintro h s ⟨t₁, h₁, t₂, h₂, hs⟩
    exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)
#align filter.one_le_div_iff Filter.one_le_div_iff
#align filter.nonneg_sub_iff Filter.nonneg_sub_iff

@[to_additive]
theorem not_one_le_div_iff : ¬1 ≤ f / g ↔ Disjoint f g :=
  Filter.one_le_div_iff.not_left
#align filter.not_one_le_div_iff Filter.not_one_le_div_iff
#align filter.not_nonneg_sub_iff Filter.not_nonneg_sub_iff

@[to_additive]
theorem NeBot.one_le_div (h : f.NeBot) : 1 ≤ f / f := by
  rintro s ⟨t₁, h₁, t₂, h₂, hs⟩
  obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)
  rw [mem_one, ← div_self' a]
  exact hs (Set.div_mem_div ha₁ ha₂)
#align filter.ne_bot.one_le_div Filter.NeBot.one_le_div
#align filter.ne_bot.nonneg_sub Filter.NeBot.nonneg_sub

@[to_additive]
theorem isUnit_pure (a : α) : IsUnit (pure a : Filter α) :=
  (Group.isUnit a).filter
#align filter.is_unit_pure Filter.isUnit_pure
#align filter.is_add_unit_pure Filter.isAddUnit_pure

@[simp]
theorem isUnit_iff_singleton : IsUnit f ↔ ∃ a, f = pure a := by
  simp only [isUnit_iff, Group.isUnit, and_true_iff]
#align filter.is_unit_iff_singleton Filter.isUnit_iff_singleton

@[to_additive]
theorem map_inv' : f⁻¹.map m = (f.map m)⁻¹ :=
  Semiconj.filter_map (map_inv m) f
#align filter.map_inv' Filter.map_inv'
#align filter.map_neg' Filter.map_neg'

@[to_additive]
protected theorem Tendsto.inv_inv : Tendsto m f₁ f₂ → Tendsto m f₁⁻¹ f₂⁻¹ := fun hf =>
  (Filter.map_inv' m).trans_le <| Filter.inv_le_inv hf
#align filter.tendsto.inv_inv Filter.Tendsto.inv_inv
#align filter.tendsto.neg_neg Filter.Tendsto.neg_neg

@[to_additive]
protected theorem map_div : (f / g).map m = f.map m / g.map m :=
  map_map₂_distrib <| map_div m
#align filter.map_div Filter.map_div
#align filter.map_sub Filter.map_sub

@[to_additive]
protected theorem Tendsto.div_div (hf : Tendsto m f₁ f₂) (hg : Tendsto m g₁ g₂) :
    Tendsto m (f₁ / g₁) (f₂ / g₂) :=
  (Filter.map_div m).trans_le <| Filter.div_le_div hf hg
#align filter.tendsto.div_div Filter.Tendsto.div_div
#align filter.tendsto.sub_sub Filter.Tendsto.sub_sub

end Group

open Pointwise

section GroupWithZero

variable [GroupWithZero α] {f g : Filter α}

theorem NeBot.div_zero_nonneg (hf : f.NeBot) : 0 ≤ f / 0 :=
  Filter.le_div_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, div_zero _⟩
#align filter.ne_bot.div_zero_nonneg Filter.NeBot.div_zero_nonneg

theorem NeBot.zero_div_nonneg (hg : g.NeBot) : 0 ≤ 0 / g :=
  Filter.le_div_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_div _⟩
#align filter.ne_bot.zero_div_nonneg Filter.NeBot.zero_div_nonneg

end GroupWithZero

/-! ### Scalar addition/multiplication of filters -/


section SMul

variable [SMul α β] {f f₁ f₂ : Filter α} {g g₁ g₂ h : Filter β} {s : Set α} {t : Set β} {a : α}
  {b : β}

/-- The filter `f • g` is generated by `{s • t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
@[to_additive "The filter `f +ᵥ g` is generated by `{s +ᵥ t | s ∈ f, t ∈ g}` in locale
 `Pointwise`."]
protected def instSMul : SMul (Filter α) (Filter β) :=
  ⟨/- This is defeq to `map₂ (· • ·) f g`, but the hypothesis unfolds to `t₁ • t₂ ⊆ s`
  rather than all the way to `Set.image2 (· • ·) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· • ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ s } }⟩
#align filter.has_smul Filter.instSMul
#align filter.has_vadd Filter.instVAdd

scoped[Pointwise] attribute [instance] Filter.instSMul Filter.instVAdd

@[to_additive (attr := simp)]
theorem map₂_smul : map₂ (· • ·) f g = f • g :=
  rfl
#align filter.map₂_smul Filter.map₂_smul
#align filter.map₂_vadd Filter.map₂_vadd

@[to_additive]
theorem mem_smul : t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t :=
  Iff.rfl
#align filter.mem_smul Filter.mem_smul
#align filter.mem_vadd Filter.mem_vadd

@[to_additive]
theorem smul_mem_smul : s ∈ f → t ∈ g → s • t ∈ f • g :=
  image2_mem_map₂
#align filter.smul_mem_smul Filter.smul_mem_smul
#align filter.vadd_mem_vadd Filter.vadd_mem_vadd

@[to_additive (attr := simp)]
theorem bot_smul : (⊥ : Filter α) • g = ⊥ :=
  map₂_bot_left
#align filter.bot_smul Filter.bot_smul
#align filter.bot_vadd Filter.bot_vadd

@[to_additive (attr := simp)]
theorem smul_bot : f • (⊥ : Filter β) = ⊥ :=
  map₂_bot_right
#align filter.smul_bot Filter.smul_bot
#align filter.vadd_bot Filter.vadd_bot

@[to_additive (attr := simp)]
theorem smul_eq_bot_iff : f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff
#align filter.smul_eq_bot_iff Filter.smul_eq_bot_iff
#align filter.vadd_eq_bot_iff Filter.vadd_eq_bot_iff

@[to_additive (attr := simp)]
theorem smul_neBot_iff : (f • g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff
#align filter.smul_ne_bot_iff Filter.smul_neBot_iff
#align filter.vadd_ne_bot_iff Filter.vadd_neBot_iff

@[to_additive]
protected theorem NeBot.smul : NeBot f → NeBot g → NeBot (f • g) :=
  NeBot.map₂
#align filter.ne_bot.smul Filter.NeBot.smul
#align filter.ne_bot.vadd Filter.NeBot.vadd

@[to_additive]
theorem NeBot.of_smul_left : (f • g).NeBot → f.NeBot :=
  NeBot.of_map₂_left
#align filter.ne_bot.of_smul_left Filter.NeBot.of_smul_left
#align filter.ne_bot.of_vadd_left Filter.NeBot.of_vadd_left

@[to_additive]
theorem NeBot.of_smul_right : (f • g).NeBot → g.NeBot :=
  NeBot.of_map₂_right
#align filter.ne_bot.of_smul_right Filter.NeBot.of_smul_right
#align filter.ne_bot.of_vadd_right Filter.NeBot.of_vadd_right

@[to_additive vadd.instNeBot]
lemma smul.instNeBot [NeBot f] [NeBot g] : NeBot (f • g) := .smul ‹_› ‹_›

scoped[Pointwise] attribute [instance] smul.instNeBot vadd.instNeBot

@[to_additive (attr := simp)]
theorem pure_smul : (pure a : Filter α) • g = g.map (a • ·) :=
  map₂_pure_left
#align filter.pure_smul Filter.pure_smul
#align filter.pure_vadd Filter.pure_vadd

@[to_additive (attr := simp)]
theorem smul_pure : f • pure b = f.map (· • b) :=
  map₂_pure_right
#align filter.smul_pure Filter.smul_pure
#align filter.vadd_pure Filter.vadd_pure

@[to_additive]
-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it.
theorem pure_smul_pure : (pure a : Filter α) • (pure b : Filter β) = pure (a • b) :=
  map₂_pure
#align filter.pure_smul_pure Filter.pure_smul_pure
#align filter.pure_vadd_pure Filter.pure_vadd_pure

@[to_additive]
theorem smul_le_smul : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ • g₁ ≤ f₂ • g₂ :=
  map₂_mono
#align filter.smul_le_smul Filter.smul_le_smul
#align filter.vadd_le_vadd Filter.vadd_le_vadd

@[to_additive]
theorem smul_le_smul_left : g₁ ≤ g₂ → f • g₁ ≤ f • g₂ :=
  map₂_mono_left
#align filter.smul_le_smul_left Filter.smul_le_smul_left
#align filter.vadd_le_vadd_left Filter.vadd_le_vadd_left

@[to_additive]
theorem smul_le_smul_right : f₁ ≤ f₂ → f₁ • g ≤ f₂ • g :=
  map₂_mono_right
#align filter.smul_le_smul_right Filter.smul_le_smul_right
#align filter.vadd_le_vadd_right Filter.vadd_le_vadd_right

@[to_additive (attr := simp)]
theorem le_smul_iff : h ≤ f • g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s • t ∈ h :=
  le_map₂_iff
#align filter.le_smul_iff Filter.le_smul_iff
#align filter.le_vadd_iff Filter.le_vadd_iff

@[to_additive]
instance covariant_smul : CovariantClass (Filter α) (Filter β) (· • ·) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_left⟩
#align filter.covariant_smul Filter.covariant_smul
#align filter.covariant_vadd Filter.covariant_vadd

end SMul

/-! ### Scalar subtraction of filters -/


section Vsub

variable [VSub α β] {f f₁ f₂ g g₁ g₂ : Filter β} {h : Filter α} {s t : Set β} {a b : β}

/-- The filter `f -ᵥ g` is generated by `{s -ᵥ t | s ∈ f, t ∈ g}` in locale `Pointwise`. -/
protected def instVSub : VSub (Filter α) (Filter β) :=
  ⟨/- This is defeq to `map₂ (-ᵥ) f g`, but the hypothesis unfolds to `t₁ -ᵥ t₂ ⊆ s` rather than all
  the way to `Set.image2 (-ᵥ) t₁ t₂ ⊆ s`. -/
  fun f g => { map₂ (· -ᵥ ·) f g with sets := { s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s } }⟩
#align filter.has_vsub Filter.instVSub

scoped[Pointwise] attribute [instance] Filter.instVSub

@[simp]
theorem map₂_vsub : map₂ (· -ᵥ ·) f g = f -ᵥ g :=
  rfl
#align filter.map₂_vsub Filter.map₂_vsub

theorem mem_vsub {s : Set α} : s ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s :=
  Iff.rfl
#align filter.mem_vsub Filter.mem_vsub

theorem vsub_mem_vsub : s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g :=
  image2_mem_map₂
#align filter.vsub_mem_vsub Filter.vsub_mem_vsub

@[simp]
theorem bot_vsub : (⊥ : Filter β) -ᵥ g = ⊥ :=
  map₂_bot_left
#align filter.bot_vsub Filter.bot_vsub

@[simp]
theorem vsub_bot : f -ᵥ (⊥ : Filter β) = ⊥ :=
  map₂_bot_right
#align filter.vsub_bot Filter.vsub_bot

@[simp]
theorem vsub_eq_bot_iff : f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff
#align filter.vsub_eq_bot_iff Filter.vsub_eq_bot_iff

@[simp]
theorem vsub_neBot_iff : (f -ᵥ g : Filter α).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff
#align filter.vsub_ne_bot_iff Filter.vsub_neBot_iff

protected theorem NeBot.vsub : NeBot f → NeBot g → NeBot (f -ᵥ g) :=
  NeBot.map₂
#align filter.ne_bot.vsub Filter.NeBot.vsub

theorem NeBot.of_vsub_left : (f -ᵥ g : Filter α).NeBot → f.NeBot :=
  NeBot.of_map₂_left
#align filter.ne_bot.of_vsub_left Filter.NeBot.of_vsub_left

theorem NeBot.of_vsub_right : (f -ᵥ g : Filter α).NeBot → g.NeBot :=
  NeBot.of_map₂_right
#align filter.ne_bot.of_vsub_right Filter.NeBot.of_vsub_right

lemma vsub.instNeBot [NeBot f] [NeBot g] : NeBot (f -ᵥ g) := .vsub ‹_› ‹_›

scoped[Pointwise] attribute [instance] vsub.instNeBot

@[simp]
theorem pure_vsub : (pure a : Filter β) -ᵥ g = g.map (a -ᵥ ·) :=
  map₂_pure_left
#align filter.pure_vsub Filter.pure_vsub

@[simp]
theorem vsub_pure : f -ᵥ pure b = f.map (· -ᵥ b) :=
  map₂_pure_right
#align filter.vsub_pure Filter.vsub_pure

-- Porting note (#11119): removed `simp` attribute because `simpNF` says it can prove it.
theorem pure_vsub_pure : (pure a : Filter β) -ᵥ pure b = (pure (a -ᵥ b) : Filter α) :=
  map₂_pure
#align filter.pure_vsub_pure Filter.pure_vsub_pure

theorem vsub_le_vsub : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂ :=
  map₂_mono
#align filter.vsub_le_vsub Filter.vsub_le_vsub

theorem vsub_le_vsub_left : g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂ :=
  map₂_mono_left
#align filter.vsub_le_vsub_left Filter.vsub_le_vsub_left

theorem vsub_le_vsub_right : f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g :=
  map₂_mono_right
#align filter.vsub_le_vsub_right Filter.vsub_le_vsub_right

@[simp]
theorem le_vsub_iff : h ≤ f -ᵥ g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → s -ᵥ t ∈ h :=
  le_map₂_iff
#align filter.le_vsub_iff Filter.le_vsub_iff

end Vsub

/-! ### Translation/scaling of filters -/


section SMul

variable [SMul α β] {f f₁ f₂ : Filter β} {s : Set β} {a : α}

/-- `a • f` is the map of `f` under `a •` in locale `Pointwise`. -/
@[to_additive "`a +ᵥ f` is the map of `f` under `a +ᵥ` in locale `Pointwise`."]
protected def instSMulFilter : SMul α (Filter β) :=
  ⟨fun a => map (a • ·)⟩
#align filter.has_smul_filter Filter.instSMulFilter
#align filter.has_vadd_filter Filter.instVAddFilter

scoped[Pointwise] attribute [instance] Filter.instSMulFilter Filter.instVAddFilter

@[to_additive (attr := simp)]
protected theorem map_smul : map (fun b => a • b) f = a • f :=
  rfl
#align filter.map_smul Filter.map_smul
#align filter.map_vadd Filter.map_vadd

@[to_additive]
theorem mem_smul_filter : s ∈ a • f ↔ (a • ·) ⁻¹' s ∈ f := Iff.rfl
#align filter.mem_smul_filter Filter.mem_smul_filter
#align filter.mem_vadd_filter Filter.mem_vadd_filter

@[to_additive]
theorem smul_set_mem_smul_filter : s ∈ f → a • s ∈ a • f :=
  image_mem_map
#align filter.smul_set_mem_smul_filter Filter.smul_set_mem_smul_filter
#align filter.vadd_set_mem_vadd_filter Filter.vadd_set_mem_vadd_filter

@[to_additive (attr := simp)]
theorem smul_filter_bot : a • (⊥ : Filter β) = ⊥ :=
  map_bot
#align filter.smul_filter_bot Filter.smul_filter_bot
#align filter.vadd_filter_bot Filter.vadd_filter_bot

@[to_additive (attr := simp)]
theorem smul_filter_eq_bot_iff : a • f = ⊥ ↔ f = ⊥ :=
  map_eq_bot_iff
#align filter.smul_filter_eq_bot_iff Filter.smul_filter_eq_bot_iff
#align filter.vadd_filter_eq_bot_iff Filter.vadd_filter_eq_bot_iff

@[to_additive (attr := simp)]
theorem smul_filter_neBot_iff : (a • f).NeBot ↔ f.NeBot :=
  map_neBot_iff _
#align filter.smul_filter_ne_bot_iff Filter.smul_filter_neBot_iff
#align filter.vadd_filter_ne_bot_iff Filter.vadd_filter_neBot_iff

@[to_additive]
theorem NeBot.smul_filter : f.NeBot → (a • f).NeBot := fun h => h.map _
#align filter.ne_bot.smul_filter Filter.NeBot.smul_filter
#align filter.ne_bot.vadd_filter Filter.NeBot.vadd_filter

@[to_additive]
theorem NeBot.of_smul_filter : (a • f).NeBot → f.NeBot :=
  NeBot.of_map
#align filter.ne_bot.of_smul_filter Filter.NeBot.of_smul_filter
#align filter.ne_bot.of_vadd_filter Filter.NeBot.of_vadd_filter

@[to_additive vadd_filter.instNeBot]
lemma smul_filter.instNeBot [NeBot f] : NeBot (a • f) := .smul_filter ‹_›

scoped[Pointwise] attribute [instance] smul_filter.instNeBot vadd_filter.instNeBot

@[to_additive]
theorem smul_filter_le_smul_filter (hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂ :=
  map_mono hf
#align filter.smul_filter_le_smul_filter Filter.smul_filter_le_smul_filter
#align filter.vadd_filter_le_vadd_filter Filter.vadd_filter_le_vadd_filter

@[to_additive]
instance covariant_smul_filter : CovariantClass α (Filter β) (· • ·) (· ≤ ·) :=
  ⟨fun _ => @map_mono β β _⟩
#align filter.covariant_smul_filter Filter.covariant_smul_filter
#align filter.covariant_vadd_filter Filter.covariant_vadd_filter

end SMul

open Pointwise

@[to_additive]
instance smulCommClass_filter [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass α β (Filter γ) :=
  ⟨fun _ _ _ => map_comm (funext <| smul_comm _ _) _⟩
#align filter.smul_comm_class_filter Filter.smulCommClass_filter
#align filter.vadd_comm_class_filter Filter.vaddCommClass_filter

@[to_additive]
instance smulCommClass_filter' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass α (Filter β) (Filter γ) :=
  ⟨fun a _ _ => map_map₂_distrib_right <| smul_comm a⟩
#align filter.smul_comm_class_filter' Filter.smulCommClass_filter'
#align filter.vadd_comm_class_filter' Filter.vaddCommClass_filter'

@[to_additive]
instance smulCommClass_filter'' [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass (Filter α) β (Filter γ) :=
  haveI := SMulCommClass.symm α β γ
  SMulCommClass.symm _ _ _
#align filter.smul_comm_class_filter'' Filter.smulCommClass_filter''
#align filter.vadd_comm_class_filter'' Filter.vaddCommClass_filter''

@[to_additive]
instance smulCommClass [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
    SMulCommClass (Filter α) (Filter β) (Filter γ) :=
  ⟨fun _ _ _ => map₂_left_comm smul_comm⟩
#align filter.smul_comm_class Filter.smulCommClass
#align filter.vadd_comm_class Filter.vaddCommClass

@[to_additive vaddAssocClass]
instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower α β (Filter γ) :=
  ⟨fun a b f => by simp only [← Filter.map_smul, map_map, smul_assoc]; rfl⟩
#align filter.is_scalar_tower Filter.isScalarTower
#align filter.vadd_assoc_class Filter.vaddAssocClass

@[to_additive vaddAssocClass']
instance isScalarTower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower α (Filter β) (Filter γ) :=
  ⟨fun a f g => by
    refine' (map_map₂_distrib_left fun _ _ => _).symm
    exact (smul_assoc a _ _).symm⟩
#align filter.is_scalar_tower' Filter.isScalarTower'
#align filter.vadd_assoc_class' Filter.vaddAssocClass'

@[to_additive vaddAssocClass'']
instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
    IsScalarTower (Filter α) (Filter β) (Filter γ) :=
  ⟨fun _ _ _ => map₂_assoc smul_assoc⟩
#align filter.is_scalar_tower'' Filter.isScalarTower''
#align filter.vadd_assoc_class'' Filter.vaddAssocClass''

@[to_additive]
instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :
    IsCentralScalar α (Filter β) :=
  ⟨fun _ f => (congr_arg fun m => map m f) <| funext fun _ => op_smul_eq_smul _ _⟩
#align filter.is_central_scalar Filter.isCentralScalar
#align filter.is_central_vadd Filter.isCentralVAdd

/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
`Filter α` on `Filter β`. -/
@[to_additive "An additive action of an additive monoid `α` on a type `β` gives an additive action
 of `Filter α` on `Filter β`"]
protected def mulAction [Monoid α] [MulAction α β] : MulAction (Filter α) (Filter β) where
  one_smul f := map₂_pure_left.trans <| by simp_rw [one_smul, map_id']
  mul_smul f g h := map₂_assoc mul_smul
#align filter.mul_action Filter.mulAction
#align filter.add_action Filter.addAction

/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Filter β`.
-/
@[to_additive "An additive action of an additive monoid on a type `β` gives an additive action on
 `Filter β`."]
protected def mulActionFilter [Monoid α] [MulAction α β] : MulAction α (Filter β) where
  mul_smul a b f := by simp only [← Filter.map_smul, map_map, Function.comp, ← mul_smul]
  one_smul f := by simp only [← Filter.map_smul, one_smul, map_id']
#align filter.mul_action_filter Filter.mulActionFilter
#align filter.add_action_filter Filter.addActionFilter

scoped[Pointwise] attribute [instance] Filter.mulAction Filter.addAction Filter.mulActionFilter
  Filter.addActionFilter

/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Filter β`. -/
protected def distribMulActionFilter [Monoid α] [AddMonoid β] [DistribMulAction α β] :
    DistribMulAction α (Filter β) where
  smul_add _ _ _ := map_map₂_distrib <| smul_add _
  smul_zero _ := (map_pure _ _).trans <| by rw [smul_zero, pure_zero]
#align filter.distrib_mul_action_filter Filter.distribMulActionFilter

/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
protected def mulDistribMulActionFilter [Monoid α] [Monoid β] [MulDistribMulAction α β] :
    MulDistribMulAction α (Set β) where
  smul_mul _ _ _ := image_image2_distrib <| smul_mul' _
  smul_one _ := image_singleton.trans <| by rw [smul_one, singleton_one]
#align filter.mul_distrib_mul_action_filter Filter.mulDistribMulActionFilter

scoped[Pointwise]
  attribute [instance] Filter.distribMulActionFilter Filter.mulDistribMulActionFilter

section SMulWithZero

variable [Zero α] [Zero β] [SMulWithZero α β] {f : Filter α} {g : Filter β}

/-!
Note that we have neither `SMulWithZero α (Filter β)` nor `SMulWithZero (Filter α) (Filter β)`
because `0 * ⊥ ≠ 0`.
-/

theorem NeBot.smul_zero_nonneg (hf : f.NeBot) : 0 ≤ f • (0 : Filter β) :=
  le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, smul_zero _⟩
#align filter.ne_bot.smul_zero_nonneg Filter.NeBot.smul_zero_nonneg

theorem NeBot.zero_smul_nonneg (hg : g.NeBot) : 0 ≤ (0 : Filter α) • g :=
  le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_smul _ _⟩
#align filter.ne_bot.zero_smul_nonneg Filter.NeBot.zero_smul_nonneg

theorem zero_smul_filter_nonpos : (0 : α) • g ≤ 0 := by
  refine' fun s hs => mem_smul_filter.2 _
  convert @univ_mem _ g
  refine' eq_univ_iff_forall.2 fun a => _
  rwa [mem_preimage, zero_smul]
#align filter.zero_smul_filter_nonpos Filter.zero_smul_filter_nonpos

theorem zero_smul_filter (hg : g.NeBot) : (0 : α) • g = 0 :=
  zero_smul_filter_nonpos.antisymm <|
    le_map_iff.2 fun s hs => by
      simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
      exact zero_mem_zero
#align filter.zero_smul_filter Filter.zero_smul_filter

end SMulWithZero

end Filter