awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
rw : IsLUB {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x} (f (p1, p2))
⊢ IsLUB (f '' d) (f (p1, p2))

Tactic:
rw [isLUB_congr ((monotone_prod_iff.mpr ⟨h₁', h₂'⟩).upperBounds_image_of_directedOn_prod hd₂),
    ← iUnion_of_singleton_coe (Prod.fst '' d), iUnion_prod_const, image_iUnion,
    ← isLUB_iUnion_iff_of_isLUB (fun a => by
      rw [singleton_prod, image_image f (fun b ↦ (a, b))]
      exact h₁ _ (mem_image_of_mem (fun d ↦ Prod.snd '' d) hX) (Nonempty.image Prod.snd hd₁)
        (DirectedOn.snd hd₂) (isLUB_prod.mp hdp).2) _, Set.range]

Premises used: Iff.mpr, monotone_prod_iff, isLUB_congr, Set.iUnion_prod_const, Monotone.upperBounds_image_of_directedOn_prod, Set.image_iUnion, Prod.fst, isLUB_iUnion_iff_of_isLUB, And.intro, Set.image, Set.range, Set.iUnion_of_singleton_coe
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB.{u_3} (α := γ) ((fun (a : α) ↦ f (a, p2)) '' (fun (d : Set (α × β)) ↦ Prod.fst '' d) d)
    ((fun (a : α) ↦ f (a, p2)) (p1, p2).1)

Tactic:
(h₂ _ (mem_image_of_mem (fun d ↦ Prod.fst '' d) hX) (Nonempty.image Prod.fst hd₁)
      (DirectedOn.fst hd₂) (isLUB_prod.mp hdp).1)

Premises used: DirectedOn.fst, Prod.fst, isLUB_prod, And.left, Set.mem_image_of_mem, Set.Nonempty.image, Iff.mp, Set.image
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
h :
  Eq.{u_3 + 1} (α := Set γ)
    {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x}
    ((fun (a : α) ↦ f (a, p2)) '' (fun (d : Set (α × β)) ↦ Prod.fst '' d) d)
⊢ IsLUB {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x} (f (p1, p2))

Tactic:
convert!
    (h₂ _ (mem_image_of_mem (fun d ↦ Prod.fst '' d) hX) (Nonempty.image Prod.fst hd₁)
      (DirectedOn.fst hd₂) (isLUB_prod.mp hdp).1)

Premises used: DirectedOn.fst, Prod.fst, isLUB_prod, And.left, Set.mem_image_of_mem, Set.Nonempty.image, Iff.mp, Set.image
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
h :
  ∀ (x : γ),
    Membership.mem (γ := Set γ)
        {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x} x ↔
      Membership.mem (γ := Set γ) ((fun (a : α) ↦ f (a, p2)) '' (fun (d : Set (α × β)) ↦ Prod.fst '' d) d) x
⊢ Eq.{u_3 + 1} (α := Set γ)
    {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x}
    ((fun (a : α) ↦ f (a, p2)) '' (fun (d : Set (α × β)) ↦ Prod.fst '' d) d)

Tactic:
ext : 1
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
x_1 : γ
⊢ Membership.mem (γ := Set γ)
      {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x} x_1 ↔
    Membership.mem (γ := Set γ) ((fun (a : α) ↦ f (a, p2)) '' (fun (d : Set (α × β)) ↦ Prod.fst '' d) d) x_1

Tactic:
simp_all only [Subtype.exists, mem_image, Prod.exists,
    exists_and_right, exists_eq_right, exists_prop, mem_setOf_eq]

Premises used: Set.mem_image, Subtype.exists, exists_eq_right, Set.mem_setOf_eq, exists_and_right, exists_prop, Prod.exists
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous.{u_2, u_4} (β := γ) fun (b : β) ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous.{u_1, u_4} (β := γ) fun (a : α) ↦ f (a, b)
simp_rw : ScottContinuousOn univ f
⊢ ScottContinuous f

Tactic:
simp_rw [← scottContinuousOn_univ] at ⊢

Premises used: scottContinuousOn_univ
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous.{u_2, u_4} (β := γ) fun (b : β) ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous.{u_1, u_4} (β := γ) fun (a : α) ↦ f (a, b)
⊢ ScottContinuousOn univ f

Tactic:
.fromProd (fun a ↦ (h₁ a).scottContinuousOn) (fun b ↦ (h₂ b).scottContinuousOn)
    (fun a ↦ (h₁ a).monotone) (fun b ↦ (h₂ b).monotone)

Premises used: ScottContinuousOn.fromProd, ScottContinuous.scottContinuousOn, ScottContinuous.monotone
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous.{u_2, u_4} (β := γ) fun (b : β) ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous.{u_1, u_4} (β := γ) fun (a : α) ↦ f (a, b)
⊢ ScottContinuousOn univ f

Tactic:
exact .fromProd (fun a ↦ (h₁ a).scottContinuousOn) (fun b ↦ (h₂ b).scottContinuousOn)
    (fun a ↦ (h₁ a).monotone) (fun b ↦ (h₂ b).monotone)
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous (Prod.map f g)

Tactic:
.fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)

Premises used: ScottContinuous.fromProd
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
refine_1 :
  ∀ (a : α) (d : Set β) (hd₁ : d.Nonempty) (hd₂ : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d) (c : β) (hdc : IsLUB d c),
    IsLUB (α := α' × β') ((fun (b : β) ↦ Prod.map f g (a, b)) '' d) ((fun (b : β) ↦ Prod.map f g (a, b)) c)
refine_2 :
  ∀ (b : β) (d : Set α) (hd₁ : d.Nonempty) (hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (c : α) (hdc : IsLUB d c),
    IsLUB (α := α' × β') ((fun (a : α) ↦ Prod.map f g (a, b)) '' d) ((fun (a : α) ↦ Prod.map f g (a, b)) c)
⊢ ScottContinuous (Prod.map f g)

Tactic:
refine .fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
⊢ (fun (b : β) ↦ (f a, g b)) '' d = SProd.sprod (α := Set α') {f a} (g '' d)

Tactic:
aesop
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
⊢ (fun (b : β) ↦ (f a, g b)) '' d = SProd.sprod (α := Set α') {f a} (g '' d)

Tactic:
have e1 : (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d) := by aesop
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
e1 : (fun (b : β) ↦ (f a, g b)) '' d = SProd.sprod (α := Set α') {f a} (g '' d)
refine_1 : IsLUB (SProd.sprod (α := Set α') {f a} (g '' d)) (f a, g c)
⊢ IsLUB (α := α' × β') ((fun (b : β) ↦ Prod.map f g (a, b)) '' d) ((fun (b : β) ↦ Prod.map f g (a, b)) c)

Tactic:
simp_rw [Prod.map_apply, e1]

Premises used: Prod.map_apply
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
e1 : (fun (b : β) ↦ (f a, g b)) '' d = SProd.sprod (α := Set α') {f a} (g '' d)
⊢ IsLUB (SProd.sprod (α := Set α') {f a} (g '' d)) (f a, g c)

Tactic:
.prod (singleton_nonempty _) (hd₁.image _) isLUB_singleton (hg hd₁ hd₂ hdc)

Premises used: isLUB_singleton, Set.singleton_nonempty, IsLUB.prod, Set.Nonempty.image
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
e1 : (fun (b : β) ↦ (f a, g b)) '' d = SProd.sprod (α := Set α') {f a} (g '' d)
⊢ IsLUB (SProd.sprod (α := Set α') {f a} (g '' d)) (f a, g c)

Tactic:
exact .prod (singleton_nonempty _) (hd₁.image _) isLUB_singleton (hg hd₁ hd₂ hdc)
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
⊢ (fun (a : α) ↦ (f a, g b)) '' d = SProd.sprod (β := Set β') (f '' d) {g b}

Tactic:
aesop
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
⊢ (fun (a : α) ↦ (f a, g b)) '' d = SProd.sprod (β := Set β') (f '' d) {g b}

Tactic:
have e2 : ((fun a ↦ (f a, g b)) '' d) = (f '' d) ×ˢ {g b} := by aesop
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun (a : α) ↦ (f a, g b)) '' d = SProd.sprod (β := Set β') (f '' d) {g b}
refine_2 : IsLUB (SProd.sprod (β := Set β') (f '' d) {g b}) (f c, g b)
⊢ IsLUB (α := α' × β') ((fun (a : α) ↦ Prod.map f g (a, b)) '' d) ((fun (a : α) ↦ Prod.map f g (a, b)) c)

Tactic:
simp_rw [Prod.map_apply, e2]

Premises used: Prod.map_apply
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun (a : α) ↦ (f a, g b)) '' d = SProd.sprod (β := Set β') (f '' d) {g b}
⊢ IsLUB (SProd.sprod (β := Set β') (f '' d) {g b}) (f c, g b)

Tactic:
.prod (hd₁.image _) (singleton_nonempty _) (hf hd₁ hd₂ hdc) isLUB_singleton

Premises used: isLUB_singleton, Set.singleton_nonempty, IsLUB.prod, Set.Nonempty.image
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder α'
inst_3 : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun (a : α) ↦ (f a, g b)) '' d = SProd.sprod (β := Set β') (f '' d) {g b}
⊢ IsLUB (SProd.sprod (β := Set β') (f '' d) {g b}) (f c, g b)

Tactic:
exact .prod (hd₁.image _) (singleton_nonempty _) (hf hd₁ hd₂ hdc) isLUB_singleton
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D₁ D₂ : Set (Set α)
f : α → β
hD : D₁ ⊆ D₂
hf : ScottContinuousOn D₂ f
⊢ ScottContinuousOn D₁ f

Tactic:
fun _ hdD₁ hd₁ hd₂ _ hda => hf (hD hdD₁) hd₁ hd₂ hda

Premises used: ScottContinuousOn
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
⊢ Monotone f

Tactic:
fun a b hab =>
    (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair hab) ?_).1
      (mem_image_of_mem _ <| mem_insert _ _)

Premises used: Set.insert_nonempty, Monotone, And.left, Set.mem_image_of_mem, directedOn_pair, Set.mem_insert, Singleton.singleton
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
refine : ∀ (a b : α) (hab : a ≤ b), IsLUB {a, b} b
⊢ Monotone f

Tactic:
refine fun a b hab =>
    (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair hab) ?_).1
      (mem_image_of_mem _ <| mem_insert _ _)

Premises used: Set.insert_nonempty, And.left, Set.mem_image_of_mem, directedOn_pair, Set.mem_insert, Singleton.singleton
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
rw : IsLeast (Ici b) b
⊢ IsLUB {a, b} b

Tactic:
rw [IsLUB, upperBounds_insert, upperBounds_singleton,
    inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]

Premises used: Iff.mpr, Set.Ici_subset_Ici, IsLUB, Set.inter_eq_self_of_subset_right, upperBounds_insert, upperBounds_singleton
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b

Tactic:
isLeast_Ici

Premises used: isLeast_Ici
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b

Tactic:
exact isLeast_Ici

Premises used: isLeast_Ici
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
inst : Preorder α
D : Set (Set α)
⊢ ScottContinuousOn D _root_.id

Tactic:
simp [ScottContinuousOn]

Premises used: ScottContinuousOn
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set α)
x : β
s : Set α
h : s ∈ D
a : α
h_1 : a ∈ s
h_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a_1 : α
h_3 : IsLUB s a_1
simp : ∀ ⦃a : β⦄, (∀ a_2 ∈ s, x ≤ a) → x ≤ a
⊢ IsLUB (Function.const α x '' s) (Function.const α x a_1)

Tactic:
simp [IsLUB, IsLeast, upperBounds, lowerBounds]

Premises used: lowerBounds, upperBounds, IsLeast, IsLUB
-- Module: Mathlib.Order.ScottContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
D : Set (Set α)
x : β
s : Set α
h : s ∈ D
a : α
h_1 : a ∈ s
h_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a_1 : α
h_3 : IsLUB s a_1
⊢ ∀ ⦃a : β⦄, (∀ a_2 ∈ s, x ≤ a) → x ≤ a

Tactic:
grind
-- 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ ∀ (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D), Monotone f

Tactic:
have := hf.monotone
-- 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
this : ∀ (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D), Monotone f
simp : ∀ a ∈ d, ∀ a_2 ∈ d, ∃ a_4 ∈ d, f a ≤ f a_4 ∧ f a_2 ≤ f a_4
⊢ DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' d)

Tactic:
simp only [Monotone, DirectedOn, mem_image, exists_exists_and_eq_and, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂] at ⊢ this hd₃

Premises used: and_imp, Monotone, DirectedOn, Set.mem_image, forall_exists_index, exists_exists_and_eq_and, 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : ∀ x ∈ d, ∀ y ∈ d, ∃ z ∈ d, x ≤ z ∧ y ≤ z
a : α
ha : IsLUB d a
this : ∀ (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D) ⦃a b : α⦄, a ≤ b → f a ≤ f b
⊢ ∀ a ∈ d, ∀ a_2 ∈ d, ∃ a_4 ∈ d, f a ≤ f a_4 ∧ f a_2 ≤ f a_4

Tactic:
grind
-- 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' d)

Tactic:
have hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d) := by
    have := hf.monotone
    simp only [Monotone, DirectedOn, mem_image, exists_exists_and_eq_and, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂] at ⊢ this hd₃
    grind
-- 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' d)
rw : IsLUB (g '' f '' d) ((g ∘ f) a)
⊢ IsLUB (g ∘ f '' d) ((g ∘ f) a)

Tactic:
rw [Set.image_comp]

Premises used: Set.image_comp
-- 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' d)
⊢ Membership.mem (γ := Set β) ((fun (x : Set α) ↦ f '' x) d) (f (Exists.choose (p := Membership.mem d) hd₂))

Tactic:
grind
-- 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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun (x : Set α) ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' d)
⊢ IsLUB (g '' f '' d) ((g ∘ f) a)

Tactic:
exact hg (hD' hd₁) ⟨f hd₂.choose, by grind⟩ hd (hf hd₁ hd₂ hd₃ ha)

Premises used: Exists.intro, Exists.choose
-- 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
hg : ScottContinuousOn ((fun (x : Set α) ↦ f '' x) '' D) g
hf : ScottContinuousOn D f
⊢ ScottContinuousOn D (g ∘ f)

Tactic:
ScottContinuousOn.comp hD (Set.mapsTo_image (f '' ·) D) hg hf

Premises used: ScottContinuousOn.comp, Set.mapsTo_image, Set.image