awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h_1 : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h : IsTop d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
.of_forall (fun _ ↦ h _)

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h_1 : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h : IsTop d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
exact .of_forall (fun _ ↦ h _)
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
⊢ (Ioi d).Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
inl : ∀ (u : ℕ → α) (hu_tt : Tendsto u atTop (𝓝 d)) (hu_gt : ∀ (n : ℕ), u n ∈ Ioi d), ∀ᶠ (x : γ) in l, f x ≤ d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
obtain ⟨u, -, -, hu_tt, hu_gt⟩ := hd.exists_seq_antitone_tendsto (by simpa)

Premises used: IsGLB.exists_seq_antitone_tendsto
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
n : ℕ
⊢ d < u n

Tactic:
grind
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
⊢ ∀ (n : ℕ), ∀ᶠ (x : γ) in l, f x < u n

Tactic:
replace h := fun n ↦ h (u n) (by grind)
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ (n : ℕ), ∀ᶠ (x : γ) in l, f x < u n
⊢ ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i

Tactic:
rw [← eventually_countable_forall] at h

Premises used: eventually_countable_forall
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
h₁ : ∀ (x : γ) (hx : ∀ (i : ℕ), f x < u i), f x ≤ d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
x : γ
hx : ∀ (i : ℕ), f x < u i
⊢ f x ≤ d

Tactic:
ge_of_tendsto hu_tt <| .of_forall <| fun n ↦ le_of_lt <| hx n

Premises used: ge_of_tendsto, le_of_lt, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
x : γ
hx : ∀ (i : ℕ), f x < u i
⊢ f x ≤ d

Tactic:
exact ge_of_tendsto hu_tt <| .of_forall <| fun n ↦ le_of_lt <| hx n

Premises used: ge_of_tendsto, le_of_lt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
⊢ a < d

Tactic:
simp [← Set.mem_Ioi, H0]

Premises used: Set.mem_Ioi
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
⊢ ∀ᶠ (x : γ) in l, f x < d

Tactic:
specialize h d <| by simp [← Set.mem_Ioi, H0]
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
h : ∀ᶠ (x : γ) in l, f x < d
h₁ : ∀ (x : γ) (hx : f x < d), f x ≤ a
⊢ ∀ᶠ (x : γ) in l, f x ≤ a

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
h : ∀ᶠ (x : γ) in l, f x < d
x : γ
hx : f x < d
h₁ : ∀ (H0 : Iic a = Iio d) (h : ∀ᶠ (x : γ) in l, f x < d) (x : γ) (hx : f x < d), f x ≤ a
⊢ f x ≤ a

Tactic:
rw [← Set.compl_Iic, ← Set.compl_Iio, compl_inj_iff] at H0

Premises used: Set.compl_Iic, Set.compl_Iio, compl_inj_iff
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a d : α
hd : IsGLB (Ioi a) d
H0 : Iic a = Iio d
h : ∀ᶠ (x : γ) in l, f x < d
x : γ
hx : f x < d
⊢ f x ≤ a

Tactic:
simpa [← Set.mem_Iic, ← Set.mem_Iio, H0] using hx

Premises used: Set.mem_Iio, Set.mem_Iic
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
⊢ (∀ᶠ (x : γ) in l, a ≤ f x) ↔ ∀ b < a, ∀ᶠ (x : γ) in l, b < f x

Tactic:
eventually_le_const_iff_forall_gt_eventually_lt_const (α := αᵒᵈ)

Premises used: OrderDual, eventually_le_const_iff_forall_gt_eventually_lt_const
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : Preorder X
inst_2 : OrderClosedTopology X
⊢ IsLocallyClosed (Set.Icc a b)

Tactic:
isClosed_Icc.isLocallyClosed

Premises used: isClosed_Icc, IsClosed.isLocallyClosed
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : OrderClosedTopology X
⊢ IsLocallyClosed (Set.Ioo a b)

Tactic:
isOpen_Ioo.isLocallyClosed

Premises used: isOpen_Ioo, IsOpen.isLocallyClosed
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
inst_1 : Preorder X
inst_2 : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Ici a)

Tactic:
isClosed_Ici.isLocallyClosed

Premises used: IsClosed.isLocallyClosed, isClosed_Ici
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
inst_1 : Preorder X
inst_2 : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Iic a)

Tactic:
isClosed_Iic.isLocallyClosed

Premises used: isClosed_Iic, IsClosed.isLocallyClosed
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
inst_1 : LinearOrder X
inst_2 : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Ioi a)

Tactic:
isOpen_Ioi.isLocallyClosed

Premises used: IsOpen.isLocallyClosed, isOpen_Ioi
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a : X
inst_1 : LinearOrder X
inst_2 : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio a)

Tactic:
isOpen_Iio.isLocallyClosed

Premises used: isOpen_Iio, IsOpen.isLocallyClosed
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIicTopology X
rw : IsLocallyClosed (Set.Iic b ∩ Set.Ioi a)
⊢ IsLocallyClosed (Set.Ioc a b)

Tactic:
rw [← Set.Iic_inter_Ioi]

Premises used: Set.Iic_inter_Ioi
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Iic b ∩ Set.Ioi a)

Tactic:
isLocallyClosed_Iic.inter isLocallyClosed_Ioi

Premises used: isLocallyClosed_Ioi, IsLocallyClosed.inter, isLocallyClosed_Iic
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Iic b ∩ Set.Ioi a)

Tactic:
exact isLocallyClosed_Iic.inter isLocallyClosed_Ioi

Premises used: isLocallyClosed_Ioi, IsLocallyClosed.inter, isLocallyClosed_Iic
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIciTopology X
rw : IsLocallyClosed (Set.Iio b ∩ Set.Ici a)
⊢ IsLocallyClosed (Set.Ico a b)

Tactic:
rw [← Set.Iio_inter_Ici]

Premises used: Set.Iio_inter_Ici
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)

Tactic:
isLocallyClosed_Iio.inter isLocallyClosed_Ici

Premises used: isLocallyClosed_Ici, IsLocallyClosed.inter, isLocallyClosed_Iio
-- Module: Mathlib.Topology.Order.IsLocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)

Tactic:
exact isLocallyClosed_Iio.inter isLocallyClosed_Ici

Premises used: isLocallyClosed_Ici, IsLocallyClosed.inter, isLocallyClosed_Iio
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
inst_1 : Min L
inst_2 : ContinuousInf L
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : L × L) ↦ p.1 ⊓ p.2

Tactic:
ContinuousInf.continuous_inf

Premises used: ContinuousInf.continuous_inf
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
inst_2 : Min L
inst_3 : ContinuousInf L
f g : X → L
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, inst] g
⊢ Continuous[inst_1, inst] fun (x : X) ↦ f x ⊓ g x

Tactic:
continuous_inf.comp (hf.prodMk hg :)

Premises used: Continuous.comp, continuous_inf, Continuous.prodMk
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
inst_1 : Max L
inst_2 : ContinuousSup L
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : L × L) ↦ p.1 ⊔ p.2

Tactic:
ContinuousSup.continuous_sup

Premises used: ContinuousSup.continuous_sup
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
inst_2 : Max L
inst_3 : ContinuousSup L
f g : X → L
hf : Continuous[inst_1, inst] f
hg : Continuous[inst_1, inst] g
⊢ Continuous[inst_1, inst] fun (x : X) ↦ f x ⊔ g x

Tactic:
continuous_sup.comp (hf.prodMk hg :)

Premises used: Continuous.comp, continuous_sup, Continuous.prodMk
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
α : Type u_3
l : Filter α
f g : α → L
x y : L
inst_1 : Max L
inst_2 : ContinuousSup L
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (f ⊔ g) l (𝓝 (x ⊔ y))

Tactic:
(continuous_sup.tendsto _).comp (hf.prodMk_nhds hg)

Premises used: continuous_sup, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
α : Type u_3
l : Filter α
f g : α → L
x y : L
inst_1 : Max L
inst_2 : ContinuousSup L
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (fun (i : α) ↦ f i ⊔ g i) l (𝓝 (x ⊔ y))

Tactic:
hf.sup_nhds' hg

Premises used: Filter.Tendsto.sup_nhds'
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
α : Type u_3
l : Filter α
f g : α → L
x y : L
inst_1 : Min L
inst_2 : ContinuousInf L
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (f ⊓ g) l (𝓝 (x ⊓ y))

Tactic:
(continuous_inf.tendsto _).comp (hf.prodMk_nhds hg)

Premises used: continuous_inf, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
α : Type u_3
l : Filter α
f g : α → L
x y : L
inst_1 : Min L
inst_2 : ContinuousInf L
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (fun (i : α) ↦ f i ⊓ g i) l (𝓝 (x ⊓ y))

Tactic:
hf.inf_nhds' hg

Premises used: Filter.Tendsto.inf_nhds'
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
hs : ∀ (i : ι), Membership.mem (γ := Finset ι) {a} i → Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (sup' {a} ⋯ f) l (𝓝 (sup' {a} ⋯ g))

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s_1 : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))

Tactic:
rw [forall_mem_cons] at hs

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s_1 : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
cons : Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))
⊢ Tendsto ((Finset.cons a s ha).sup' ⋯ f) l (𝓝 ((Finset.cons a s ha).sup' ⋯ g))

Tactic:
simp only [sup'_cons, hne]

Premises used: Finset.sup'_cons
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s_1 : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))

Tactic:
hs.1.sup_nhds (ihs hs.2)

Premises used: Filter.Tendsto.sup_nhds, And.right, And.left
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s_1 : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))

Tactic:
exact hs.1.sup_nhds (ihs hs.2)

Premises used: Filter.Tendsto.sup_nhds, And.right, And.left
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
singleton :
  ∀ (a : ι) (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) {a} i → Tendsto (f i) l (𝓝 (g i))),
    Tendsto (sup' {a} ⋯ f) l (𝓝 (sup' {a} ⋯ g))
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (hne : s.Nonempty)
    (ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g)))
    (hs : ∀ i ∈ Finset.cons a s ha, Tendsto (f i) l (𝓝 (g i))),
    Tendsto ((Finset.cons a s ha).sup' ⋯ f) l (𝓝 ((Finset.cons a s ha).sup' ⋯ g))
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
induction hne using Finset.Nonempty.cons_induction with
  | singleton => simpa using hs
  | cons a s ha hne ihs =>
    rw [forall_mem_cons] at hs
    simp only [sup'_cons, hne]
    exact hs.1.sup_nhds (ihs hs.2)

Premises used: Finset.cons, Finset.forall_mem_cons, Finset.sup'_cons, Singleton.singleton
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun (a : α) ↦ s.sup' hne fun (x : ι) ↦ f x a) l (𝓝 (s.sup' hne g))

Tactic:
simpa only [← Finset.sup'_apply] using finset_sup'_nhds hne hs

Premises used: Finset.sup'_apply, Filter.Tendsto.finset_sup'_nhds
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeInf L
inst_2 : ContinuousInf L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.inf' hne f) l (𝓝 (s.inf' hne g))

Tactic:
finset_sup'_nhds (L := Lᵒᵈ) hne hs

Premises used: Finset.inf', WithTop.some, Filter.Tendsto.finset_sup'_nhds, WithTop.untop, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeInf L
inst_2 : ContinuousInf L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun (a : α) ↦ s.inf' hne fun (x : ι) ↦ f x a) l (𝓝 (s.inf' hne g))

Tactic:
finset_sup'_nhds_apply (L := Lᵒᵈ) hne hs

Premises used: Finset.inf', WithTop.some, WithTop.untop, Filter.Tendsto.finset_sup'_nhds_apply, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
inl :
  ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) l (𝓝 (g i))),
    Tendsto (Finset.sup ∅ f) l (𝓝 (Finset.sup ∅ g))
inr : ∀ (hne : s.Nonempty), Tendsto (s.sup f) l (𝓝 (s.sup g))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (Finset.sup ∅ f) l (𝓝 (Finset.sup ∅ g))

Tactic:
simpa using tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
inr : Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
simp only [← sup'_eq_sup hne]

Premises used: Finset.sup'_eq_sup
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
finset_sup'_nhds hne hs

Premises used: Filter.Tendsto.finset_sup'_nhds
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
exact finset_sup'_nhds hne hs

Premises used: Filter.Tendsto.finset_sup'_nhds
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun (a : α) ↦ s.sup fun (x : ι) ↦ f x a) l (𝓝 (s.sup g))

Tactic:
simpa only [← Finset.sup_apply] using finset_sup_nhds hs

Premises used: Filter.Tendsto.finset_sup_nhds, Finset.sup_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeInf L
inst_2 : OrderTop L
inst_3 : ContinuousInf L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.inf f) l (𝓝 (s.inf g))

Tactic:
finset_sup_nhds (L := Lᵒᵈ) hs

Premises used: Filter.Tendsto.finset_sup_nhds, OrderDual, Finset.inf
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeInf L
inst_2 : OrderTop L
inst_3 : ContinuousInf L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun (a : α) ↦ s.inf fun (x : ι) ↦ f x a) l (𝓝 (s.inf g))

Tactic:
finset_sup_nhds_apply (L := Lᵒᵈ) hs

Premises used: Filter.Tendsto.finset_sup_nhds_apply, OrderDual, Finset.inf
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
inst_2 : Max L
inst_3 : ContinuousSup L
f g : X → L
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (f ⊔ g) x

Tactic:
hf.sup_nhds' hg

Premises used: ContinuousAt, Filter.Tendsto.sup_nhds'
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
inst_2 : Max L
inst_3 : ContinuousSup L
f g : X → L
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ f a ⊔ g a) x

Tactic:
hf.sup' hg

Premises used: ContinuousAt.sup'
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
inst_2 : Max L
inst_3 : ContinuousSup L
f g : X → L
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (f ⊔ g) s x

Tactic:
hf.sup_nhds' hg

Premises used: ContinuousWithinAt, Filter.Tendsto.sup_nhds'