awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
⊢ Eq (α := Filter ((i : ι) → α i)) (Filter.coprodᵢ (α := α) fun (x : ι) ↦ ⊥) ⊥

Tactic:
coprodᵢ_bot'

Premises used: Filter.coprodᵢ_bot'
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
h : (f i).NeBot
⊢ (Filter.coprodᵢ (α := α) f).NeBot

Tactic:
coprodᵢ_neBot_iff.2 ⟨i, h⟩

Premises used: Iff.mpr, Filter.coprodᵢ_neBot_iff, Exists.intro
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_1 : Nonempty ι
f : (i : ι) → Filter (α i)
H : ∀ (i : ι), (f i).NeBot
⊢ (Filter.coprodᵢ (α := α) f).NeBot

Tactic:
(H (Classical.arbitrary ι)).coprodᵢ

Premises used: Filter.NeBot.coprodᵢ, Classical.arbitrary
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
hf : ∀ (i : ι), f₁ i ≤ f₂ i
⊢ Filter.coprodᵢ (α := α) f₁ ≤ Filter.coprodᵢ (α := α) f₂

Tactic:
iSup_mono fun i => comap_mono (hf i)

Premises used: Set.Mem, Filter.comap_mono, iSup_mono
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
simp :
  ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ (t₁ : Set (β i)), m i ⁻¹' t₁ ∈ f i ∧ eval (β := β) i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' x
⊢ LE.le (α := Filter ((i : ι) → β i)) (map (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) (Filter.coprodᵢ (α := α) f))
    (Filter.coprodᵢ (α := β) fun (i : ι) ↦ map (m i) (f i))

Tactic:
simp only [le_def, mem_map, mem_coprodᵢ_iff]

Premises used: Filter.mem_coprodᵢ_iff, Filter.mem_map, Filter.le_def
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ (t₁ : Set (β i)), m i ⁻¹' t₁ ∈ f i ∧ eval (β := β) i ⁻¹' t₁ ⊆ s
i : ι
obtain :
  ∀ (t : Set (β i)) (H : m i ⁻¹' t ∈ f i) (hH : eval (β := β) i ⁻¹' t ⊆ s),
    ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' s
⊢ ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' s

Tactic:
obtain ⟨t, H, hH⟩ := h i
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ (t₁ : Set (β i)), m i ⁻¹' t₁ ∈ f i ∧ eval (β := β) i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval (β := β) i ⁻¹' t ⊆ s
⊢ ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' s

Tactic:
⟨{ x : α i | m i x ∈ t }, H, fun x hx => hH hx⟩

Premises used: setOf, Membership.mem, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ (t₁ : Set (β i)), m i ⁻¹' t₁ ∈ f i ∧ eval (β := β) i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval (β := β) i ⁻¹' t ⊆ s
⊢ ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' s

Tactic:
exact ⟨{ x : α i | m i x ∈ t }, H, fun x hx => hH hx⟩
-- Module: Mathlib.Order.Filter.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
g : (i : ι) → Filter (β i)
h : ∀ (i : ι), Tendsto (m i) (f i) (g i)
⊢ Tendsto (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) (Filter.coprodᵢ (α := α) f) (Filter.coprodᵢ (α := β) g)

Tactic:
map_pi_map_coprodᵢ_le.trans (coprodᵢ_mono h)

Premises used: Filter.coprodᵢ_mono, Set.Mem, Filter.map_pi_map_coprodᵢ_le, Filter.Tendsto, LE.le.trans
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
s : Set α
⊢ Membership.mem (γ := Filter α) 1 s ↔ 1 ∈ s

Tactic:
mem_pure

Premises used: Set.Mem, Filter.mem_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
⊢ Membership.mem (γ := Filter α) 1 1

Tactic:
mem_pure.2 Set.one_mem_one

Premises used: Iff.mpr, Set.Mem, Set.one_mem_one, Filter.mem_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
⊢ Eq.{u_2 + 1} (α := Filter α) (pure 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : One α
l : Filter β
⊢ SProd.sprod (α := Filter α) 1 l = map (fun (x : β) ↦ (1, x)) l

Tactic:
pure_prod

Premises used: Set.Mem, setOf, Filter.pure_prod
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : One α
l : Filter β
⊢ SProd.sprod (β := Filter α) l 1 = map (fun (x : β) ↦ (x, 1)) l

Tactic:
prod_pure

Premises used: Set.Mem, setOf, Filter.prod_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
⊢ Eq.{u_2 + 1} (α := Filter α) (𝓟 1) 1

Tactic:
principal_singleton _

Premises used: Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
⊢ NeBot.{u_2} (α := α) 1

Tactic:
Filter.pure_neBot

Premises used: Filter.pure_neBot
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : One α
f : α → β
⊢ map f 1 = pure (f 1)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
f : Filter α
⊢ f ≤ 1 ↔ 1 ∈ f

Tactic:
le_pure_iff

Premises used: Filter.le_pure_iff, Set.Mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
f : Filter α
h : f.NeBot
⊢ f ≤ 1 ↔ f = 1

Tactic:
h.le_pure_iff

Premises used: Set.Mem, Filter.NeBot.le_pure_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
p : α → Prop
⊢ (∀ᶠ (x : α) in 1, p x) ↔ p 1

Tactic:
eventually_pure

Premises used: Filter.eventually_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
p : α → Prop
⊢ (∃ᶠ (x : α) in 1, p x) ↔ p 1

Tactic:
frequently_pure

Premises used: Filter.frequently_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : One α
a : Filter β
f : β → α
⊢ Tendsto f a 1 ↔ ∀ᶠ (x : β) in a, f x = 1

Tactic:
tendsto_pure

Premises used: Filter.tendsto_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
⊢ SProd.sprod (α := Filter α) (β := Filter β) 1 1 = 1

Tactic:
prod_pure_pure

Premises used: Set.Mem, setOf, Filter.prod_pure_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
⊢ Eq.{u_2 + 1} (α := (a : α) → Filter α) (⇑pureOneHom : (a : α) → Filter α) pure

Tactic:
rfl

Premises used: Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : One α
a : α
⊢ Eq (α := Filter α) ((pureOneHom : (a : α) → Filter α) a : Filter α) (pure a : Filter α)

Tactic:
rfl

Premises used: Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
inst_2 : FunLike F α β
inst_3 : OneHomClass F α β
φ : F
⊢ Eq.{u_3 + 1} (α := Filter β) (map.{u_2, u_3} (α := α) (⇑φ : (a : α) → β) 1) 1

Tactic:
simp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
⊢ map Inv.inv f = f⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
s : Set α
⊢ s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f g : Filter α
hf : f ≤ g
⊢ f⁻¹ ≤ g⁻¹

Tactic:
map_mono hf

Premises used: Filter.map_mono, Set.Mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
a : α
⊢ Eq (α := Filter α) (pure a)⁻¹ (pure a⁻¹)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
⊢ f⁻¹ = ⊥ ↔ f = ⊥

Tactic:
map_eq_bot_iff

Premises used: Filter.map_eq_bot_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
⊢ f⁻¹.NeBot ↔ f.NeBot

Tactic:
map_neBot_iff _

Premises used: Filter.map_neBot_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
⊢ f.NeBot → f⁻¹.NeBot

Tactic:
fun h => h.map _

Premises used: Filter.NeBot.map, Inv.inv
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
inst_1 : f.NeBot
⊢ f⁻¹.NeBot

Tactic:
.inv ‹_›

Premises used: Filter.NeBot.inv
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
p : α → Prop
⊢ (∀ᶠ (x : α) in f⁻¹, p x) ↔ ∀ᶠ (x : α) in f, p x⁻¹

Tactic:
eventually_map

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Inv α
f : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in f⁻¹, p x) ↔ ∃ᶠ (x : α) in f, p x⁻¹

Tactic:
frequently_map

Premises used: Filter.frequently_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : InvolutiveInv α
f : Filter α
⊢ comap Inv.inv f = f⁻¹

Tactic:
.symm <| map_eq_comap_of_inverse (inv_comp_inv _) (inv_comp_inv _)

Premises used: Filter.map_eq_comap_of_inverse, inv_comp_inv, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
rwa : Inv.inv ⁻¹' s⁻¹ ∈ f
rwa₁ : s⁻¹⁻¹ ∈ f
rwa₂ rwa₃ rwa₄ rwa₅ : s ∈ f
⊢ s⁻¹ ∈ f⁻¹

Tactic:
rwa [mem_inv, inv_preimage, inv_inv]

Premises used: Filter.mem_inv, inv_inv, Set.inv_preimage
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : InvolutiveInv α
f : Filter α
ι : Sort u_7
p : ι → Prop
s : ι → Set α
h : f.HasBasis p s
⊢ f⁻¹.HasBasis p fun (i : ι) ↦ (s i)⁻¹

Tactic:
simpa using h.map Inv.inv

Premises used: Filter.HasBasis.map, Inv.inv
-- 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 : InvolutiveInv α
f_1 g : Filter α
s : Set α
f : Filter α
rw : map id f = f
rw₁ rw₂ : f = f
⊢ map (Inv.inv ∘ Inv.inv) f = f

Tactic:
rw [inv_involutive.comp_self, map_id]

Premises used: inv_involutive, Filter.map_id, Function.Involutive.comp_self
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : InvolutiveInv α
f g : Filter α
⊢ f⁻¹ ≤ g⁻¹ ↔ f ≤ g

Tactic:
⟨fun h => inv_inv f ▸ inv_inv g ▸ Filter.inv_le_inv h, Filter.inv_le_inv⟩

Premises used: Eq.rec, Filter.inv_le_inv, inv_inv, Iff.intro
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : InvolutiveInv α
f g : Filter α
rw : f⁻¹⁻¹ ≤ g⁻¹ ↔ f ≤ g⁻¹
rw₁ rw₂ : f ≤ g⁻¹ ↔ f ≤ g⁻¹
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹

Tactic:
rw [← Filter.inv_le_inv_iff, inv_inv]

Premises used: Filter.inv_le_inv_iff, inv_inv
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : InvolutiveInv α
f : Filter α
⊢ f⁻¹ ≤ f ↔ f⁻¹ = f

Tactic:
⟨fun h => h.antisymm <| inv_le_iff_le_inv.1 h, Eq.le⟩

Premises used: LE.le.antisymm, Eq.le, Iff.intro, Iff.mp, Filter.inv_le_iff_le_inv
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
G : Type u_7
inst : CommGroup G
inst_1 : Preorder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_7 + 1} (α := Filter G) atTop⁻¹ atBot

Tactic:
(OrderIso.inv G).map_atTop

Premises used: OrderIso.inv, setOf, Filter.atBot, Set.Iic, OrderDual, OrderIso.map_atTop
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Mul α
f g : Filter α
ιf : Type u_7
ιg : Type u_8
pf : ιf → Prop
sf : ιf → Set α
pg : ιg → Prop
sg : ιg → Set α
hf : f.HasBasis pf sf
hg : g.HasBasis pg sg
⊢ (f * g).HasBasis (fun (i : ιf × ιg) ↦ pf i.1 ∧ pg i.2) fun (i : ιf × ιg) ↦ sf i.1 * sg i.2

Tactic:
hf.map₂ (· * ·) hg

Premises used: HMul.hMul, setOf, Filter.HasBasis.map₂, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
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
inst : Mul α
f g : Filter α
inst_1 : f.NeBot
inst_2 : g.NeBot
⊢ (f * g).NeBot

Tactic:
.mul ‹_› ‹_›

Premises used: Filter.NeBot.mul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Mul α
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
inst : Mul α
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
inst : Mul α
a b : α
⊢ HMul.hMul (α := Filter α) (pure a) (pure b) = pure (a * b)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Mul α
f g 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:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Mul α
inst_1 : Mul β
f f₁ f₂ g g₁ g₂ h : Filter α
s t : Set α
a b : α
⊢ MulLeftMono.{u_2} (Filter α)

Tactic:
⟨fun _ _ _ => map₂_mono_left⟩

Premises used: CovariantClass.mk, Filter.map₂_mono_left
-- 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 : Mul α
inst_1 : Mul β
f f₁ f₂ g g₁ g₂ h : Filter α
s t : Set α
a b : α
⊢ MulRightMono.{u_2} (Filter α)

Tactic:
⟨fun _ _ _ => map₂_mono_right⟩

Premises used: CovariantClass.mk, Filter.map₂_mono_right
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Mul β
f₁ f₂ : Filter α
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
⊢ map (⇑m : (a : α) → β) (f₁ * f₂) = HMul.hMul (α := Filter β) (map (⇑m : (a : α) → β) f₁) (map (⇑m : (a : α) → β) f₂)

Tactic:
map_map₂_distrib <| map_mul m

Premises used: setOf, Filter.map_map₂_distrib, map_mul, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Mul α
⊢ Eq.{u_2 + 1} (α := (a : α) → Filter α) (⇑pureMulHom : (a : α) → Filter α) pure

Tactic:
rfl

Premises used: Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Mul α
a : α
⊢ Eq (α := Filter α) ((pureMulHom : (a : α) → Filter α) a : Filter α) (pure a : Filter α)

Tactic:
rfl

Premises used: Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Div α
f g : Filter α
ιf : Type u_7
ιg : Type u_8
pf : ιf → Prop
sf : ιf → Set α
pg : ιg → Prop
sg : ιg → Set α
hf : f.HasBasis pf sf
hg : g.HasBasis pg sg
⊢ (f / g).HasBasis (fun (i : ιf × ιg) ↦ pf i.1 ∧ pg i.2) fun (i : ιf × ιg) ↦ sf i.1 / sg i.2

Tactic:
hf.map₂ (· / ·) hg

Premises used: setOf, HDiv.hDiv, Filter.HasBasis.map₂, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
f g : Filter α
inst_1 : f.NeBot
inst_2 : g.NeBot
⊢ (f / g).NeBot

Tactic:
.div ‹_› ‹_›

Premises used: Filter.NeBot.div
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Div α
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
inst : Div α
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
inst : Div α
a b : α
⊢ HDiv.hDiv (α := Filter α) (pure a) (pure b) = pure (a / b)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Div α
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
inst : Div α
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
inst : Div α
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
inst : Div α
f g 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:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Div α
f f₁ f₂ g g₁ g₂ h : Filter α
s t : Set α
a b : α
⊢ CovariantClass.{u_2, u_2} (Filter α) (Filter α) (fun (x1 x2 : Filter α) ↦ x1 / x2) fun (x1 x2 : Filter α) ↦ x1 ≤ x2

Tactic:
⟨fun _ _ _ => map₂_mono_left⟩

Premises used: CovariantClass.mk, Filter.map₂_mono_left
-- 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 : Div α
f f₁ f₂ g g₁ g₂ h : Filter α
s t : Set α
a b : α
⊢ CovariantClass.{u_2, u_2} (Filter α) (Filter α)
    (swap (φ := fun (a a_1 : Filter α) ↦ Filter α) fun (x1 x2 : Filter α) ↦ x1 / x2) fun (x1 x2 : Filter α) ↦ x1 ≤ x2

Tactic:
⟨fun _ _ _ => map₂_mono_right⟩

Premises used: CovariantClass.mk, Filter.map₂_mono_right
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
f g : Filter β
⊢ HMul.hMul (α := Filter α) (comap (⇑m : (a : α) → β) f) (comap (⇑m : (a : α) → β) g) ≤ comap (⇑m : (a : α) → β) (f * g)

Tactic:
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⟩

Premises used: HMul.hMul, Membership.mem, Set.preimage_mul_preimage_subset, HasSubset.Subset.trans, Set.preimage_mono, Set.Subset.rfl, Set.preimage, And.intro, _private.0.Filter.comap_mul_comap_le.match_1, Exists.intro, DFunLike.coe, Filter.comap
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
m : F
f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ Tendsto (⇑m : (a : α) → β) f₁ f₂ → Tendsto (⇑m : (a : α) → β) g₁ g₂ → Tendsto (⇑m : (a : α) → β) (f₁ * g₁) (f₂ * g₂)

Tactic:
fun hf hg =>
  (Filter.map_mul m).trans_le <| mul_le_mul' hf hg

Premises used: Filter.map_mul, Eq.trans_le, Filter.Tendsto, mul_le_mul'
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : MulOneClass α
⊢ Eq.{u_2 + 1} (α := (a : α) → Filter α) (⇑pureMonoidHom : (a : α) → Filter α) pure

Tactic:
rfl

Premises used: Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : MulOneClass α
a : α
⊢ Eq (α := Filter α) ((pureMonoidHom : (a : α) → Filter α) a : Filter α) (pure a : Filter α)

Tactic:
rfl

Premises used: Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ Membership.mem (γ := Filter α) 1 (HPow.hPow (β := ℕ) s 0)

Tactic:
one_mem_one

Premises used: Set.Mem, setOf, Filter.one_mem_one, npowRec
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ Membership.mem (γ := Filter α) 1 (HPow.hPow (β := ℕ) s 0)

Tactic:
exact one_mem_one

Premises used: Filter.one_mem_one
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
rw : s ^ (n + 1) ∈ f ^ n * f
⊢ s ^ (n + 1) ∈ f ^ (n + 1)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f

Tactic:
mul_mem_mul (pow_mem_pow hs n) hs

Premises used: Set.Mem, setOf, Filter.mul_mem_mul, npowRec, Set.image2
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f

Tactic:
exact mul_mem_mul (pow_mem_pow hs n) hs

Premises used: Filter.mul_mem_mul