awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : Top β
⊢ Eq (α := l.Germ β) (↑⊤ : l.Germ β) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : Max β
a b : β
⊢ Eq (α := l.Germ β) (↑(a ⊔ b) : l.Germ β) ((↑a : l.Germ β) ⊔ (↑b : l.Germ β))

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : Min β
a b : β
⊢ Eq (α := l.Germ β) (↑(a ⊓ b) : l.Germ β) ((↑a : l.Germ β) ⊓ (↑b : l.Germ β))

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
choose :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
    ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c

Tactic:
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx

Premises used: ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c

Tactic:
⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩

Premises used: Iff.mpr, Filter.Germ.ofFun, Filter.Germ.coe_eq, LE.le, dite, Exists.intro
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
refine :
  g =ᶠ[l]
    (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
      if hx : f x ≤ g x then c x hx else f x
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c

Tactic:
refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
h₁ : ∀ (x : α) (hx : f x ≤ g x), g x = f x * if hx : f x ≤ g x then c x hx else f x
⊢ g =ᶠ[l]
    (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
      if hx : f x ≤ g x then c x hx else f x

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x_1 y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
h₁ : g x = f x * c x hx
h₂ : f x * c x hx = f x * c x hx
h₃ : f x ≤ g x
h₄ : f x * c x hx = f x * c x hx
h₅ : f x ≤ g x
⊢ g x = f x * if hx : f x ≤ g x then c x hx else f x

Tactic:
rw [dif_pos hx, hc]

Premises used: dif_pos
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
choose :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
    ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
choose₁ :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
    g =ᶠ[l]
      (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
        if hx : f x ≤ g x then c x hx else f x
h₁ :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx) (x : α) (hx : f x ≤ g x),
    g x = f x * if hx : f x ≤ g x then c x hx else f x
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c

Tactic:
classical
    choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
    refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
    filter_upwards [h] with x hx
    rw [dif_pos hx, hc]

Premises used: ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Order.Filter.Germ.OrderedMonoid
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CommMonoid β
inst_1 : Preorder β
inst_2 : IsOrderedMonoid β
f g : l.Germ β
x x_1 : α → β
H_1 : LE.le (α := l.Germ β) (↑x : l.Germ β) (↑x_1 : l.Germ β)
h : l.Germ β
x_2 : α → β
x_3 : α
H : x x_3 ≤ x_1 x_3
dsimp : x x_3 * x_2 x_3 ≤ x_1 x_3 * x_2 x_3
⊢ LE.le.{u_2} (α := β) ((fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) x x_2 x_3)
    ((fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) x_1 x_2 x_3)

Tactic:
dsimp
-- Module: Mathlib.Order.Filter.Germ.OrderedMonoid
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CommMonoid β
inst_1 : Preorder β
inst_2 : IsOrderedMonoid β
f g : l.Germ β
x x_1 : α → β
H_1 : LE.le (α := l.Germ β) (↑x : l.Germ β) (↑x_1 : l.Germ β)
h : l.Germ β
x_2 : α → β
x_3 : α
H : x x_3 ≤ x_1 x_3
⊢ x x_3 * x_2 x_3 ≤ x_1 x_3 * x_2 x_3

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∈ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
simp only [*, hst.1 hxs, mulIndicator_of_mem]

Premises used: Iff.mp, Set.mulIndicator_of_mem
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
simp only [mulIndicator_of_notMem, hxs, mt hst.2 hxs, not_false_eq_true]

Premises used: Iff.mpr, Set.mulIndicator_of_notMem, mt, not_false_eq_true
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
M : Type u_3
inst : Monoid M
s t : Set α
f : α → M
l : Filter α
h : ∀ᶠ (a : α) in l, a ∉ s ∩ t
⊢ (s ∪ t).mulIndicator f =ᶠ[l] s.mulIndicator f * t.mulIndicator f

Tactic:
h.mono fun _a ha => mulIndicator_union_of_notMem_inter ha _

Premises used: Filter.EventuallyEq, Set.mulIndicator_union_of_notMem_inter, Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
inst_1 : Preorder β
s : Set α
f g : α → β
l : Filter α
h : f ≤ᶠ[l ⊓ 𝓟 s] g
⊢ s.mulIndicator f ≤ᶠ[l] s.mulIndicator g

Tactic:
(eventually_inf_principal.1 h).mono fun _ => mulIndicator_rel_mulIndicator le_rfl

Premises used: Filter.eventually_inf_principal, le_rfl, Set.mulIndicator_rel_mulIndicator, Filter.Eventually.mono, Iff.mp, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (i : ι) ↦ (s i).mulIndicator f a) fun (x : ι) ↦
    mulIndicator (⋃ (i : ι), s i) f a

Tactic:
hs.piecewise_eventually_eq_iUnion f 1 a

Premises used: Set.mulIndicator, Filter.EventuallyEq, Monotone.piecewise_eventually_eq_iUnion, OfNat.ofNat
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (i : ι) ↦ (s i).mulIndicator f a) fun (x : ι) ↦
    mulIndicator (⋃ (i : ι), s i) f a

Tactic:
exact hs.piecewise_eventually_eq_iUnion f 1 a

Premises used: Monotone.piecewise_eventually_eq_iUnion, OfNat.ofNat
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (i : ι) ↦ (s i).mulIndicator f a) fun (x : ι) ↦
    mulIndicator (⋃ (i : ι), s i) f a

Tactic:
classical exact hs.piecewise_eventually_eq_iUnion f 1 a
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ Tendsto (fun (i : ι) ↦ (s i).mulIndicator f a) atTop (pure (mulIndicator (⋃ (i : ι), s i) f a))

Tactic:
tendsto_pure.2 <| hs.mulIndicator_eventuallyEq_iUnion s f a

Premises used: Iff.mpr, Filter.tendsto_pure, Monotone.mulIndicator_eventuallyEq_iUnion
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (i : ι) ↦ (s i).mulIndicator f a) fun (x : ι) ↦
    mulIndicator (⋂ (i : ι), s i) f a

Tactic:
hs.piecewise_eventually_eq_iInter f 1 a

Premises used: Set.mulIndicator, Antitone.piecewise_eventually_eq_iInter, Filter.EventuallyEq, OfNat.ofNat
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (i : ι) ↦ (s i).mulIndicator f a) fun (x : ι) ↦
    mulIndicator (⋂ (i : ι), s i) f a

Tactic:
exact hs.piecewise_eventually_eq_iInter f 1 a

Premises used: Antitone.piecewise_eventually_eq_iInter, OfNat.ofNat
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (i : ι) ↦ (s i).mulIndicator f a) fun (x : ι) ↦
    mulIndicator (⋂ (i : ι), s i) f a

Tactic:
classical exact hs.piecewise_eventually_eq_iInter f 1 a
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : Preorder ι
inst_1 : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ Tendsto (fun (i : ι) ↦ (s i).mulIndicator f a) atTop (pure (mulIndicator (⋂ (i : ι), s i) f a))

Tactic:
tendsto_pure.2 <| hs.mulIndicator_eventuallyEq_iInter s f a

Premises used: Iff.mpr, Filter.tendsto_pure, Antitone.mulIndicator_eventuallyEq_iInter
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
rw :
  EventuallyEq.{u_5, u_2} (β := β) atTop (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) fun (x : Finset ι) ↦
    mulIndicator (⋃ (t : Finset ι), ⋃ i ∈ t, s i) f a
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) fun (x : Finset ι) ↦
    (iUnion s).mulIndicator f a

Tactic:
rw [iUnion_eq_iUnion_finset s]

Premises used: Set.iUnion_eq_iUnion_finset
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
hs : Monotone.{u_5, u_1} (β := Set α) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, s i_1
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) fun (x : Finset ι) ↦
    mulIndicator (⋃ (t : Finset ι), ⋃ i ∈ t, s i) f a

Tactic:
apply Monotone.mulIndicator_eventuallyEq_iUnion

Premises used: Monotone.mulIndicator_eventuallyEq_iUnion
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
⊢ Monotone.{u_5, u_1} (β := Set α) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, s i_1

Tactic:
fun _ _ ↦ biUnion_subset_biUnion_left

Premises used: Monotone, Set.Subset, Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
⊢ Monotone.{u_5, u_1} (β := Set α) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, s i_1

Tactic:
exact fun _ _ ↦ biUnion_subset_biUnion_left

Premises used: Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
⊢ Tendsto (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) atTop (pure ((iUnion s).mulIndicator f a))

Tactic:
tendsto_pure.2 <| mulIndicator_biUnion_finset_eventuallyEq s f a

Premises used: Iff.mpr, Filter.tendsto_pure, mulIndicator_biUnion_finset_eventuallyEq
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ Function.mulSupport f =ᶠ[l] Function.mulSupport g

Tactic:
h.preimage ({1}ᶜ : Set β)

Premises used: Set.Mem, Compl.compl, setOf, Filter.EventuallyEq.preimage, Set.preimage, Set.singleton, Function.mulSupport, Singleton.singleton, OfNat.ofNat, Not
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f g : α → β
s : Set α
hfg : f =ᶠ[l] g
⊢ s.mulIndicator f =ᶠ[l] s.mulIndicator g

Tactic:
mulIndicator_eventuallyEq (hfg.filter_mono inf_le_left) EventuallyEq.rfl

Premises used: Filter.EventuallyEq.filter_mono, inf_le_left, Filter.EventuallyEq.rfl, mulIndicator_eventuallyEq
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
rw rw₁ : EventuallyEq.{u_1, u_2} (β := β) l 1 1
⊢ EventuallyEq.{u_1, u_2} (β := β) l (s.mulIndicator 1) 1

Tactic:
rw [mulIndicator_one']

Premises used: Set.mulIndicator_one'
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s_1 t : Set α
h : s_1.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
rw : s ∩ Function.mulSupport f =ᶠ[l] s
⊢ Function.mulSupport (s.mulIndicator f) =ᶠ[l] s

Tactic:
rw [mulSupport_mulIndicator]

Premises used: Set.mulSupport_mulIndicator
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s_1 t : Set α
h : s_1.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ s ∩ Function.mulSupport f =ᶠ[l] s

Tactic:
(hf.mono fun x hx ↦ and_iff_left hx).set_eq

Premises used: Set.Mem, Filter.Eventually.set_eq, setOf, and_iff_left, Set.inter, Filter.Eventually.mono, Function.mulSupport, Not
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s_1 t : Set α
h : s_1.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ s ∩ Function.mulSupport f =ᶠ[l] s

Tactic:
exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq

Premises used: Filter.Eventually.set_eq, and_iff_left, Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
⊢ ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s

Tactic:
have : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s := fun {s} ↦ by
    rw [mulSupport_mulIndicator]
    exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
⊢ s =ᶠ[l] t

Tactic:
this.symm.trans <| h.mulSupport.trans this

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.mulSupport, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
⊢ s =ᶠ[l] t

Tactic:
exact this.symm.trans <| h.mulSupport.trans this

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.mulSupport, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
c : β
hc : c ≠ 1
s t : Set α
h : EventuallyEq.{u_1, u_2} (β := β) l (s.mulIndicator fun (x : α) ↦ c) (t.mulIndicator fun (x : α) ↦ c)
⊢ s =ᶠ[l] t

Tactic:
.of_mulIndicator (Eventually.of_forall fun _ ↦ hc) h

Premises used: Filter.Eventually.of_forall, Filter.EventuallyEq.of_mulIndicator
-- Module: Mathlib.Order.Filter.IndicatorFunction
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
c : β
hc : c ≠ 1
s t : Set α
⊢ EventuallyEq.{u_1, u_2} (β := β) l (s.mulIndicator fun (x : α) ↦ c) (t.mulIndicator fun (x : α) ↦ c) ↔ s =ᶠ[l] t

Tactic:
⟨.of_mulIndicator_const hc, mulIndicator_eventuallyEq .rfl⟩

Premises used: Filter.EventuallyEq.of_mulIndicator_const, Iff.intro, Filter.EventuallyEq.rfl, mulIndicator_eventuallyEq
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
s t : Set α
Ixx : α → α → Set α
⊢ Tendsto (fun (p : α × α) ↦ Ixx p.1 p.2) (𝓟 s ×ˢ 𝓟 s) (𝓟 t).smallSets ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t

Tactic:
simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal,
      forall_prod_set, mem_powerset_iff]

Premises used: Set.mem_powerset_iff, Set.forall_prod_set, Filter.prod_principal_principal, Filter.smallSets_principal, Filter.tendsto_principal_principal
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun (p : α × α) ↦ Ixx p.1 p.2) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (l₂ ⊓ l₂').smallSets

Tactic:
simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1

Premises used: Filter.TendstoIxxClass.tendsto_Ixx, Filter.prod_inf_prod, Filter.smallSets_inf, Filter.Tendsto.inf
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
l₁ l₂ : Filter α
Ixx Ixx' : α → α → Set α
h : ∀ (a b : α), Ixx a b ⊆ Ixx' a b
h' : TendstoIxxClass Ixx' l₁ l₂
⊢ TendstoIxxClass Ixx l₁ l₂

Tactic:
⟨h'.1.smallSets_mono <| Eventually.of_forall <| Prod.forall.2 h⟩

Premises used: Iff.mpr, Filter.TendstoIxxClass.tendsto_Ixx, Filter.Eventually.of_forall, Filter.TendstoIxxClass.mk, Filter.Tendsto.smallSets_mono, Prod.forall
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
ι : Type u_3
p : ι → Prop
s : ι → Set α
l : Filter α
hl : l.HasBasis p s
Ixx : α → α → Set α
H : ∀ (i : ι), p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i
⊢ TendstoIxxClass Ixx l l

Tactic:
⟨(hl.prod_self.tendsto_iff hl.smallSets).2 fun i hi => ⟨i, hi, fun _ h => H i hi _ h.1 _ h.2⟩⟩

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, Filter.TendstoIxxClass.mk, Prod.fst, And.right, And.left, And.intro, Filter.HasBasis.smallSets, Exists.intro, Prod.snd
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
l₁ l₂ : Filter α
inst_1 : TendstoIxxClass Icc l₁ l₂
lb : Filter β
u₁ u₂ : β → α
h₁ : Tendsto u₁ lb l₁
h₂ : Tendsto u₂ lb l₁
⊢ Tendsto (fun (x : β) ↦ Icc (u₁ x) (u₂ x)) lb l₂.smallSets

Tactic:
(@TendstoIxxClass.tendsto_Ixx α Set.Icc _ _ _).comp <| h₁.prodMk h₂

Premises used: Filter.TendstoIxxClass.tendsto_Ixx, setOf, Set.Icc, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
l₁ l₂ : Filter α
inst_1 : TendstoIxxClass Ioc l₁ l₂
lb : Filter β
u₁ u₂ : β → α
h₁ : Tendsto u₁ lb l₁
h₂ : Tendsto u₂ lb l₁
⊢ Tendsto (fun (x : β) ↦ Ioc (u₁ x) (u₂ x)) lb l₂.smallSets

Tactic:
(@TendstoIxxClass.tendsto_Ixx α Set.Ioc _ _ _).comp <| h₁.prodMk h₂

Premises used: Set.Ioc, Filter.TendstoIxxClass.tendsto_Ixx, setOf, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
l₁ l₂ : Filter α
inst_1 : TendstoIxxClass Ico l₁ l₂
lb : Filter β
u₁ u₂ : β → α
h₁ : Tendsto u₁ lb l₁
h₂ : Tendsto u₂ lb l₁
⊢ Tendsto (fun (x : β) ↦ Ico (u₁ x) (u₂ x)) lb l₂.smallSets

Tactic:
(@TendstoIxxClass.tendsto_Ixx α Set.Ico _ _ _).comp <| h₁.prodMk h₂

Premises used: Filter.TendstoIxxClass.tendsto_Ixx, setOf, Set.Ico, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
l₁ l₂ : Filter α
inst_1 : TendstoIxxClass Ioo l₁ l₂
lb : Filter β
u₁ u₂ : β → α
h₁ : Tendsto u₁ lb l₁
h₂ : Tendsto u₂ lb l₁
⊢ Tendsto (fun (x : β) ↦ Ioo (u₁ x) (u₂ x)) lb l₂.smallSets

Tactic:
(@TendstoIxxClass.tendsto_Ixx α Set.Ioo _ _ _).comp <| h₁.prodMk h₂

Premises used: Filter.TendstoIxxClass.tendsto_Ixx, setOf, Filter.Tendsto.prodMk, Filter.Tendsto.comp, Set.Ioo
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Icc atTop atTop

Tactic:
(hasBasis_iInf_principal_finite _).tendstoIxxClass fun _ _ =>
    Set.OrdConnected.out <| ordConnected_biInter fun _ _ => ordConnected_Ici

Premises used: Set.ordConnected_Ici, Filter.HasBasis.tendstoIxxClass, Set.OrdConnected.out, Filter.hasBasis_iInf_principal_finite, Filter.atTop, Set.ordConnected_biInter
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Ico atTop atTop

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Ioc atTop atTop

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Ioo atTop atTop

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Icc atBot atBot

Tactic:
(hasBasis_iInf_principal_finite _).tendstoIxxClass fun _ _ =>
    Set.OrdConnected.out <| ordConnected_biInter fun _ _ => ordConnected_Iic

Premises used: Set.ordConnected_Iic, Filter.HasBasis.tendstoIxxClass, Set.OrdConnected.out, Filter.hasBasis_iInf_principal_finite, Set.ordConnected_biInter, Filter.atBot
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Ico atBot atBot

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Ioc atBot atBot

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ TendstoIxxClass.{u_1} (α := α) Ioo atBot atBot

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : Set α
hs : s.OrdConnected
⊢ TendstoIxxClass Icc (𝓟 s) (𝓟 s)

Tactic:
tendstoIxxClass_principal.2 hs.out

Premises used: Iff.mpr, Set.OrdConnected.out, Filter.tendstoIxxClass_principal
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ico (𝓟 (Ici a)) (𝓟 (Ici a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, Filter.tendstoIxxClass_of_subset