awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
⊢ map₂ (fun (x1 x2 : β) ↦ x1 -ᵥ x2) f g = f -ᵥ g

Tactic:
rfl

Premises used: setOf, Filter.map₂, Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
s : Set α
⊢ s ∈ f -ᵥ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ -ᵥ t₂ ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
s t : Set β
⊢ s ∈ f → t ∈ g → s -ᵥ t ∈ f -ᵥ g

Tactic:
image2_mem_map₂

Premises used: Filter.image2_mem_map₂, Set.Mem, setOf
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
g : Filter β
⊢ ⊥ -ᵥ g = ⊥

Tactic:
map₂_bot_left

Premises used: Filter.map₂_bot_left, setOf, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f : Filter β
⊢ f -ᵥ ⊥ = ⊥

Tactic:
map₂_bot_right

Premises used: Filter.map₂_bot_right, setOf, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
⊢ f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
map₂_eq_bot_iff

Premises used: setOf, Filter.map₂_eq_bot_iff, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
⊢ (f -ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
map₂_neBot_iff

Premises used: Filter.map₂_neBot_iff, setOf, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
⊢ f.NeBot → g.NeBot → (f -ᵥ g).NeBot

Tactic:
NeBot.map₂

Premises used: setOf, Filter.NeBot.map₂, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
⊢ (f -ᵥ g).NeBot → f.NeBot

Tactic:
NeBot.of_map₂_left

Premises used: setOf, Filter.NeBot.of_map₂_left, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
⊢ (f -ᵥ g).NeBot → g.NeBot

Tactic:
NeBot.of_map₂_right

Premises used: setOf, Filter.map₂, Filter.copy, Filter.NeBot.of_map₂_right
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
inst_1 : f.NeBot
inst_2 : g.NeBot
⊢ (f -ᵥ g).NeBot

Tactic:
.vsub ‹_› ‹_›

Premises used: Filter.NeBot.vsub
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
g : Filter β
a : β
⊢ pure a -ᵥ g = map (fun (x : β) ↦ a -ᵥ x) g

Tactic:
map₂_pure_left

Premises used: setOf, Filter.map₂_pure_left, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f : Filter β
b : β
⊢ f -ᵥ pure b = map (fun (x : β) ↦ x -ᵥ b) f

Tactic:
map₂_pure_right

Premises used: setOf, Filter.map₂, Filter.copy, Filter.map₂_pure_right
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
a b : β
⊢ VSub.vsub (P := Filter β) (pure a) (pure b) = pure (a -ᵥ b)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f₁ f₂ g₁ g₂ : Filter β
⊢ f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂

Tactic:
map₂_mono

Premises used: Set.Mem, setOf, Filter.map₂_mono
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g₁ g₂ : Filter β
⊢ g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂

Tactic:
map₂_mono_left

Premises used: Set.Mem, setOf, Filter.map₂_mono_left
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f₁ f₂ g : Filter β
⊢ f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g

Tactic:
map₂_mono_right

Premises used: Set.Mem, setOf, Filter.map₂_mono_right
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : VSub α β
f g : Filter β
h : Filter α
⊢ h ≤ f -ᵥ g ↔ ∀ ⦃s : Set β⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s -ᵥ t ∈ h

Tactic:
le_map₂_iff

Premises used: Set.Mem, setOf, Filter.le_map₂_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
⊢ map (fun (b : β) ↦ a • b) f = a • f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
s : Set β
a : α
⊢ s ∈ a • f ↔ (fun (x : β) ↦ a • x) ⁻¹' s ∈ f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
s : Set β
a : α
⊢ s ∈ f → a • s ∈ a • f

Tactic:
image_mem_map

Premises used: Set.Mem, Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
⊢ HSMul.hSMul (β := Filter β) a ⊥ = ⊥

Tactic:
map_bot

Premises used: Filter.map_bot
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
⊢ a • f = ⊥ ↔ f = ⊥

Tactic:
map_eq_bot_iff

Premises used: Filter.map_eq_bot_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
⊢ (a • f).NeBot ↔ f.NeBot

Tactic:
map_neBot_iff _

Premises used: Filter.map_neBot_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
⊢ f.NeBot → (a • f).NeBot

Tactic:
fun h => h.map _

Premises used: Filter.NeBot.map, HSMul.hSMul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
⊢ (a • f).NeBot → f.NeBot

Tactic:
NeBot.of_map

Premises used: Filter.NeBot.of_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
inst_1 : f.NeBot
⊢ (a • f).NeBot

Tactic:
.smul_filter ‹_›

Premises used: Filter.NeBot.smul_filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
p : β → Prop
⊢ (∀ᶠ (y : β) in a • f, p y) ↔ ∀ᶠ (x : β) in f, p (a • x)

Tactic:
eventually_map

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter β
a : α
p : β → Prop
⊢ (∃ᶠ (y : β) in a • f, p y) ↔ ∃ᶠ (x : β) in f, p (a • x)

Tactic:
frequently_map

Premises used: Filter.frequently_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f₁ f₂ : Filter β
a : α
hf : f₁ ≤ f₂
⊢ a • f₁ ≤ a • f₂

Tactic:
map_mono hf

Premises used: Filter.map_mono, Set.Mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
f f₁ f₂ : Filter β
s : Set β
a : α
⊢ CovariantClass.{u_2, u_3} α (Filter β) (fun (x1 : α) (x2 : Filter β) ↦ x1 • x2) fun (x1 x2 : Filter β) ↦ x1 ≤ x2

Tactic:
⟨fun _ => @map_mono β β _⟩

Premises used: CovariantClass.mk, Filter.map_mono
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} α β (Filter γ)

Tactic:
⟨fun _ _ _ => map_comm (funext <| smul_comm _ _) _⟩

Premises used: funext, Filter.map_comm, SMulCommClass.smul_comm, SMulCommClass.mk
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} α (Filter β) (Filter γ)

Tactic:
⟨fun a _ _ => map_map₂_distrib_right <| smul_comm a⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Filter.map_map₂_distrib_right
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} (Filter α) β (Filter γ)

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

Premises used: SMulCommClass.symm, Filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} (Filter α) (Filter β) (Filter γ)

Tactic:
⟨fun _ _ _ => map₂_left_comm smul_comm⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Filter.map₂_left_comm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
b : β
f : Filter γ
simp :
  Eq (α := Filter γ) (map (fun (b_1 : γ) ↦ a • b • b_1) f) (map ((fun (b : γ) ↦ a • b) ∘ fun (b_1 : γ) ↦ b • b_1) f)
⊢ (a • b) • f = a • b • f

Tactic:
simp only [← Filter.map_smul, map_map, smul_assoc]

Premises used: smul_assoc, Filter.map_map, Filter.map_smul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ Eq (α := Filter γ) (map (fun (b_1 : γ) ↦ a • b • b_1) f) (map ((fun (b : γ) ↦ a • b) ∘ fun (b_1 : γ) ↦ b • b_1) f)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
⊢ (a • f) • g = a • f • g

Tactic:
(map_map₂_distrib_left fun _ _ => ?_).symm

Premises used: Filter.map_map₂_distrib_left, Set.Mem, setOf, Filter.map₂, Filter.copy, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
refine : ∀ (x : β) (x_1 : γ), a • x • x_1 = (a • x) • x_1
⊢ (a • f) • g = a • f • g

Tactic:
refine (map_map₂_distrib_left fun _ _ => ?_).symm

Premises used: Filter.map_map₂_distrib_left, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
x : β
x_1 : γ
⊢ a • x • x_1 = (a • x) • x_1

Tactic:
(smul_assoc a _ _).symm

Premises used: smul_assoc, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
x : β
x_1 : γ
⊢ a • x • x_1 = (a • x) • x_1

Tactic:
exact (smul_assoc a _ _).symm

Premises used: smul_assoc, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
⊢ IsScalarTower.{u_2, u_3, u_4} (Filter α) (Filter β) (Filter γ)

Tactic:
⟨fun _ _ _ => map₂_assoc smul_assoc⟩

Premises used: smul_assoc, Filter.map₂_assoc, IsScalarTower.mk
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_2 : IsCentralScalar α β
⊢ IsCentralScalar.{u_2, u_3} α (Filter β)

Tactic:
⟨fun _ f => (congr_arg fun m => map m f) <| funext fun _ => op_smul_eq_smul _ _⟩

Premises used: Filter.map, congr_arg, funext, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : MulAction α β
f : Filter β
simp_rw : map (fun (x2 : β) ↦ x2) f = f
⊢ map (fun (x2 : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 x2) f = f

Tactic:
simp_rw [one_smul, map_id']

Premises used: one_smul, Filter.map_id'
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : MulAction α β
a b : α
f : Filter β
⊢ (a * b) • f = a • b • f

Tactic:
simp only [← Filter.map_smul, map_map, Function.comp_def, ← mul_smul]

Premises used: Filter.map_map, Function.comp_def, Filter.map_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : MulAction α β
f : Filter β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 f = f

Tactic:
simp only [← Filter.map_smul, one_smul, map_id']

Premises used: one_smul, Filter.map_smul, Filter.map_id'
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
x : α
rw : Eq.{u_3 + 1} (α := Filter β) (pure 0) 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := Filter β) 0 0
⊢ Eq (α := Filter β) (pure (HSMul.hSMul (β := β) x 0)) 0

Tactic:
rw [smul_zero, pure_zero]

Premises used: Filter.pure_zero, smul_zero
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : Monoid β
inst_2 : MulDistribMulAction α β
x : α
rw : Eq (α := Set β) {1} 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := Set β) 1 1
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 1} 1

Tactic:
rw [smul_one, singleton_one]

Premises used: MulDistribMulAction.smul_one, Set.singleton_one
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
f : Filter α
hf : f.NeBot
⊢ 0 ≤ HSMul.hSMul (β := Filter β) f 0

Tactic:
le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, smul_zero _⟩

Premises used: Iff.mpr, _private.0.Filter.NeBot.mul_zero_nonneg.match_1, Filter.le_smul_iff, smul_zero, Membership.mem, And.intro, Exists.intro, HSMul.hSMul, Filter.NeBot.nonempty_of_mem, OfNat.ofNat
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
hg : g.NeBot
⊢ 0 ≤ HSMul.hSMul.{u_2, u_3, u_3} (α := Filter α) 0 g

Tactic:
le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_smul _ _⟩

Premises used: Iff.mpr, _private.0.Filter.NeBot.mul_zero_nonneg.match_1, Filter.le_smul_iff, Membership.mem, zero_smul, And.intro, Exists.intro, HSMul.hSMul, Filter.NeBot.nonempty_of_mem, OfNat.ofNat
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 g ≤ 0

Tactic:
fun s hs => mem_smul_filter.2 ?_

Premises used: Iff.mpr, Filter.mem_smul_filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
refine :
  ∀ (s : Set β) (hs : Membership.mem (γ := Filter β) 0 s),
    (fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s ∈ g
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 g ≤ 0

Tactic:
refine fun s hs => mem_smul_filter.2 ?_

Premises used: Iff.mpr, Filter.mem_smul_filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
⊢ univ ∈ g

Tactic:
@univ_mem _ g

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
h : Eq (α := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) univ
⊢ (fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s ∈ g

Tactic:
convert! @univ_mem _ g

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
⊢ Eq (α := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) univ

Tactic:
eq_univ_iff_forall.2 fun a => ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
h : ∀ (a : β), Membership.mem (γ := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) a
⊢ Eq (α := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) univ

Tactic:
refine eq_univ_iff_forall.2 fun a => ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
a : β
h : HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 a ∈ s
h₁ h₂ h₃ h₄ : 0 ∈ s
⊢ Membership.mem (γ := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) a

Tactic:
rwa [mem_preimage, zero_smul]

Premises used: zero_smul, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
simp_rw : Membership.mem (γ := Filter β) 0 {0}
⊢ Membership.mem (γ := Filter β) 0 ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) '' s)

Tactic:
simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]

Premises used: Set.Nonempty.image_const, zero_smul, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ Membership.mem (γ := Filter β) 0 {0}

Tactic:
zero_mem_zero

Premises used: Set.Mem, setOf, Filter.zero_mem_zero
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ Membership.mem (γ := Filter β) 0 {0}

Tactic:
exact zero_mem_zero

Premises used: Filter.zero_mem_zero
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
rcases : ∀ (d : γ) (hd : d * c = 1), Tendsto (c • m) f (c • g) ↔ Tendsto m f g
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
rcases hc.exists_left_inv with ⟨d, hd⟩

Premises used: IsUnit.exists_left_inv
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
⟨fun H ↦ ?_, fun H ↦ tendsto_map.comp H⟩

Premises used: Filter.tendsto_map, Iff.intro, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
refine : ∀ (H : Tendsto (c • m) f (c • g)), Tendsto m f g
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ tendsto_map.comp H⟩
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
H : Tendsto (c • m) f (c • g)
⊢ Tendsto m f g

Tactic:
simpa [Function.comp_def, smul_smul, hd] using (tendsto_map (f := (d • ·))).comp H

Premises used: smul_smul, Filter.tendsto_map, Function.comp_def, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Group γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
Group.isUnit _ |>.smul_tendsto_smul_iff

Premises used: Group.isUnit, IsUnit.smul_tendsto_smul_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : GroupWithZero γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : c ≠ 0
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
hc.isUnit.smul_tendsto_smul_iff

Premises used: Ne.isUnit, IsUnit.smul_tendsto_smul_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : Filter α
g : Filter β
hs : s ∈ f
ht : t ∈ g
⊢ s ×ˢ t ∈ f ×ˢ g

Tactic:
inter_mem_inf (preimage_mem_comap hs) (preimage_mem_comap ht)

Premises used: Filter.inter_mem_inf, Set.Mem, setOf, Set.prod, Filter.preimage_mem_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
mp : s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
mpr : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g
⊢ s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1 ∈ f, ∃ t₂_1 ∈ g, t₁_1 ×ˢ t₂_1 ⊆ t₁ ∩ t₂

Tactic:
⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩

Premises used: _private.0.Filter.mem_prod_iff.match_1, Membership.mem, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1 ∈ f, ∃ t₂_1 ∈ g, t₁_1 ×ˢ t₂_1 ⊆ t₁ ∩ t₂

Tactic:
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : t₁ ×ˢ t₂ ⊆ s
⊢ s ∈ f ×ˢ g

Tactic:
mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h

Premises used: Filter.mem_inf_of_inter, Set.Mem, Filter.preimage_mem_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : t₁ ×ˢ t₂ ⊆ s
⊢ s ∈ f ×ˢ g

Tactic:
exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h

Premises used: Filter.mem_inf_of_inter, Filter.preimage_mem_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
l₁ l₂ : Filter α
⊢ (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

Tactic:
simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]

Premises used: Filter.disjoint_iff, Filter.mem_prod_iff, Set.prod_subset_compl_diagonal_iff_disjoint
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : Filter α
g : Filter β
inst : f.NeBot
inst_1 : g.NeBot
⊢ s ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g

Tactic:
⟨fun h =>
    let ⟨_s', hs', _t', ht', H⟩ := mem_prod_iff.1 h
    (prod_subset_prod_iff.1 H).elim
      (fun ⟨hs's, ht't⟩ => ⟨mem_of_superset hs' hs's, mem_of_superset ht' ht't⟩) fun h =>
      h.elim (fun hs'e => absurd hs'e (nonempty_of_mem hs').ne_empty) fun ht'e =>
        absurd ht'e (nonempty_of_mem ht').ne_empty,
    fun h => prod_mem_prod h.1 h.2⟩

Premises used: Set.prod_subset_prod_iff, Set.Nonempty.ne_empty, Membership.mem, _private.0.Filter.prod_mem_prod_iff.match_2, Filter.nonempty_of_mem, And, absurd, And.right, And.left, And.intro, Iff.intro, Iff.mp, Filter.prod_mem_prod, Or.elim, Filter.mem_prod_iff, _private.0.Filter.prod_mem_prod_iff.match_1, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
rw : (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a : α | ∀ b ∈ t, (a, b) ∈ s} ∈ f

Tactic:
rw [← @exists_mem_subset_iff _ f, mem_prod_iff]

Premises used: Filter.exists_mem_subset_iff, Filter.mem_prod_iff