awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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)
a : (↑(Prod.fst '' d) : Type u_1)
⊢ IsLUB (f '' SProd.sprod (α := Set α) {(↑a : α)} (Prod.snd '' d)) ((fun (b : β) ↦ f ((↑a : α), b)) (p1, p2).2)
have rw : IsLUB.{u_3} (α := γ) ((fun (x : β) ↦ f ((↑a : α), x)) '' Prod.snd '' d) ((fun (b : β) ↦ f ((↑a : α), b)) (p1, p2).2)
Tactic: rw [singleton_prod, image_image f (fun b ↦ (a, b))]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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 (f '' d) (f (p1, p2))
have rw : IsLUB {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x} (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]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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 {x : γ | ∃ (y : (↑(Prod.fst '' d) : Type u_1)), (fun (b : β) ↦ f ((↑y : α), b)) (p1, p2).2 = x} (f (p1, p2))
have 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)
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)
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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)
⊢ 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)
have 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
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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)
⊢ ScottContinuous f
have simp_rw : ScottContinuousOn univ f
Tactic: simp_rw [← scottContinuousOn_univ] at ⊢
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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)
have 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)
Tactic: refine .fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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)
⊢ ScottContinuous (Prod.map f g)
have 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)
Tactic: refine .fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (hypothesis)
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
⊢ IsLUB (α := α' × β') ((fun (b : β) ↦ Prod.map f g (a, b)) '' d) ((fun (b : β) ↦ Prod.map f g (a, b)) c)
have e1 : (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
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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 (α := α' × β') ((fun (b : β) ↦ Prod.map f g (a, b)) '' d) ((fun (b : β) ↦ Prod.map f g (a, b)) c)
have refine_1 : IsLUB (SProd.sprod (α := Set α') {f a} (g '' d)) (f a, g c)
Tactic: simp_rw [Prod.map_apply, e1]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (hypothesis)
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
⊢ IsLUB (α := α' × β') ((fun (a : α) ↦ Prod.map f g (a, b)) '' d) ((fun (a : α) ↦ Prod.map f g (a, b)) c)
have e2 : (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
-- Lean 4 proof step from Mathlib.Order.ScottContinuity.Prod (goal)
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 (α := α' × β') ((fun (a : α) ↦ Prod.map f g (a, b)) '' d) ((fun (a : α) ↦ Prod.map f g (a, b)) c)
have refine_2 : IsLUB (SProd.sprod (β := Set β') (f '' d) {g b}) (f c, g b)
Tactic: simp_rw [Prod.map_apply, e2]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
have refine : ∀ (a b : α) (hab : a ≤ b), IsLUB {a, b} b
Tactic: refine fun a b hab =>
    (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair hab) ?_).1
      (mem_image_of_mem _ <| mem_insert _ _)
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ IsLUB {a, b} b
have rw : IsLeast (Ici b) b
Tactic: rw [IsLUB, upperBounds_insert, upperBounds_singleton,
    inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ IsLUB (Function.const α x '' s) (Function.const α x a_1)
have simp : ∀ ⦃a : β⦄, (∀ a_2 ∈ s, x ≤ a) → x ≤ a
Tactic: simp [IsLUB, IsLeast, upperBounds, lowerBounds]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
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)
have this : ∀ (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D), Monotone f
Tactic: have := hf.monotone
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' d)
have simp : ∀ a ∈ d, ∀ a_2 ∈ d, ∃ a_4 ∈ d, f a ≤ f a_4 ∧ f a_2 ≤ f a_4
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₃
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
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
⊢ IsLUB (g ∘ f '' d) ((g ∘ f) a)
have hd : 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
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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)
have rw : IsLUB (g '' f '' d) ((g ∘ f) a)
Tactic: rw [Set.image_comp]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ 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)
have left : ∀ a_1 ∈ d, f a_1 ≤ f a ∧ g a_1 ≤ g a
Tactic: simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
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₂)
⊢ (fun (x : α) ↦ (f x, g x)) a ≤ (p₁, p₂)
have hp₁ : ∀ 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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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₂
⊢ (fun (x : α) ↦ (f x, g x)) a ≤ (p₁, p₂)
have right : ((fun (x : α) ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ (fun (x : α) ↦ (f x, g x)) a ≤ (p₁, p₂)
have right₁ : ((fun (x : α) ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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₂
⊢ ((fun (x : α) ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1
have right : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x} (p₁, p₂).1
Tactic: rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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₂
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x} (p₁, p₂).1
have right : ∀ a ∈ d, f a ≤ p₁
Tactic: simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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₂
⊢ ((fun (x : α) ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2
have right : Membership.mem (γ := Set γ) {x : γ | ∀ ⦃a : γ⦄, a ∈ g '' d → a ≤ x} (p₁, p₂).2
Tactic: rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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₂
⊢ Membership.mem (γ := Set γ) {x : γ | ∀ ⦃a : γ⦄, a ∈ g '' d → a ≤ x} (p₁, p₂).2
have right : ∀ a ∈ d, g a ≤ p₂
Tactic: simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
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
have ha₁ : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
Tactic: simp only [isLUB_prod] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
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.snd '' d) a.2
have ha₁ : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
Tactic: simp only [isLUB_prod] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : β
⊢ ScottContinuous (Function.const α x)
have simp_rw : ScottContinuousOn univ (Function.const α x)
Tactic: simp_rw [← scottContinuousOn_univ, ScottContinuousOn.const]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ ScottContinuous (g ∘ f)
have rw : ∀ (hf : ScottContinuousOn univ f) (hg : ScottContinuousOn univ g), ScottContinuousOn univ (g ∘ f)
Tactic: rw [← scottContinuousOn_univ] at ⊢ hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
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
⊢ ScottContinuous (β := β × γ) fun (x : α) ↦ (f x, g x)
have rw : ∀ (hf : ScottContinuousOn univ f) (hg : ScottContinuousOn univ g),
  ScottContinuousOn (β := β × γ) univ fun (x : α) ↦ (f x, g x)
Tactic: rw [← scottContinuousOn_univ] at ⊢ hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ ScottContinuous (α := α × β) Prod.fst
have simp_rw : ScottContinuousOn (α := α × β) univ Prod.fst
Tactic: simp_rw [← scottContinuousOn_univ, ScottContinuousOn.fst]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ ScottContinuous (α := α × β) Prod.snd
have simp_rw : ScottContinuousOn (α := α × β) univ Prod.snd
Tactic: simp_rw [← scottContinuousOn_univ, ScottContinuousOn.snd]