awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x : Filter α
y : Filter β
z : Filter γ
hg : Tendsto g y z
hf : Tendsto f x y
⊢ Tendsto (g ∘ f) x z

Tactic:
fun _ hs => hf (hg hs)

Premises used: Set.Mem, setOf, Set.preimage, Filter.Tendsto, Set
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x y : Filter α
z : Filter β
hx : Tendsto f x z
h : y ≤ x
⊢ Tendsto f y z

Tactic:
(map_mono h).trans hx

Premises used: Filter.map_mono, Filter.Tendsto, LE.le.trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Filter α
y z : Filter β
hy : Tendsto f x y
hz : y ≤ z
⊢ Tendsto f x z

Tactic:
le_trans hy hz

Premises used: Filter.Tendsto, le_trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Filter α
y : Filter β
h : Tendsto f x y
hx : x.NeBot
⊢ y.NeBot

Tactic:
(hx.map _).mono h

Premises used: Filter.NeBot.mono, Filter.NeBot.map
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Filter α
⊢ Tendsto f x (map f x)

Tactic:
le_refl (map f x)

Premises used: le_refl, Filter.map, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
rw : map f (map g x) ≤ y ↔ Tendsto (f ∘ g) x y
rw₁ : map f (map g x) ≤ y ↔ map (f ∘ g) x ≤ y
rw₂ rw₃ : map (f ∘ g) x ≤ y ↔ map (f ∘ g) x ≤ y
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

Tactic:
rw [Tendsto, Tendsto, map_map]

Premises used: Filter.map_map, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Filter β
⊢ Tendsto f (comap f x) x

Tactic:
map_comap_le

Premises used: Filter.Tendsto, Filter.map_comap_le
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
c : Filter γ
h : Tendsto (g ∘ f) a c
rwa rwa₁ rwa₂ rwa₃ : map (g ∘ f) a ≤ c
⊢ map g (map f a) ≤ c

Tactic:
rwa [map_map]

Premises used: Filter.map_map
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
rw : (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g
⊢ Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g

Tactic:
rw [Tendsto, ← map_compose]

Premises used: Filter.Tendsto, Filter.map_compose
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g

Tactic:
simp only [(· ∘ ·), map_comap_of_mem h, Tendsto]

Premises used: Function.comp, Filter.map_comap_of_mem, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
rw : ∀ (hfg : a ≤ comap (g ∘ f) c) (hg : comap g c ≤ b), a ≤ comap f b
⊢ Tendsto f a b

Tactic:
rw [tendsto_iff_comap] at hfg ⊢

Premises used: Filter.tendsto_iff_comap
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap (g ∘ f) c

Tactic:
hfg
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ comap (g ∘ f) c ≤ comap f b

Tactic:
simpa [comap_comap] using comap_mono hg

Premises used: Filter.comap_mono, Filter.comap_comap
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
a₁ : comap (g ∘ f) c ≤ comap f b
⊢ a ≤ comap f b

Tactic:
calc
    a ≤ comap (g ∘ f) c := hfg
    _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg

Premises used: Function.comp, Filter.comap
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ g = f

Tactic:
((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)

Premises used: LE.le.antisymm, Filter.comap_mono, Iff.mp, Filter.map_le_iff_le_comap, LE.le.trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
refine : comap φ (comap ψ f) ≤ f
⊢ comap φ g = f

Tactic:
refine ((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)

Premises used: LE.le.antisymm, Filter.comap_mono, Iff.mp, Filter.map_le_iff_le_comap, LE.le.trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
rw : comap (ψ ∘ φ) f ≤ f
rw₁ : comap id f ≤ f
rw₂ rw₃ : f ≤ f
⊢ comap φ (comap ψ f) ≤ f

Tactic:
rw [comap_comap, eq, comap_id]

Premises used: Filter.comap_comap, Filter.comap_id
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ map φ f = g

Tactic:
le_antisymm hφ (le_trans ?_ (map_mono hψ))

Premises used: Filter.map_mono, le_antisymm, le_trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
refine : g ≤ map φ (map ψ g)
⊢ map φ f = g

Tactic:
refine le_antisymm hφ (le_trans ?_ (map_mono hψ))

Premises used: Filter.map_mono, le_antisymm, le_trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
rw : g ≤ map (φ ∘ ψ) g
rw₁ : g ≤ map id g
rw₂ rw₃ : g ≤ g
⊢ g ≤ map φ (map ψ g)

Tactic:
rw [map_map, eq, map_id]

Premises used: Filter.map_map, Filter.map_id
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Filter α
y₁ y₂ : Filter β
⊢ Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

Tactic:
simp only [Tendsto, le_inf_iff]

Premises used: le_inf_iff, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
h : Tendsto f x₁ y
⊢ Tendsto f (x₁ ⊓ x₂) y

Tactic:
le_trans (map_mono inf_le_left) h

Premises used: Filter.map_mono, Filter.Tendsto, inf_le_left, le_trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
h : Tendsto f x₂ y
⊢ Tendsto f (x₁ ⊓ x₂) y

Tactic:
le_trans (map_mono inf_le_right) h

Premises used: Filter.map_mono, inf_le_right, Filter.Tendsto, le_trans
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y₁ y₂ : Filter β
h₁ : Tendsto f x₁ y₁
h₂ : Tendsto f x₂ y₂
⊢ Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)

Tactic:
tendsto_inf.2 ⟨tendsto_inf_left h₁, tendsto_inf_right h₂⟩

Premises used: Iff.mpr, Filter.tendsto_inf, Filter.tendsto_inf_left, And.intro, Filter.tendsto_inf_right
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : Filter α
y : ι → Filter β
⊢ Tendsto f x (⨅ (i : ι), y i) ↔ ∀ (i : ι), Tendsto f x (y i)

Tactic:
simp only [Tendsto, le_iInf_iff]

Premises used: le_iInf_iff, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : ι → Filter α
y : Filter β
i : ι
hi : Tendsto f (x i) y
⊢ Tendsto f (⨅ (i : ι), x i) y

Tactic:
hi.mono_left <| iInf_le _ _

Premises used: Filter.Tendsto.mono_left, iInf_le
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : ι → Filter α
y : ι → Filter β
h : ∀ (i : ι), Tendsto f (x i) (y i)
⊢ Tendsto f (iInf x) (iInf y)

Tactic:
tendsto_iInf.2 fun i => tendsto_iInf' i (h i)

Premises used: Iff.mpr, Filter.tendsto_iInf', Filter.tendsto_iInf
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
⊢ Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

Tactic:
simp only [Tendsto, map_sup, sup_le_iff]

Premises used: Filter.map_sup, sup_le_iff, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
⊢ Tendsto f x₁ y → Tendsto f x₂ y → Tendsto f (x₁ ⊔ x₂) y

Tactic:
fun h₁ h₂ => tendsto_sup.mpr ⟨h₁, h₂⟩

Premises used: Iff.mpr, Filter.tendsto_sup, And.intro
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y₁ y₂ : Filter β
h₁ : Tendsto f x₁ y₁
h₂ : Tendsto f x₂ y₂
⊢ Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂)

Tactic:
tendsto_sup.mpr ⟨h₁.mono_right le_sup_left, h₂.mono_right le_sup_right⟩

Premises used: Iff.mpr, le_sup_left, le_sup_right, Filter.tendsto_sup, And.intro, Filter.Tendsto.mono_right
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : ι → Filter α
y : Filter β
⊢ Tendsto f (⨆ (i : ι), x i) y ↔ ∀ (i : ι), Tendsto f (x i) y

Tactic:
simp only [Tendsto, map_iSup, iSup_le_iff]

Premises used: Filter.map_iSup, Filter.Tendsto, iSup_le_iff
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : ι → Filter α
y : ι → Filter β
h : ∀ (i : ι), Tendsto f (x i) (y i)
⊢ Tendsto f (iSup x) (iSup y)

Tactic:
tendsto_iSup.2 fun i => (h i).mono_right <| le_iSup _ _

Premises used: Iff.mpr, le_iSup, Filter.tendsto_iSup, Filter.Tendsto.mono_right
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
s : Set β
⊢ Tendsto f l (𝓟 s) ↔ ∀ᶠ (a : α) in l, f a ∈ s

Tactic:
simp only [Tendsto, le_principal_iff, mem_map', Filter.Eventually]

Premises used: Filter.le_principal_iff, Filter.Eventually, Filter.mem_map', Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t

Tactic:
simp
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : Filter α
b : β
⊢ Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b

Tactic:
simp only [Tendsto, le_pure_iff, mem_map', mem_singleton_iff, Filter.Eventually]

Premises used: Filter.le_pure_iff, Filter.Eventually, Set.mem_singleton_iff, Filter.mem_map', Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ Tendsto f (pure a) (pure (f a))

Tactic:
tendsto_pure.2 rfl

Premises used: Iff.mpr, Filter.tendsto_pure, rfl
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
a : Filter α
b : β
⊢ Tendsto (fun (x : α) ↦ b) a (pure b)

Tactic:
tendsto_pure.2 <| univ_mem' fun _ => rfl

Premises used: Iff.mpr, Filter.tendsto_pure, rfl, Filter.univ_mem'
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
a : α
l : Filter α
⊢ pure a ≤ l ↔ ∀ s ∈ l, a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
l : Filter β
⊢ Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
l : Filter α
t : Set β
⊢ t ∈ map f (l ⊓ 𝓟 (f ⁻¹' s)) ↔ t ∈ map f l ⊓ 𝓟 s

Tactic:
simp only [mem_map', mem_inf_principal, mem_setOf_eq, mem_preimage]

Premises used: Set.mem_setOf_eq, Filter.mem_map', Filter.mem_inf_principal, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : Filter α
b₁ b₂ : Filter β
hf : Tendsto f a b₁
inst : a.NeBot
hb : Disjoint b₁ b₂
⊢ ¬Tendsto f a b₂

Tactic:
fun hf' =>
  (tendsto_inf.2 ⟨hf, hf'⟩).neBot.ne hb.eq_bot

Premises used: Iff.mpr, Filter.tendsto_inf, Filter.NeBot.ne, And.intro, Filter.Tendsto.neBot, Not, Disjoint.eq_bot
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : Tendsto f (l₁ ⊓ 𝓟 {x : α | p x}) l₂
h₁ : Tendsto g (l₁ ⊓ 𝓟 {x : α | ¬p x}) l₂
simp :
  ∀ (h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁)
    (h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁),
    ∀ s ∈ l₂, (fun (x : α) ↦ if p x then f x else g x) ⁻¹' s ∈ l₁
⊢ Tendsto (fun (x : α) ↦ if p x then f x else g x) l₁ l₂

Tactic:
simp only [tendsto_def, mem_inf_principal] at *

Premises used: Filter.tendsto_def, Filter.mem_inf_principal
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
h :
  ∀ (x : α) (hp₀ : p x → x ∈ f ⁻¹' s) (hp₁ : ¬p x → x ∈ g ⁻¹' s),
    Membership.mem (γ := Set α) ((fun (x : α) ↦ if p x then f x else g x) ⁻¹' s) x
⊢ (fun (x : α) ↦ if p x then f x else g x) ⁻¹' s ∈ l₁

Tactic:
filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : (if p x then f x else g x) ∈ s
⊢ Membership.mem (γ := Set α) ((fun (x : α) ↦ if p x then f x else g x) ⁻¹' s) x

Tactic:
rw [mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
pos : ∀ (h : p x), f x ∈ s
neg : ∀ (h : ¬p x), g x ∈ s
⊢ (if p x then f x else g x) ∈ s

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : p x
⊢ f x ∈ s

Tactic:
hp₀ h

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : ¬p x
⊢ g x ∈ s

Tactic:
hp₁ h

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
h : p x
⊢ f x ∈ s

Tactic:
exacts [hp₀ h, hp₁ h]
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_5
β : Type u_6
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : DecidablePred p
hf : Tendsto f l₁ l₂
hg : Tendsto g l₁ l₂
⊢ Tendsto (fun (a : α) ↦ if p a then f a else g a) l₁ l₂

Tactic:
(tendsto_inf_left hf).if (tendsto_inf_left hg)

Premises used: Filter.tendsto_inf_left, Filter.Tendsto.if
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
s : Set α
inst : (x : α) → Decidable (x ∈ s)
h₀ : Tendsto f (l₁ ⊓ 𝓟 s) l₂
h₁ : Tendsto g (l₁ ⊓ 𝓟 sᶜ) l₂
⊢ Tendsto (s.piecewise (β := fun (a : α) ↦ β) f g) l₁ l₂

Tactic:
Tendsto.if h₀ h₁

Premises used: Filter.Tendsto.if, Set.piecewise
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Tendsto f (𝓟 s) (𝓟 t)

Tactic:
Filter.tendsto_principal_principal.2 h

Premises used: Iff.mpr, Filter.tendsto_principal_principal
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f f' : α → β
H : f =ᶠ[l] f'
g : γ → α
lc : Filter γ
hg : Tendsto g lc l
⊢ f ∘ g =ᶠ[lc] f' ∘ g

Tactic:
hg.eventually H

Premises used: Filter.EventuallyEq, Filter.Tendsto.eventually
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ MapsTo (map m) (Iic F) (Iic G) ↔ Tendsto m F G

Tactic:
⟨fun hm ↦ hm self_mem_Iic, fun hm _ ↦ hm.mono_left⟩

Premises used: Set.self_mem_Iic, Iff.intro, Filter.Tendsto.mono_left
-- Module: Mathlib.Order.Filter.Tendsto
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : Tendsto m (𝓟 s) (𝓟 t) ↔ MapsTo m s t
rw₁ : (∀ a ∈ s, m a ∈ t) ↔ MapsTo m s t
rw₂ rw₃ : (∀ a ∈ s, m a ∈ t) ↔ ∀ ⦃x : α⦄, x ∈ s → m x ∈ t
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t

Tactic:
rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]

Premises used: Filter.map_mapsTo_Iic_iff_tendsto, Set.MapsTo, Filter.tendsto_principal_principal
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ Membership.mem (γ := Filter β) cofinite (univ \ s)

Tactic:
simpa [compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ (f ⁻¹' s).Finite

Tactic:
simpa [compl_eq_univ_diff] using TendstoCofinite.tendsto_cofinite f
    (show univ \ s ∈ cofinite by simpa [compl_eq_univ_diff])

Premises used: Set.compl_eq_univ_diff, Filter.TendstoCofinite.tendsto_cofinite
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
b : β
⊢ Set.Finite (α := β) {b}

Tactic:
simp
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
b : β
⊢ (f ⁻¹' {b}).Finite

Tactic:
simpa using TendstoCofinite.finite_preimage f (by simp)

Premises used: Filter.TendstoCofinite.finite_preimage
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ TendstoCofinite f ↔ ∀ (b : β), (f ⁻¹' {b}).Finite

Tactic:
⟨fun _ ↦ TendstoCofinite.finite_preimage_singleton f,
  fun h ↦ ⟨Tendsto.cofinite_of_finite_preimage_singleton h⟩⟩

Premises used: Filter.Tendsto.cofinite_of_finite_preimage_singleton, Filter.TendstoCofinite.finite_preimage_singleton, Iff.intro, Filter.TendstoCofinite.mk
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
h : Function.Injective f
⊢ TendstoCofinite f

Tactic:
⟨h.tendsto_cofinite⟩

Premises used: Function.Injective.tendsto_cofinite, Filter.TendstoCofinite.mk
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Finite α
⊢ TendstoCofinite f

Tactic:
(tendstoCofinite_iff_finite_preimage_singleton f).mpr fun b ↦ Set.toFinite (f ⁻¹' {b})

Premises used: Iff.mpr, Filter.tendstoCofinite_iff_finite_preimage_singleton, Set.toFinite, Set.preimage, Singleton.singleton
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
f : α → β
g : β → ι
inst : TendstoCofinite g
inst_1 : TendstoCofinite f
r : ι
⊢ Set.Finite.{u_3} (α := ι) {b : ι | b = r}

Tactic:
simp
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
f : α → β
g : β → ι
inst : TendstoCofinite g
inst_1 : TendstoCofinite f
r : ι
⊢ (g ∘ f ⁻¹' {r}).Finite

Tactic:
simpa using TendstoCofinite.finite_preimage f (TendstoCofinite.finite_preimage g (by simp))

Premises used: Filter.TendstoCofinite.finite_preimage
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
⊢ TendstoCofinite.{u_1, u_1} (α := α) _root_.id

Tactic:
simp [tendstoCofinite_iff_finite_preimage_singleton]

Premises used: Filter.tendstoCofinite_iff_finite_preimage_singleton
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
e : α ↪ β
⊢ TendstoCofinite.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
⟨e.injective.tendsto_cofinite⟩

Premises used: Function.Injective.tendsto_cofinite, Function.Embedding.injective, Filter.TendstoCofinite.mk
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ TendstoCofinite.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
⟨e.injective.tendsto_cofinite⟩

Premises used: Function.Injective.tendsto_cofinite, Equiv.injective, Filter.TendstoCofinite.mk
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
u v : α → M
h : ∀ (x : β), mapDomain f (u + v) x = (mapDomain f u + mapDomain f v) x
⊢ mapDomain f (u + v) = mapDomain f u + mapDomain f v

Tactic:
ext
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
u v : α → M
x : β
⊢ mapDomain f (u + v) x = (mapDomain f u + mapDomain f v) x

Tactic:
simp [mapDomain, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, Filter.TendstoCofinite.mapDomain
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
inst_2 : DistribSMul R M
r : R
v : α → M
h : ∀ (x : β), mapDomain f (r • v) x = (r • mapDomain f v) x
⊢ mapDomain f (r • v) = r • mapDomain f v

Tactic:
ext
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
inst_2 : DistribSMul R M
r : R
v : α → M
x : β
⊢ mapDomain f (r • v) x = (r • mapDomain f v) x

Tactic:
simp [mapDomain, Finset.smul_sum]

Premises used: Filter.TendstoCofinite.mapDomain, Finset.smul_sum
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
v : α → M
i : β
h' : i ∉ range f
⊢ f ⁻¹' {i} = ∅

Tactic:
rw [← Set.preimage_singleton_eq_empty] at h'

Premises used: Set.preimage_singleton_eq_empty
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
v : α → M
i : β
h' : f ⁻¹' {i} = ∅
⊢ mapDomain f v i = 0

Tactic:
simp [mapDomain, Set.Finite.toFinset, h']

Premises used: Set.Finite.toFinset, Filter.TendstoCofinite.mapDomain
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)

Tactic:
(tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_

Premises used: Iff.mpr, Filter.tendstoCofinite_iff_finite_preimage_singleton
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)

Tactic:
refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_

Premises used: Iff.mpr, Filter.tendstoCofinite_iff_finite_preimage_singleton