awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
left :
  Membership.mem (γ := Set (β × γ))
    {x : β × γ | ∀ ⦃a : β × γ⦄, Membership.mem (γ := Set (β × γ)) ((fun (x : α) ↦ (f x, g x)) '' d) a → a ≤ x}
    ((fun (x : α) ↦ (f x, g x)) a)
right :
  Membership.mem (γ := Set (β × γ))
    (lowerBounds
      {x : β × γ | ∀ ⦃a : β × γ⦄, Membership.mem (γ := Set (β × γ)) ((fun (x : α) ↦ (f x, g x)) '' d) a → a ≤ x})
    ((fun (x : α) ↦ (f x, g x)) a)
⊢ Membership.mem (γ := Set (β × γ))
      {x : β × γ | ∀ ⦃a : β × γ⦄, Membership.mem (γ := Set (β × γ)) ((fun (x : α) ↦ (f x, g x)) '' d) a → a ≤ x}
      ((fun (x : α) ↦ (f x, g x)) a) ∧
    Membership.mem (γ := Set (β × γ))
      (lowerBounds
        {x : β × γ | ∀ ⦃a : β × γ⦄, Membership.mem (γ := Set (β × γ)) ((fun (x : α) ↦ (f x, g x)) '' d) a → a ≤ x})
      ((fun (x : α) ↦ (f x, g x)) a)

Tactic:
constructor
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
left : ∀ a_1 ∈ d, f a_1 ≤ f a ∧ g a_1 ≤ g a
⊢ Membership.mem (γ := Set (β × γ))
    {x : β × γ | ∀ ⦃a : β × γ⦄, Membership.mem (γ := Set (β × γ)) ((fun (x : α) ↦ (f x, g x)) '' d) a → a ≤ x}
    ((fun (x : α) ↦ (f x, g x)) a)

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, Prod.mk_le_mk, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
b : α
hb : b ∈ d
⊢ f b ≤ f a ∧ g b ≤ g a

Tactic:
⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩

Premises used: ScottContinuousOn.monotone, And.left, And.intro
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
b : α
hb : b ∈ d
⊢ f b ≤ f a ∧ g b ≤ g a

Tactic:
exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp :
  Membership.mem (γ := Set (β × γ))
    {x : β × γ | ∀ ⦃a : β × γ⦄, Membership.mem (γ := Set (β × γ)) ((fun (x : α) ↦ (f x, g x)) '' d) a → a ≤ x} (p₁, p₂)
⊢ ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk] at hp

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, Prod.mk_le_mk, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
right : ((fun (x : α) ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1
right₁ : ((fun (x : α) ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2
⊢ (fun (x : α) ↦ (f x, g x)) a ≤ (p₁, p₂)

Tactic:
constructor
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
right : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x} (p₁, p₂).1
⊢ ((fun (x : α) ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1

Tactic:
rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]

Premises used: upperBounds, isLUB_le_iff
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
right : ∀ a ∈ d, f a ≤ p₁
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x} (p₁, p₂).1

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a_1 : α
hb : a_1 ∈ d
⊢ f a_1 ≤ p₁

Tactic:
(hp _ hb).1

Premises used: And.left
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a_1 : α
hb : a_1 ∈ d
⊢ f a_1 ≤ p₁

Tactic:
exact (hp _ hb).1

Premises used: And.left
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
right : Membership.mem (γ := Set γ) {x : γ | ∀ ⦃a : γ⦄, a ∈ g '' d → a ≤ x} (p₁, p₂).2
⊢ ((fun (x : α) ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2

Tactic:
rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]

Premises used: upperBounds, isLUB_le_iff
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
right : ∀ a ∈ d, g a ≤ p₂
⊢ Membership.mem (γ := Set γ) {x : γ | ∀ ⦃a : γ⦄, a ∈ g '' d → a ≤ x} (p₁, p₂).2

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a_1 : α
hb : a_1 ∈ d
⊢ g a_1 ≤ p₂

Tactic:
(hp _ hb).2

Premises used: And.right
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a_1 : α
hb : a_1 ∈ d
⊢ g a_1 ≤ p₂

Tactic:
exact (hp _ hb).2

Premises used: And.right
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB d a
⊢ IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2

Tactic:
simp only [isLUB_prod] at ha

Premises used: isLUB_prod
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.fst '' d) a.1

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.fst '' d) a.1

Tactic:
exact ha.1

Premises used: And.left
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.snd '' d) a.2

Tactic:
ha.2

Premises used: And.right
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.snd '' d) a.2

Tactic:
exact ha.2

Premises used: And.right
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ ScottContinuousOn univ f ↔ ScottContinuous f

Tactic:
simp [ScottContinuousOn, ScottContinuous]

Premises used: ScottContinuous, ScottContinuousOn
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
D : Set (Set α)
⊢ ScottContinuous f → ScottContinuousOn D f

Tactic:
fun h _ _ d₂ d₃ _ hda => h d₂ d₃ hda

Premises used: ScottContinuousOn
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : ScottContinuous f
⊢ Monotone f

Tactic:
h.scottContinuousOn.monotone univ (fun _ _ _ ↦ mem_univ _)

Premises used: ScottContinuousOn.monotone, Set.univ, Insert.insert, Set.mem_univ, Singleton.singleton, ScottContinuous.scottContinuousOn
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
inst : Preorder α
⊢ ScottContinuous.{u_1, u_1} (α := α) _root_.id

Tactic:
simp [ScottContinuous]

Premises used: ScottContinuous
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : β
simp_rw : ScottContinuousOn univ (Function.const α x)
⊢ ScottContinuous (Function.const α x)

Tactic:
simp_rw [← scottContinuousOn_univ, ScottContinuousOn.const]

Premises used: ScottContinuousOn.const, scottContinuousOn_univ
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuous f
hg : ScottContinuous g
rw : ∀ (hf : ScottContinuousOn univ f) (hg : ScottContinuousOn univ g), ScottContinuousOn univ (g ∘ f)
⊢ ScottContinuous (g ∘ f)

Tactic:
rw [← scottContinuousOn_univ] at ⊢ hf hg

Premises used: scottContinuousOn_univ
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ∀ (a b : α), a ≤ b → Membership.mem (γ := Set (Set α)) univ {a, b}

Tactic:
simp
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ MapsTo.{u_1, u_2} (β := Set β) (fun (x : Set α) ↦ f '' x) univ univ

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn univ (g ∘ f)

Tactic:
exact ScottContinuousOn.comp (by simp) (by simp [MapsTo]) hg hf

Premises used: ScottContinuousOn.comp
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuous f
hg : ScottContinuous g
rw :
  ∀ (hf : ScottContinuousOn univ f) (hg : ScottContinuousOn univ g),
    ScottContinuousOn (β := β × γ) univ fun (x : α) ↦ (f x, g x)
⊢ ScottContinuous (β := β × γ) fun (x : α) ↦ (f x, g x)

Tactic:
rw [← scottContinuousOn_univ] at ⊢ hf hg

Premises used: scottContinuousOn_univ
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ∀ (a b : α), a ≤ b → Membership.mem (γ := Set (Set α)) univ {a, b}

Tactic:
grind
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn (β := β × γ) univ fun (x : α) ↦ (f x, g x)

Tactic:
exact ScottContinuousOn.prodMk (by grind) hf hg

Premises used: ScottContinuousOn.prodMk
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
simp_rw : ScottContinuousOn (α := α × β) univ Prod.fst
⊢ ScottContinuous (α := α × β) Prod.fst

Tactic:
simp_rw [← scottContinuousOn_univ, ScottContinuousOn.fst]

Premises used: scottContinuousOn_univ, ScottContinuousOn.fst
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
simp_rw : ScottContinuousOn (α := α × β) univ Prod.snd
⊢ ScottContinuous (α := α × β) Prod.snd

Tactic:
simp_rw [← scottContinuousOn_univ, ScottContinuousOn.snd]

Premises used: ScottContinuousOn.snd, scottContinuousOn_univ
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp : IsLUB d (p₁, p₂)
⊢ (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)

Tactic:
simp only [IsLUB, IsLeast, upperBounds, Prod.forall, mem_setOf_eq, Prod.mk_le_mk] at hdp

Premises used: upperBounds, Set.mem_setOf_eq, IsLeast, IsLUB, Prod.forall, Prod.mk_le_mk
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
simp :
  Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)
⊢ IsLUB (α := β) ((fun (b : β × β) ↦ b.1 ⊔ b.2) '' d) ((fun (b : β × β) ↦ b.1 ⊔ b.2) (p₁, p₂))

Tactic:
simp only [IsLUB, IsLeast, upperBounds, mem_image, Prod.exists, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, upperBounds, IsLeast, IsLUB, Prod.exists
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
⊢ Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}) (p₁, p₂)

Tactic:
have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}) (p₁, p₂)
⊢ ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b

Tactic:
simp only [lowerBounds, mem_setOf_eq, Prod.forall, Prod.mk_le_mk] at e1

Premises used: lowerBounds, Set.mem_setOf_eq, Prod.forall, Prod.mk_le_mk
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)

Tactic:
⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
refine_1 : ∀ (a b₁ b₂ : β) (hbd : (b₁, b₂) ∈ d) (hba : b₁ ⊔ b₂ = a), a ≤ p₁ ⊔ p₂
refine_2 :
  ∀ (b : β)
    (hb : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} b),
    p₁ ⊔ p₂ ≤ b
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)

Tactic:
refine ⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
refine_1 : b₁ ⊔ b₂ ≤ p₁ ⊔ p₂
⊢ a ≤ p₁ ⊔ p₂

Tactic:
rw [← hba]
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ b₁ ⊔ b₂ ≤ p₁ ⊔ p₂

Tactic:
sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2

Premises used: sup_le_sup, And.right, And.left
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ b₁ ⊔ b₂ ≤ p₁ ⊔ p₂

Tactic:
exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2

Premises used: sup_le_sup, And.right, And.left
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b : β
hb : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} b
refine_2 : p₁ ≤ b ∧ p₂ ≤ b
⊢ p₁ ⊔ p₂ ≤ b

Tactic:
rw [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b : β
hb : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} b
⊢ p₁ ≤ b ∧ p₂ ≤ b

Tactic:
e1 _ _ fun b₁ b₂ hb' => sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Premises used: sup_le_iff, Iff.mp, rfl
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b : β
hb : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} b
⊢ p₁ ≤ b ∧ p₂ ≤ b

Tactic:
exact e1 _ _ fun b₁ b₂ hb' => sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Premises used: sup_le_iff, Iff.mp, rfl