awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (α := Filter α) ⊥ (n - 1 + 1) = ⊥
rw₁ : ⊥ * HPow.hPow (α := Filter α) ⊥ (n - 1) = ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Filter α) ⊥ ⊥
⊢ HPow.hPow (α := Filter α) ⊥ n = ⊥

Tactic:
rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]

Premises used: Filter.bot_mul, Nat.sub_one_add_one, pow_succ'
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ f * ⊤ = ⊤

Tactic:
top_le_iff.1 fun s => ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
refine : ∀ s ∈ f * ⊤, Membership.mem (γ := Filter α) ⊤ s
⊢ f * ⊤ = ⊤

Tactic:
refine top_le_iff.1 fun s => ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
simp : (∃ t₁ ∈ f, t₁ * univ ⊆ s) → s = univ
⊢ s ∈ f * ⊤ → Membership.mem (γ := Filter α) ⊤ s

Tactic:
simp only [mem_mul, mem_top, exists_eq_left]

Premises used: Filter.mem_mul, exists_eq_left, Filter.mem_top
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
rwa : ∀ (hs : univ ⊆ s), s = univ
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hs : s = univ), s = univ
⊢ s = univ

Tactic:
rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Premises used: Set.univ_subset_iff, Filter.mem_one, Iff.mp, Set.mul_univ_of_one_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ ⊤ * f = ⊤

Tactic:
top_le_iff.1 fun s => ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
refine : ∀ s ∈ ⊤ * f, Membership.mem (γ := Filter α) ⊤ s
⊢ ⊤ * f = ⊤

Tactic:
refine top_le_iff.1 fun s => ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
simp : (∃ t₂ ∈ f, univ * t₂ ⊆ s) → s = univ
⊢ s ∈ ⊤ * f → Membership.mem (γ := Filter α) ⊤ s

Tactic:
simp only [mem_mul, mem_top, exists_eq_left]

Premises used: Filter.mem_mul, exists_eq_left, Filter.mem_top
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
rwa : ∀ (hs : univ ⊆ s), s = univ
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hs : s = univ), s = univ
⊢ s = univ

Tactic:
rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Premises used: Set.univ_subset_iff, Filter.mem_one, Iff.mp, Set.univ_mul_of_one_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
⊢ HMul.hMul (α := Filter α) ⊤ ⊤ = ⊤

Tactic:
mul_top_of_one_le le_top

Premises used: le_top, Filter.mul_top_of_one_le
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Filter α) ⊤ (n + 1) * ⊤ = ⊤
rw₁ : HMul.hMul (α := Filter α) ⊤ ⊤ = ⊤
rw₂ rw₃ : Eq.{u_2 + 1} (α := Filter α) ⊤ ⊤
⊢ HPow.hPow (α := Filter α) ⊤ (n + 2) = ⊤

Tactic:
rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]

Premises used: pow_succ, Filter.top_mul_top, Nat.succ_ne_zero
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Monoid α
a : α
⊢ IsUnit a → IsUnit (M := Filter α) (pure a)

Tactic:
IsUnit.map (pureMonoidHom : α →* Filter α)

Premises used: Filter.pureMonoidHom, IsUnit.map, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
⟨fun hfg => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
refine_1 : ∀ (hfg : f * g = 1), ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
refine_2 : (∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1
⊢ f * g = 1 ↔ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
refine ⟨fun hfg => ?_, ?_⟩
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ 1 ∈ f * g

Tactic:
hfg.symm ▸ one_mem_one

Premises used: Eq.rec, Filter.one_mem_one, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
refine_1 :
  ∀ (t₁ : Set α) (h₁ : t₁ ∈ f) (t₂ : Set α) (h₂ : t₂ ∈ g) (h : t₁ * t₂ ⊆ 1),
    ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm ▸ one_mem_one

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
⊢ (f * g).NeBot

Tactic:
have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : (f * g).NeBot
⊢ ∃ (a : α) (b : α), t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1

Tactic:
rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h

Premises used: Filter.mul_mem_mul, Set.mul_eq_one_iff, Set.Nonempty.subset_one_iff, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : (f * g).NeBot
h₃ : ∃ (a : α) (b : α), t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
⊢ (f * g).NeBot

Tactic:
rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h

Premises used: Filter.mul_mem_mul, Set.mul_eq_one_iff, Set.Nonempty.subset_one_iff, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : ∃ (a : α) (b : α), t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : (f * g).NeBot
refine_1 :
  ∀ (a b : α) (h₁ : {a} ∈ f) (h : a * b = 1) (h₂ : {b} ∈ g), ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
obtain ⟨a, b, rfl, rfl, h⟩ := h

Premises used: rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
⟨a, b, ?_, ?_, h⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
refine_1 : f = pure a
refine_1₁ : g = pure b
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
refine ⟨a, b, ?_, ?_, h⟩
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
refine_1 : f ≤ pure a
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : {a} ∈ f
⊢ f = pure a

Tactic:
rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]

Premises used: Filter.le_pure_iff, Filter.NeBot.le_pure_iff, Filter.NeBot.of_mul_left
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
refine_1 : g ≤ pure b
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : {b} ∈ g
⊢ g = pure b

Tactic:
rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]

Premises used: Filter.NeBot.of_mul_right, Filter.le_pure_iff, Filter.NeBot.le_pure_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
a b : α
h : a * b = 1
refine_2 : Eq (α := Filter α) (pure (a * b)) 1
refine_2₁ : Eq.{u_2 + 1} (α := Filter α) (pure 1) 1
refine_2₂ refine_2₃ : Eq.{u_2 + 1} (α := Filter α) 1 1
⊢ HMul.hMul (α := Filter α) (pure a) (pure b) = 1

Tactic:
rw [pure_mul_pure, h, pure_one]

Premises used: Filter.pure_mul_pure, Filter.pure_one
-- 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 : DivisionMonoid α
f g s t : Filter α
h : s * t = 1
obtain :
  ∀ (a b : α) (hab : a * b = 1) (h : HMul.hMul (α := Filter α) (pure a) (pure b) = 1),
    Eq (α := Filter α) (pure a)⁻¹ (pure b)
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h

Premises used: Iff.mp, Filter.mul_eq_one_iff, 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 : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : HMul.hMul (α := Filter α) (pure a) (pure b) = 1
rw : Eq (α := Filter α) (pure a⁻¹) (pure b)
rw₁ rw₂ : Eq (α := Filter α) (pure b) (pure b)
⊢ Eq (α := Filter α) (pure a)⁻¹ (pure b)

Tactic:
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]

Premises used: inv_eq_of_mul_eq_one_right, Filter.inv_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
f : Filter α
mp : IsUnit f → ∃ (a : α), f = pure a ∧ IsUnit a
mpr : (∃ (a : α), f = pure a ∧ IsUnit a) → IsUnit f
⊢ IsUnit f ↔ ∃ (a : α), f = pure a ∧ IsUnit a

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
mp :
  ∀ (a b : α) (ha : (↑u : Filter α) = pure a) (hb : (↑u⁻¹ : Filter α) = pure b) (h : a * b = 1),
    ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a
⊢ ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv

Premises used: Units.mul_inv, Iff.mp, Filter.mul_eq_one_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
⊢ ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a

Tactic:
⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩

Premises used: Filter.pure_injective, And.intro, Units.mk, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
mp : Eq (α := Filter α) (pure (b * a)) (pure 1)
⊢ ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
mp : (↑u⁻¹ : Filter α) * (↑u : Filter α) = pure 1
⊢ Eq (α := Filter α) (pure (b * a)) (pure 1)

Tactic:
rw [← pure_mul_pure, ← ha, ← hb]

Premises used: Filter.pure_mul_pure
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
⊢ (↑u⁻¹ : Filter α) * (↑u : Filter α) = pure 1

Tactic:
u.inv_mul

Premises used: Units.inv_mul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
⊢ (↑u⁻¹ : Filter α) * (↑u : Filter α) = pure 1

Tactic:
exact u.inv_mul

Premises used: Units.inv_mul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (M := Filter α) (pure a)

Tactic:
ha.filter

Premises used: IsUnit.filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (M := Filter α) (pure a)

Tactic:
exact ha.filter

Premises used: IsUnit.filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Distrib α
f g h : Filter α
⊢ f * (g + h) ≤ f * g + f * h

Tactic:
map₂_distrib_le_left mul_add

Premises used: Set.Mem, Filter.map₂_distrib_le_left, setOf, mul_add
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Distrib α
f g h : Filter α
⊢ (f + g) * h ≤ f * h + g * h

Tactic:
map₂_distrib_le_right add_mul

Premises used: add_mul, Set.Mem, Filter.map₂_distrib_le_right, setOf
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : MulZeroClass α
f : Filter α
hf : f.NeBot
⊢ 0 ≤ f * 0

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

Premises used: Iff.mpr, _private.0.Filter.NeBot.mul_zero_nonneg.match_1, HMul.hMul, Membership.mem, Filter.le_mul_iff, MulZeroClass.mul_zero, And.intro, Exists.intro, Filter.NeBot.nonempty_of_mem, OfNat.ofNat
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : MulZeroClass α
g : Filter α
hg : g.NeBot
⊢ 0 ≤ 0 * g

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

Premises used: Iff.mpr, _private.0.Filter.NeBot.mul_zero_nonneg.match_1, HMul.hMul, MulZeroClass.zero_mul, Membership.mem, Filter.le_mul_iff, And.intro, Exists.intro, Filter.NeBot.nonempty_of_mem, OfNat.ofNat
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
⊢ 1 ≤ f / g ↔ ¬Disjoint f g

Tactic:
⟨fun h hfg => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
refine_1 : ∀ (h : 1 ≤ f / g) (hfg : Disjoint f g), False
refine_2 : ¬Disjoint f g → 1 ≤ f / g
⊢ 1 ≤ f / g ↔ ¬Disjoint f g

Tactic:
refine ⟨fun h hfg => ?_, ?_⟩
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
refine_1 : ∀ (s : Set α) (hs : s ∈ f) (t : Set α) (ht : t ∈ g) (hst : ∅ = s ∩ t), False
⊢ False

Tactic:
obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)

Premises used: Disjoint.le_bot, Filter.mem_bot
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False

Tactic:
Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)

Premises used: Iff.mpr, Filter.div_mem_div, disjoint_iff, Iff.mp, Set.one_mem_div_iff, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False

Tactic:
exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)

Premises used: Iff.mpr, Filter.div_mem_div, disjoint_iff, Iff.mp, Set.one_mem_div_iff, Eq.symm
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
h : ¬Disjoint f g
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ Membership.mem (γ := Filter α) 1 s

Tactic:
hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)

Premises used: Iff.mpr, Set.Mem, setOf, Filter.disjoint_of_disjoint_of_mem, Set.one_mem_div_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
h : ¬Disjoint f g
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ Membership.mem (γ := Filter α) 1 s

Tactic:
exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)

Premises used: Iff.mpr, Filter.disjoint_of_disjoint_of_mem, Set.one_mem_div_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f g : Filter α
⊢ ¬1 ≤ f / g ↔ Disjoint f g

Tactic:
Filter.one_le_div_iff.not_left

Premises used: Iff.not_left, Filter.one_le_div_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f : Filter α
h : f.NeBot
⊢ 1 ≤ f / f

Tactic:
simpa using neBot_iff.mp h

Premises used: Filter.neBot_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
a : α
⊢ IsUnit (M := Filter α) (pure a)

Tactic:
(Group.isUnit a).filter

Premises used: Group.isUnit, IsUnit.filter
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : Group α
f : Filter α
⊢ IsUnit f ↔ ∃ (a : α), f = pure a

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

Premises used: and_true, Group.isUnit, Filter.isUnit_iff
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
f : Filter α
⊢ Eq.{u_3 + 1} (α := Filter β) (map (⇑m : (a : α) → β) f⁻¹) (map (⇑m : (a : α) → β) f)⁻¹

Tactic:
Semiconj.filter_map (map_inv m) f

Premises used: map_inv, Function.Semiconj.filter_map
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
f₁ : Filter α
f₂ : Filter β
⊢ Tendsto (⇑m : (a : α) → β) f₁ f₂ → Tendsto (⇑m : (a : α) → β) f₁⁻¹ f₂⁻¹

Tactic:
fun hf =>
  (Filter.map_inv' m).trans_le <| Filter.inv_le_inv hf

Premises used: Filter.map_inv', Filter.inv_le_inv, Eq.trans_le, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
f g : Filter α
⊢ map (⇑m : (a : α) → β) (f / g) = HDiv.hDiv (α := Filter β) (map (⇑m : (a : α) → β) f) (map (⇑m : (a : α) → β) g)

Tactic:
map_map₂_distrib <| map_div m

Premises used: setOf, Filter.map_map₂_distrib, Filter.map₂, Filter.copy, map_div
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
m : F
f₁ g₁ : Filter α
f₂ g₂ : Filter β
hf : Tendsto (⇑m : (a : α) → β) f₁ f₂
hg : Tendsto (⇑m : (a : α) → β) g₁ g₂
⊢ Tendsto (⇑m : (a : α) → β) (f₁ / g₁) (f₂ / g₂)

Tactic:
(Filter.map_div m).trans_le <| Filter.div_le_div hf hg

Premises used: Filter.div_le_div, Eq.trans_le, Filter.Tendsto, Filter.map_div
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : GroupWithZero α
f : Filter α
hf : f.NeBot
⊢ 0 ≤ f / 0

Tactic:
Filter.le_div_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, div_zero _⟩

Premises used: Iff.mpr, _private.0.Filter.NeBot.mul_zero_nonneg.match_1, Membership.mem, HDiv.hDiv, Filter.le_div_iff, And.intro, Exists.intro, Filter.NeBot.nonempty_of_mem, OfNat.ofNat, div_zero
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
inst : GroupWithZero α
g : Filter α
hg : g.NeBot
⊢ 0 ≤ 0 / g

Tactic:
Filter.le_div_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_div _⟩

Premises used: Iff.mpr, _private.0.Filter.NeBot.mul_zero_nonneg.match_1, zero_div, Membership.mem, HDiv.hDiv, Filter.le_div_iff, And.intro, Exists.intro, Filter.NeBot.nonempty_of_mem, OfNat.ofNat
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter α
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, Filter.HasBasis.map₂, HSMul.hSMul, Filter.map₂, Filter.copy
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter α
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 : SMul α β
f : Filter α
g : Filter β
t : Set β
⊢ t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f : Filter α
g : Filter β
s : Set α
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 : SMul α β
g : Filter β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := 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 : SMul α β
f : Filter α
⊢ HSMul.hSMul (β := 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 : SMul α β
f : Filter α
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 : SMul α β
f : Filter α
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 : SMul α β
f : Filter α
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 : SMul α β
f : Filter α
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 : SMul α β
f : Filter α
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 : SMul α β
f : Filter α
g : Filter β
inst_1 : f.NeBot
inst_2 : g.NeBot
⊢ (f • g).NeBot

Tactic:
.smul ‹_› ‹_›

Premises used: Filter.NeBot.smul
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
g : Filter β
a : α
⊢ HSMul.hSMul (α := Filter α) (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 : SMul α β
f : Filter α
b : β
⊢ HSMul.hSMul (β := Filter β) 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 : SMul α β
a : α
b : β
⊢ HSMul.hSMul (α := Filter α) (β := Filter β) (pure a) (pure b) = pure (a • b)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Pointwise
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
f₁ f₂ : Filter α
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 : SMul α β
f : Filter α
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 : SMul α β
f₁ f₂ : Filter α
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 : SMul α β
f : Filter α
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 : SMul α β
f f₁ f₂ : Filter α
g g₁ g₂ h : Filter β
s : Set α
t : Set β
a : α
b : β
⊢ CovariantClass.{u_2, u_3} (Filter α) (Filter β) (fun (x1 : Filter α) (x2 : Filter β) ↦ x1 • x2)
    fun (x1 x2 : Filter β) ↦ x1 ≤ x2

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

Premises used: CovariantClass.mk, Filter.map₂_mono_left