awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.{u_2, u_1} (Y := L) (fun (a : X) ↦ f a ⊔ g a) s x

Tactic:
hf.sup' hg

Premises used: ContinuousWithinAt.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
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (f ⊔ g) s

Tactic:
fun x hx ↦
  (hf x hx).sup' (hg x hx)

Premises used: ContinuousWithinAt.sup', ContinuousOn
-- 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
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ f a ⊔ g a) s

Tactic:
hf.sup' hg

Premises used: ContinuousOn.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] (f ⊔ g)

Tactic:
hf.sup hg

Premises used: 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 : Min L
inst_3 : ContinuousInf L
f g : X → L
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (f ⊓ g) x

Tactic:
hf.inf_nhds' hg

Premises used: ContinuousAt, Filter.Tendsto.inf_nhds'
-- 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
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.inf' hg

Premises used: ContinuousAt.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
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (f ⊓ g) s x

Tactic:
hf.inf_nhds' hg

Premises used: ContinuousWithinAt, Filter.Tendsto.inf_nhds'
-- 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
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ f a ⊓ g a) s x

Tactic:
hf.inf' hg

Premises used: ContinuousWithinAt.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
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (f ⊓ g) s

Tactic:
fun x hx ↦
  (hf x hx).inf' (hg x hx)

Premises used: ContinuousWithinAt.inf', ContinuousOn
-- 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
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ f a ⊓ g a) s

Tactic:
hf.inf' hg

Premises used: ContinuousOn.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] (f ⊓ g)

Tactic:
hf.inf hg

Premises used: Continuous.inf
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.sup' hne fun (x : ι) ↦ f x a) x

Tactic:
Tendsto.finset_sup'_nhds_apply hne hs

Premises used: ContinuousAt, Filter.Tendsto.finset_sup'_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup' hne f) x

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

Premises used: Finset.sup'_apply, ContinuousAt.finset_sup'_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.sup' hne fun (x : ι) ↦ f x a) t x

Tactic:
Tendsto.finset_sup'_nhds_apply hne hs

Premises used: ContinuousWithinAt, Filter.Tendsto.finset_sup'_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup' hne f) t x

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

Premises used: Finset.sup'_apply, ContinuousWithinAt.finset_sup'_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.sup' hne fun (x : ι) ↦ f x a) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_sup'_apply hne fun i hi ↦ hs i hi x hx

Premises used: ContinuousOn, ContinuousWithinAt.finset_sup'_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn (s.sup' hne f) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_sup' hne fun i hi ↦ hs i hi x hx

Premises used: ContinuousOn, ContinuousWithinAt.finset_sup'
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
hne : s.Nonempty
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] fun (a : X) ↦ s.sup' hne fun (x : ι) ↦ f x a

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup'_apply _ fun i hi ↦
    (hs i hi).continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.finset_sup'_apply, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : ContinuousSup L
s : Finset ι
f : ι → X → L
hne : s.Nonempty
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] (s.sup' hne f)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup' _ fun i hi ↦ (hs i hi).continuousAt

Premises used: Iff.mpr, ContinuousAt.finset_sup', Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.sup fun (x : ι) ↦ f x a) x

Tactic:
Tendsto.finset_sup_nhds_apply hs

Premises used: ContinuousAt, Filter.Tendsto.finset_sup_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup f) x

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

Premises used: ContinuousAt.finset_sup_apply, Finset.sup_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.sup fun (x : ι) ↦ f x a) t x

Tactic:
Tendsto.finset_sup_nhds_apply hs

Premises used: ContinuousWithinAt, Filter.Tendsto.finset_sup_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup f) t x

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

Premises used: ContinuousWithinAt.finset_sup_apply, Finset.sup_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.sup fun (x : ι) ↦ f x a) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_sup_apply fun i hi ↦ hs i hi x hx

Premises used: ContinuousWithinAt.finset_sup_apply, ContinuousOn
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn (s.sup f) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_sup fun i hi ↦ hs i hi x hx

Premises used: ContinuousWithinAt.finset_sup, ContinuousOn
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] fun (a : X) ↦ s.sup fun (x : ι) ↦ f x a

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup_apply fun i hi ↦
    (hs i hi).continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.finset_sup_apply, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeSup L
inst_3 : OrderBot L
inst_4 : ContinuousSup L
s : Finset ι
f : ι → X → L
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] (s.sup f)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup fun i hi ↦ (hs i hi).continuousAt

Premises used: Iff.mpr, ContinuousAt.finset_sup, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.inf' hne fun (x : ι) ↦ f x a) x

Tactic:
Tendsto.finset_inf'_nhds_apply hne hs

Premises used: ContinuousAt, Filter.Tendsto.finset_inf'_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf' hne f) x

Tactic:
simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

Premises used: ContinuousAt.finset_inf'_apply, Finset.inf'_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.inf' hne fun (x : ι) ↦ f x a) t x

Tactic:
Tendsto.finset_inf'_nhds_apply hne hs

Premises used: ContinuousWithinAt, Filter.Tendsto.finset_inf'_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf' hne f) t x

Tactic:
simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

Premises used: ContinuousWithinAt.finset_inf'_apply, Finset.inf'_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.inf' hne fun (x : ι) ↦ f x a) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_inf'_apply hne fun i hi ↦ hs i hi x hx

Premises used: ContinuousWithinAt.finset_inf'_apply, ContinuousOn
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn (s.inf' hne f) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_inf' hne fun i hi ↦ hs i hi x hx

Premises used: ContinuousWithinAt.finset_inf', ContinuousOn
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
hne : s.Nonempty
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] fun (a : X) ↦ s.inf' hne fun (x : ι) ↦ f x a

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf'_apply _ fun i hi ↦
    (hs i hi).continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.finset_inf'_apply, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : ContinuousInf L
s : Finset ι
f : ι → X → L
hne : s.Nonempty
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] (s.inf' hne f)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf' _ fun i hi ↦ (hs i hi).continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.finset_inf', continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.inf fun (x : ι) ↦ f x a) x

Tactic:
Tendsto.finset_inf_nhds_apply hs

Premises used: ContinuousAt, Filter.Tendsto.finset_inf_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf f) x

Tactic:
simpa only [← Finset.inf_apply] using finset_inf_apply hs

Premises used: Finset.inf_apply, ContinuousAt.finset_inf_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.inf fun (x : ι) ↦ f x a) t x

Tactic:
Tendsto.finset_inf_nhds_apply hs

Premises used: ContinuousWithinAt, Filter.Tendsto.finset_inf_nhds_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf f) t x

Tactic:
simpa only [← Finset.inf_apply] using finset_inf_apply hs

Premises used: ContinuousWithinAt.finset_inf_apply, Finset.inf_apply
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn.{u_2, u_1} (Y := L) (fun (a : X) ↦ s.inf fun (x : ι) ↦ f x a) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_inf_apply fun i hi ↦ hs i hi x hx

Premises used: ContinuousWithinAt.finset_inf_apply, ContinuousOn
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
hs : ∀ i ∈ s, ContinuousOn (f i) t
⊢ ContinuousOn (s.inf f) t

Tactic:
fun x hx ↦
  ContinuousWithinAt.finset_inf fun i hi ↦ hs i hi x hx

Premises used: ContinuousWithinAt.finset_inf, ContinuousOn
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] fun (a : X) ↦ s.inf fun (x : ι) ↦ f x a

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf_apply fun i hi ↦
    (hs i hi).continuousAt

Premises used: Iff.mpr, ContinuousAt.finset_inf_apply, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Lattice
Goal:
L : Type u_1
X : Type u_2
inst : TopologicalSpace L
inst_1 : TopologicalSpace X
ι : Type u_3
inst_2 : SemilatticeInf L
inst_3 : OrderTop L
inst_4 : ContinuousInf L
s : Finset ι
f : ι → X → L
hs : ∀ i ∈ s, Continuous[inst_1, inst] (f i)
⊢ Continuous[inst_1, inst] (s.inf f)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf fun i hi ↦ (hs i hi).continuousAt

Premises used: Iff.mpr, ContinuousAt.finset_inf, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
simp_rw :
  Eq.{u_1 + 1} (α := Set (Set α))
    {s : Set α | ∃ (t : Set α), t.Finite ∧ ∃ (u : Set α), IsOpen[scott α univ] u ∧ (↑(upperClosure t) : Set α)ᶜ ∩ u = s}
    {c : Set α |
      ∃ (a : Set (WithLower α)),
        Membership.mem (γ := Set (Set (WithLower α)))
            {s : Set (WithLower α) | ∃ (t : Set (WithLower α)), t.Finite ∧ (↑(upperClosure t) : Set (WithLower α))ᶜ = s}
            a ∧
          ∃ (b : Set (WithScott α)),
            Membership.mem (γ := Set (Set (WithScott α))) {U : Set (WithScott α) | IsOpen[scott α univ] U} b ∧
              (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' a ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' b =
                c}
⊢ Eq.{u_1 + 1} (α := Set (Set α))
    {s : Set α | ∃ (t : Set α), t.Finite ∧ ∃ (u : Set α), IsOpen[scott α univ] u ∧ u \ (↑(upperClosure t) : Set α) = s}
    {c : Set α |
      ∃ (a : Set (WithLower α)),
        Membership.mem (γ := Set (Set (WithLower α)))
            {s : Set (WithLower α) | ∃ (t : Set (WithLower α)), t.Finite ∧ (↑(upperClosure t) : Set (WithLower α))ᶜ = s}
            a ∧
          ∃ (b : Set (WithScott α)),
            Membership.mem (γ := Set (Set (WithScott α))) {U : Set (WithScott α) | IsOpen[scott α univ] U} b ∧
              (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' a ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' b =
                c}

Tactic:
simp_rw [diff_eq_compl_inter]

Premises used: Set.diff_eq_compl_inter
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
⊢ Eq.{u_1 + 1} (α := Set (Set α))
    {s : Set α | ∃ (t : Set α), t.Finite ∧ ∃ (u : Set α), IsOpen[scott α univ] u ∧ (↑(upperClosure t) : Set α)ᶜ ∩ u = s}
    {c : Set α |
      ∃ (a : Set (WithLower α)),
        Membership.mem (γ := Set (Set (WithLower α)))
            {s : Set (WithLower α) | ∃ (t : Set (WithLower α)), t.Finite ∧ (↑(upperClosure t) : Set (WithLower α))ᶜ = s}
            a ∧
          ∃ (b : Set (WithScott α)),
            Membership.mem (γ := Set (Set (WithScott α))) {U : Set (WithScott α) | IsOpen[scott α univ] U} b ∧
              (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' a ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' b =
                c}

Tactic:
aesop
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
⊢ lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}

Tactic:
have lawsonBasis_image2 : lawsonBasis α =
      (image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1)
        (IsLower.lowerBasis (WithLower α)) {U | IsOpen[scott α univ] U}) := by
    rw [lawsonBasis, image2, IsLower.lowerBasis]
    simp_rw [diff_eq_compl_inter]
    aesop
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
rw :
  IsTopologicalBasis.{u_1} (α := α)
    (image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U})
⊢ IsTopologicalBasis (lawsonBasis α)

Tactic:
rw [lawsonBasis_image2]