awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
h : IsLocalMax f a
s : Set α
⊢ IsLocalMaxOn f s a

Tactic:
h.filter_inf _

Premises used: IsMaxFilter.filter_inf, nhdsWithin, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
h : IsLocalExtr f a
s : Set α
⊢ IsLocalExtrOn f s a

Tactic:
h.filter_inf _

Premises used: nhdsWithin, IsLocalExtrOn, IsExtrFilter.filter_inf
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
t : Set α
hf : IsLocalMinOn f t a
h : s ⊆ t
⊢ IsLocalMinOn f s a

Tactic:
hf.filter_mono <| nhdsWithin_mono a h

Premises used: IsMinFilter.filter_mono, IsLocalMinOn, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
t : Set α
hf : IsLocalMaxOn f t a
h : s ⊆ t
⊢ IsLocalMaxOn f s a

Tactic:
hf.filter_mono <| nhdsWithin_mono a h

Premises used: IsMaxFilter.filter_mono, IsLocalMaxOn, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
t : Set α
hf : IsLocalExtrOn f t a
h : s ⊆ t
⊢ IsLocalExtrOn f s a

Tactic:
hf.filter_mono <| nhdsWithin_mono a h

Premises used: IsLocalExtrOn, IsExtrFilter.filter_mono, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsLocalMinOn f s a
t : Set α
⊢ IsLocalMinOn f (s ∩ t) a

Tactic:
hf.on_subset inter_subset_left

Premises used: Set.inter_subset_left, IsLocalMinOn.on_subset
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsLocalMaxOn f s a
t : Set α
⊢ IsLocalMaxOn f (s ∩ t) a

Tactic:
hf.on_subset inter_subset_left

Premises used: Set.inter_subset_left, IsLocalMaxOn.on_subset
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsLocalExtrOn f s a
t : Set α
⊢ IsLocalExtrOn f (s ∩ t) a

Tactic:
hf.on_subset inter_subset_left

Premises used: Set.inter_subset_left, IsLocalExtrOn.on_subset
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsMinOn f s a
⊢ IsLocalMinOn f s a

Tactic:
hf.filter_mono <| inf_le_right

Premises used: IsMinFilter.filter_mono, IsLocalMinOn, inf_le_right
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsMaxOn f s a
⊢ IsLocalMaxOn f s a

Tactic:
hf.filter_mono <| inf_le_right

Premises used: inf_le_right, IsMaxFilter.filter_mono, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsExtrOn f s a
⊢ IsLocalExtrOn f s a

Tactic:
hf.filter_mono <| inf_le_right

Premises used: IsLocalExtrOn, inf_le_right, IsExtrFilter.filter_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsLocalMinOn f s a
hs : s ∈ 𝓝 a
⊢ IsLocalMin f a

Tactic:
have : 𝓝 a ≤ 𝓟 s := le_principal_iff.2 hs
  hf.filter_mono <| le_inf le_rfl this

Premises used: Iff.mpr, IsMinFilter.filter_mono, le_rfl, Filter.le_principal_iff, le_inf, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsLocalMaxOn f s a
hs : s ∈ 𝓝 a
⊢ IsLocalMax f a

Tactic:
have : 𝓝 a ≤ 𝓟 s := le_principal_iff.2 hs
  hf.filter_mono <| le_inf le_rfl this

Premises used: Iff.mpr, le_rfl, Filter.le_principal_iff, IsLocalMax, IsMaxFilter.filter_mono, le_inf
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsLocalExtrOn f s a
hs : s ∈ 𝓝 a
⊢ IsLocalExtr f a

Tactic:
hf.elim (fun hf => (hf.isLocalMin hs).isExtr) fun hf => (hf.isLocalMax hs).isExtr

Premises used: IsLocalMinOn.isLocalMin, IsMinFilter.isExtr, IsLocalMaxOn.isLocalMax, IsMaxFilter.isExtr, IsLocalExtrOn.elim
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
⊢ IsLocalMinOn f univ a ↔ IsLocalMin f a

Tactic:
simp only [IsLocalMinOn, IsLocalMin, nhdsWithin_univ]

Premises used: nhdsWithin_univ, IsLocalMinOn, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
⊢ IsLocalMaxOn f univ a ↔ IsLocalMax f a

Tactic:
simp only [IsLocalMaxOn, IsLocalMax, nhdsWithin_univ]

Premises used: IsLocalMax, nhdsWithin_univ, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
a : α
⊢ IsLocalExtrOn f univ a ↔ IsLocalExtr f a

Tactic:
isLocalMinOn_univ_iff.or isLocalMaxOn_univ_iff

Premises used: isLocalMinOn_univ_iff, IsLocalMinOn, IsLocalExtr, IsLocalExtrOn, IsLocalMin, Iff.or, IsExtrFilter, isLocalMaxOn_univ_iff
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsMinOn f s a
hs : s ∈ 𝓝 a
⊢ IsLocalMin f a

Tactic:
hf.localize.isLocalMin hs

Premises used: IsLocalMinOn.isLocalMin, IsMinOn.localize
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsMaxOn f s a
hs : s ∈ 𝓝 a
⊢ IsLocalMax f a

Tactic:
hf.localize.isLocalMax hs

Premises used: IsMaxOn.localize, IsLocalMaxOn.isLocalMax
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
hf : IsExtrOn f s a
hs : s ∈ 𝓝 a
⊢ IsLocalExtr f a

Tactic:
hf.localize.isLocalExtr hs

Premises used: IsExtrOn.localize, IsLocalExtrOn.isLocalExtr
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
inst_2 : TopologicalSpace β
hf : IsLocalMinOn f s a
inst_3 : (𝓝[<] f a).NeBot
⊢ ¬𝓝 (f a) ≤ map f (𝓝[s] a)

Tactic:
fun hle =>
  have : ∀ᶠ y in 𝓝[<] f a, f a ≤ y := (eventually_map.2 hf).filter_mono (inf_le_left.trans hle)
  let ⟨_y, hy⟩ := (this.and self_mem_nhdsWithin).exists
  hy.1.not_gt hy.2

Premises used: Iff.mpr, Filter.Eventually.filter_mono, False, Filter.Eventually.and, Filter.eventually_map, _private.0.IsLocalMinOn.not_nhds_le_map.match_1, Filter.Eventually.exists, And.right, self_mem_nhdsWithin, LE.le.not_gt, And.left, inf_le_left, LE.le.trans, Not
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
inst_2 : TopologicalSpace β
hf : IsLocalMaxOn f s a
inst_3 : (𝓝[>] f a).NeBot
⊢ ¬𝓝 (f a) ≤ map f (𝓝[s] a)

Tactic:
@IsLocalMinOn.not_nhds_le_map α βᵒᵈ _ _ _ _ _ ‹_› hf ‹_›

Premises used: Set.Mem, IsLocalMinOn.not_nhds_le_map, OrderDual
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
inst_2 : TopologicalSpace β
hf : IsLocalExtrOn f s a
inst_3 : (𝓝[<] f a).NeBot
inst_4 : (𝓝[>] f a).NeBot
⊢ ¬𝓝 (f a) ≤ map f (𝓝[s] a)

Tactic:
hf.elim (fun h => h.not_nhds_le_map) fun h => h.not_nhds_le_map

Premises used: IsLocalMinOn.not_nhds_le_map, IsLocalMaxOn.not_nhds_le_map, IsLocalExtrOn.elim
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
a : α
b : β
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ b) s a

Tactic:
isMinFilter_const

Premises used: IsLocalMinOn, isMinFilter_const
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
a : α
b : β
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ b) s a

Tactic:
isMaxFilter_const

Premises used: IsLocalMaxOn, isMaxFilter_const
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
a : α
b : β
⊢ IsLocalExtrOn.{u, v} (β := β) (fun (x : α) ↦ b) s a

Tactic:
isExtrFilter_const

Premises used: isExtrFilter_const, IsLocalExtrOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
a : α
b : β
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ b) a

Tactic:
isMinFilter_const

Premises used: IsLocalMin, isMinFilter_const
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
a : α
b : β
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ b) a

Tactic:
isMaxFilter_const

Premises used: IsLocalMax, isMaxFilter_const
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
a : α
b : β
⊢ IsLocalExtr.{u, v} (β := β) (fun (x : α) ↦ b) a

Tactic:
isExtrFilter_const

Premises used: isExtrFilter_const, IsLocalExtr
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
hf : IsLocalMin f a
g : β → γ
hg : Monotone g
⊢ IsLocalMin (g ∘ f) a

Tactic:
hf.comp_mono hg

Premises used: IsLocalMin, IsMinFilter.comp_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
hf : IsLocalMax f a
g : β → γ
hg : Monotone g
⊢ IsLocalMax (g ∘ f) a

Tactic:
hf.comp_mono hg

Premises used: IsLocalMax, IsMaxFilter.comp_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
hf : IsLocalExtr f a
g : β → γ
hg : Monotone g
⊢ IsLocalExtr (g ∘ f) a

Tactic:
hf.comp_mono hg

Premises used: IsExtrFilter.comp_mono, IsLocalExtr
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
hf : IsLocalMin f a
g : β → γ
hg : Antitone g
⊢ IsLocalMax (g ∘ f) a

Tactic:
hf.comp_antitone hg

Premises used: IsLocalMax, IsMinFilter.comp_antitone
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
hf : IsLocalMax f a
g : β → γ
hg : Antitone g
⊢ IsLocalMin (g ∘ f) a

Tactic:
hf.comp_antitone hg

Premises used: IsMaxFilter.comp_antitone, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
hf : IsLocalExtr f a
g : β → γ
hg : Antitone g
⊢ IsLocalExtr (g ∘ f) a

Tactic:
hf.comp_antitone hg

Premises used: IsLocalExtr, IsExtrFilter.comp_antitone
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsLocalMinOn f s a
g : β → γ
hg : Monotone g
⊢ IsLocalMinOn (g ∘ f) s a

Tactic:
hf.comp_mono hg

Premises used: IsLocalMinOn, IsMinFilter.comp_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsLocalMaxOn f s a
g : β → γ
hg : Monotone g
⊢ IsLocalMaxOn (g ∘ f) s a

Tactic:
hf.comp_mono hg

Premises used: IsMaxFilter.comp_mono, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsLocalExtrOn f s a
g : β → γ
hg : Monotone g
⊢ IsLocalExtrOn (g ∘ f) s a

Tactic:
hf.comp_mono hg

Premises used: IsExtrFilter.comp_mono, IsLocalExtrOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsLocalMinOn f s a
g : β → γ
hg : Antitone g
⊢ IsLocalMaxOn (g ∘ f) s a

Tactic:
hf.comp_antitone hg

Premises used: IsLocalMaxOn, IsMinFilter.comp_antitone
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsLocalMaxOn f s a
g : β → γ
hg : Antitone g
⊢ IsLocalMinOn (g ∘ f) s a

Tactic:
hf.comp_antitone hg

Premises used: IsLocalMinOn, IsMaxFilter.comp_antitone
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsLocalExtrOn f s a
g : β → γ
hg : Antitone g
⊢ IsLocalExtrOn (g ∘ f) s a

Tactic:
hf.comp_antitone hg

Premises used: IsLocalExtrOn, IsExtrFilter.comp_antitone
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
inst_3 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsLocalMin f a
g : α → γ
hg : IsLocalMin g a
⊢ IsLocalMin.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) a

Tactic:
hf.bicomp_mono hop hg

Premises used: IsMinFilter.bicomp_mono, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
a : α
inst_3 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsLocalMax f a
g : α → γ
hg : IsLocalMax g a
⊢ IsLocalMax.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) a

Tactic:
hf.bicomp_mono hop hg

Premises used: IsLocalMax, IsMaxFilter.bicomp_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
inst_3 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsLocalMinOn f s a
g : α → γ
hg : IsLocalMinOn g s a
⊢ IsLocalMinOn.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) s a

Tactic:
hf.bicomp_mono hop hg

Premises used: IsLocalMinOn, IsMinFilter.bicomp_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
s : Set α
a : α
inst_3 : Preorder δ
op : β → γ → δ
hop : ((fun (x1 x2 : β) ↦ x1 ≤ x2) ⇒ (fun (x1 x2 : γ) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : δ) ↦ x1 ≤ x2) op op
hf : IsLocalMaxOn f s a
g : α → γ
hg : IsLocalMaxOn g s a
⊢ IsLocalMaxOn.{u, x} (β := δ) (fun (x : α) ↦ op (f x) (g x)) s a

Tactic:
hf.bicomp_mono hop hg

Premises used: IsLocalMaxOn, IsMaxFilter.bicomp_mono
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
g : δ → α
b : δ
hf : IsLocalMin f (g b)
hg : ContinuousAt g b
⊢ IsLocalMin (f ∘ g) b

Tactic:
hg hf

Premises used: Set.Mem, Filter.Eventually, setOf, IsMinFilter, IsLocalMin, Set.preimage
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
g : δ → α
b : δ
hf : IsLocalMax f (g b)
hg : ContinuousAt g b
⊢ IsLocalMax (f ∘ g) b

Tactic:
hg hf

Premises used: IsLocalMax, Set.Mem, Filter.Eventually, setOf, Set.preimage, IsMaxFilter
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
g : δ → α
b : δ
hf : IsLocalExtr f (g b)
hg : ContinuousAt g b
⊢ IsLocalExtr (f ∘ g) b

Tactic:
hf.comp_tendsto hg

Premises used: IsLocalExtr, IsExtrFilter.comp_tendsto
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
s : Set δ
g : δ → α
b : δ
hf : IsLocalMin f (g b)
hg : ContinuousOn g s
hb : b ∈ s
⊢ IsLocalMinOn (f ∘ g) s b

Tactic:
hf.comp_tendsto (hg b hb)

Premises used: IsMinFilter.comp_tendsto, IsLocalMinOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
s : Set δ
g : δ → α
b : δ
hf : IsLocalMax f (g b)
hg : ContinuousOn g s
hb : b ∈ s
⊢ IsLocalMaxOn (f ∘ g) s b

Tactic:
hf.comp_tendsto (hg b hb)

Premises used: IsLocalMaxOn, IsMaxFilter.comp_tendsto
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
s : Set δ
g : δ → α
b : δ
hf : IsLocalExtr f (g b)
hg : ContinuousOn g s
hb : b ∈ s
⊢ IsLocalExtrOn (f ∘ g) s b

Tactic:
hf.elim (fun hf => (hf.comp_continuousOn hg hb).isExtr) fun hf =>
    (IsLocalMax.comp_continuousOn hf hg hb).isExtr

Premises used: IsLocalMax.comp_continuousOn, IsLocalExtr.elim, IsLocalMin.comp_continuousOn, IsMinFilter.isExtr, IsMaxFilter.isExtr
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
t : Set α
s : Set δ
g : δ → α
b : δ
hf : IsLocalMinOn f t (g b)
hst : s ⊆ g ⁻¹' t
hg : ContinuousOn g s
hb : b ∈ s
⊢ IsLocalMinOn (f ∘ g) s b

Tactic:
hf.comp_tendsto
    (tendsto_nhdsWithin_mono_right (image_subset_iff.mpr hst)
      (ContinuousWithinAt.tendsto_nhdsWithin_image (hg b hb)))

Premises used: Iff.mpr, IsMinFilter.comp_tendsto, IsLocalMinOn, tendsto_nhdsWithin_mono_right, ContinuousWithinAt.tendsto_nhdsWithin_image, Set.image_subset_iff
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
t : Set α
s : Set δ
g : δ → α
b : δ
hf : IsLocalMaxOn f t (g b)
hst : s ⊆ g ⁻¹' t
hg : ContinuousOn g s
hb : b ∈ s
⊢ IsLocalMaxOn (f ∘ g) s b

Tactic:
hf.comp_tendsto
    (tendsto_nhdsWithin_mono_right (image_subset_iff.mpr hst)
      (ContinuousWithinAt.tendsto_nhdsWithin_image (hg b hb)))

Premises used: Iff.mpr, tendsto_nhdsWithin_mono_right, IsLocalMaxOn, ContinuousWithinAt.tendsto_nhdsWithin_image, Set.image_subset_iff, IsMaxFilter.comp_tendsto
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
δ : Type x
inst : TopologicalSpace α
inst_1 : Preorder β
f : α → β
inst_2 : TopologicalSpace δ
t : Set α
s : Set δ
g : δ → α
b : δ
hf : IsLocalExtrOn f t (g b)
hst : s ⊆ g ⁻¹' t
hg : ContinuousOn g s
hb : b ∈ s
⊢ IsLocalExtrOn (f ∘ g) s b

Tactic:
hf.elim (fun hf => (hf.comp_continuousOn hst hg hb).isExtr) fun hf =>
    (IsLocalMaxOn.comp_continuousOn hf hst hg hb).isExtr

Premises used: IsLocalMinOn.comp_continuousOn, IsLocalMaxOn.comp_continuousOn, IsMinFilter.isExtr, IsMaxFilter.isExtr, IsLocalExtrOn.elim
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommMonoid β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
hf : IsLocalMin f a
hg : IsLocalMin g a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ f x + g x) a

Tactic:
hf.add hg

Premises used: IsMinFilter.add, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommMonoid β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
hf : IsLocalMax f a
hg : IsLocalMax g a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ f x + g x) a

Tactic:
hf.add hg

Premises used: IsLocalMax, IsMaxFilter.add
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommMonoid β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
hg : IsLocalMinOn g s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ f x + g x) s a

Tactic:
hf.add hg

Premises used: IsMinFilter.add, IsLocalMinOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommMonoid β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
hg : IsLocalMaxOn g s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x + g x) s a

Tactic:
hf.add hg

Premises used: IsMaxFilter.add, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f : α → β
a : α
hf : IsLocalMin f a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ -f x) a

Tactic:
hf.neg

Premises used: IsLocalMax, IsMinFilter.neg
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f : α → β
a : α
hf : IsLocalMax f a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ -f x) a

Tactic:
hf.neg

Premises used: IsMaxFilter.neg, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f : α → β
a : α
hf : IsLocalExtr f a
⊢ IsLocalExtr.{u, v} (β := β) (fun (x : α) ↦ -f x) a

Tactic:
hf.neg

Premises used: IsLocalExtr, IsExtrFilter.neg
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ -f x) s a

Tactic:
hf.neg

Premises used: IsLocalMaxOn, IsMinFilter.neg
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ -f x) s a

Tactic:
hf.neg

Premises used: IsLocalMinOn, IsMaxFilter.neg
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f : α → β
a : α
s : Set α
hf : IsLocalExtrOn f s a
⊢ IsLocalExtrOn.{u, v} (β := β) (fun (x : α) ↦ -f x) s a

Tactic:
hf.neg

Premises used: IsLocalExtrOn, IsExtrFilter.neg
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
hf : IsLocalMin f a
hg : IsLocalMax g a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ f x - g x) a

Tactic:
hf.sub hg

Premises used: IsLocalMin, IsMinFilter.sub
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
hf : IsLocalMax f a
hg : IsLocalMin g a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ f x - g x) a

Tactic:
hf.sub hg

Premises used: IsLocalMax, IsMaxFilter.sub
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
hg : IsLocalMaxOn g s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ f x - g x) s a

Tactic:
hf.sub hg

Premises used: IsLocalMinOn, IsMinFilter.sub