awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s.OrdConnected ↔ (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s
have refine : ∀ (h : (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s), s.OrdConnected
Tactic: refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s
⊢ s.OrdConnected
have rw : ((↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α)).OrdConnected
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint (↑(upperClosure s) : Set α) t ↔ Disjoint s t
have refine : Disjoint s t → Disjoint (↑(upperClosure s) : Set α) t
Tactic: refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint s t → Disjoint (↑(upperClosure s) : Set α) t
have simp : (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t
Tactic: simp only [disjoint_left, SetLike.mem_coe, mem_upperClosure, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x ↔ x ∈ s
have refine_1 : ∀ (h : Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x), x ∈ s
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
refine_1 : ∀ (h : Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x), x ∈ s
⊢ Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x ↔ x ∈ s
have refine_2 : ∀ (h : x ∈ s) (b : α), (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) b → ∀ (hbx : b ≤ x) (a : α) (has : a ∈ s) (hab : a ≤ b), x ≤ b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x
⊢ x ∈ s
have refine_1 : ∀ (a : α) (has : a ∈ s) (hax : a ≤ x), x ∈ s
Tactic: obtain ⟨a, has, hax⟩ := h.prop
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ s.erase a = s ↔ a ∉ s
have rw : s.sdiff {a} = s ↔ a ∉ s
Tactic: rw [← sdiff_singleton]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s
have refine : ∀ (a : α) (ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a),
  Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
Tactic: refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
have inl : ∀ (hat : a ∈ t),
  Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
Tactic: obtain hat | hat := em (a ∈ t)
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
inl :
  ∀ (hat : a ∈ t),
    Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
have inr : ∀ (hat : a ∉ t),
  Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
Tactic: obtain hat | hat := em (a ∈ t)
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∉ t
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
have inr : a ∉ (↑(lowerClosure t) : Set α)
Tactic: refine subset_union_left ⟨ha, ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ upperClosure t ⊓ s.sdiff t = s
have rw : s.sdiff t ⊓ upperClosure t = s
Tactic: rw [inf_comm, sdiff_inf_upperClosure hts hst]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
rw : s.sdiff t ⊓ upperClosure t = s
⊢ upperClosure t ⊓ s.sdiff t = s
have rw₁ : s = s
Tactic: rw [inf_comm, sdiff_inf_upperClosure hts hst]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s
have hts : {a} ⊆ (↑s : Set α)
Tactic: rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
hts : {a} ⊆ (↑s : Set α)
⊢ s.erase a ⊓ Ici a = s
have hst : ∀ b ∈ s, ∀ (c : α), Membership.mem (γ := Set α) {a} c → b ≤ c → Membership.mem (γ := Set α) {a} b
Tactic: rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ Ici a ⊓ s.erase a = s
have rw : s.erase a ⊓ Ici a = s
Tactic: rw [inf_comm, erase_inf_Ici ha has]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
rw : s.erase a ⊓ Ici a = s
⊢ Ici a ⊓ s.erase a = s
have rw₁ : s = s
Tactic: rw [inf_comm, erase_inf_Ici ha has]
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
s t : UpperSet α
h : s.carrier = t.carrier
⊢ s = t
have mk : ∀ (carrier : Set α) (upper' : IsUpperSet carrier)
  (h : { carrier := carrier, upper' := upper' : UpperSet α }.carrier = t.carrier),
  { carrier := carrier, upper' := upper' : UpperSet α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
t : UpperSet α
carrier : Set α
upper' : IsUpperSet carrier
h : { carrier := carrier, upper' := upper' : UpperSet α }.carrier = t.carrier
⊢ { carrier := carrier, upper' := upper' : UpperSet α } = t
have mk : ∀ (carrier_1 : Set α) (upper'_1 : IsUpperSet carrier_1)
  (h :
    { carrier := carrier, upper' := upper' : UpperSet α }.carrier =
      { carrier := carrier_1, upper' := upper'_1 : UpperSet α }.carrier),
  { carrier := carrier, upper' := upper' : UpperSet α } = { carrier := carrier_1, upper' := upper'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
⊢ Membership.mem (γ := UpperSet α) (⨆ (i : ι), f i) a ↔ ∀ (i : ι), a ∈ f i
have rw : Membership.mem (γ := Set α) (⋂ (i : ι), (↑(f i) : Set α)) a ↔ ∀ (i : ι), a ∈ f i
Tactic: rw [← SetLike.mem_coe, coe_iSup]
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
⊢ Membership.mem (γ := UpperSet α) (⨅ (i : ι), f i) a ↔ ∃ (i : ι), a ∈ f i
have rw : Membership.mem (γ := Set α) (⋃ (i : ι), (↑(f i) : Set α)) a ↔ ∃ (i : ι), a ∈ f i
Tactic: rw [← SetLike.mem_coe, coe_iInf]
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
⊢ (map f).symm = map f.symm
have h : ∀ (x : UpperSet β) (x_1 : α),
  x_1 ∈ (↑(((map f).symm : (a : UpperSet β) → UpperSet α) x : UpperSet α) : Set α) ↔
    x_1 ∈ (↑((map f.symm : (a : UpperSet β) → UpperSet α) x : UpperSet α) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ Membership.mem (γ := UpperSet β) ((map f : (a : UpperSet α) → UpperSet β) s : UpperSet β) b ↔
    Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)
have rw : Membership.mem (γ := UpperSet β) (((map f.symm).symm : (a : UpperSet α) → UpperSet β) s : UpperSet β) b ↔
  Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)
Tactic: rw [← f.symm_symm, ← symm_map, f.symm_symm]
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq (α := UpperSet α ≃o UpperSet α) (map (OrderIso.refl α)) (OrderIso.refl (UpperSet α))
have h : ∀ (x : UpperSet α) (x_1 : α),
  x_1 ∈ (↑((map (OrderIso.refl α) : (a : UpperSet α) → UpperSet α) x : UpperSet α) : Set α) ↔
    x_1 ∈ (↑((OrderIso.refl (UpperSet α) : (a : UpperSet α) → UpperSet α) x : UpperSet α) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.CompleteLattice (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
⊢ Eq.{u_3 + 1} (α := UpperSet γ)
    ((map g : (a : UpperSet β) → UpperSet γ) ((map f : (a : UpperSet α) → UpperSet β) s) : UpperSet γ)
    ((map (f.trans g) : (a : UpperSet α) → UpperSet γ) s : UpperSet γ)
have a : ∀ (x : γ),
  x ∈ (↑((map g : (a : UpperSet β) → UpperSet γ) ((map f : (a : UpperSet α) → UpperSet β) s) : UpperSet γ) : Set γ) ↔
    x ∈ (↑((map (f.trans g) : (a : UpperSet α) → UpperSet γ) s : UpperSet γ) : Set γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Fibration (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LE α
inst_1 : LE β
hf : Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
⊢ y' ∈ f '' s
have obtain : ∀ (y : α) (e' : y ≤ x) (e : f y ≤ f x), f y ∈ f '' s
Tactic: obtain ⟨y, e', rfl⟩ := hf e
Cleared hypotheses: y', e
-- Lean 4 proof step from Mathlib.Order.UpperLower.LocallyFinite (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderTop α
hs : s.Finite
⊢ (↑(upperClosure s) : Set α).Finite
have rw : Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Ici a)
Tactic: rw [coe_upperClosure]
-- Lean 4 proof step from Mathlib.Order.UpperLower.LocallyFinite (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderBot α
hs : s.Finite
⊢ (↑(lowerClosure s) : Set α).Finite
have rw : Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Iic a)
Tactic: rw [coe_lowerClosure]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Principal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
a : α
⊢ Eq.{u_2 + 1} (α := UpperSet β) ((map f : (a : UpperSet α) → UpperSet β) (Ici a) : UpperSet β)
    (Ici ((f : (a : α) → β) a) : UpperSet β)
have a₁ : ∀ (x : β),
  x ∈ (↑((map f : (a : UpperSet α) → UpperSet β) (Ici a) : UpperSet β) : Set β) ↔
    x ∈ (↑(Ici ((f : (a : α) → β) a) : UpperSet β) : Set β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Principal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
a : α
⊢ Eq.{u_2 + 1} (α := UpperSet β) ((map f : (a : UpperSet α) → UpperSet β) (Ioi a) : UpperSet β)
    (Ioi ((f : (a : α) → β) a) : UpperSet β)
have a₁ : ∀ (x : β),
  x ∈ (↑((map f : (a : UpperSet α) → UpperSet β) (Ioi a) : UpperSet β) : Set β) ↔
    x ∈ (↑(Ioi ((f : (a : α) → β) a) : UpperSet β) : Set β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
have simp_rw : (↑(s ×ˢ t) : Set (α × β)) = (↑⊤ : Set (α × β)) ↔ (↑s : Set α) = (↑⊤ : Set α) ∨ (↑t : Set β) = (↑⊤ : Set β)
Tactic: simp_rw [SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
have simp_rw : s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
Tactic: simp_rw [codisjoint_iff, prod_sup_prod, prod_eq_top]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
simp_rw : s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
have simp_rw₁ : (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂) = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
Tactic: simp_rw [codisjoint_iff, prod_sup_prod, prod_eq_top]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
have simp_rw : (↑(s ×ˢ t) : Set (α × β)) = (↑⊥ : Set (α × β)) ↔ (↑s : Set α) = (↑⊥ : Set α) ∨ (↑t : Set β) = (↑⊥ : Set β)
Tactic: simp_rw [SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
have simp_rw : s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = ⊥ ↔ s₁ ⊓ s₂ = ⊥ ∨ t₁ ⊓ t₂ = ⊥
Tactic: simp_rw [disjoint_iff, prod_inf_prod, prod_eq_bot]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
simp_rw : s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = ⊥ ↔ s₁ ⊓ s₂ = ⊥ ∨ t₁ ⊓ t₂ = ⊥
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
have simp_rw₁ : (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂) = ⊥ ↔ s₁ ⊓ s₂ = ⊥ ∨ t₁ ⊓ t₂ = ⊥
Tactic: simp_rw [disjoint_iff, prod_inf_prod, prod_eq_bot]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
⊢ upperClosure (s ×ˢ t) = SProd.sprod (α := UpperSet α) (β := UpperSet β) (upperClosure s) (upperClosure t)
have a : ∀ (x : α × β),
  x ∈ (↑(upperClosure (s ×ˢ t)) : Set (α × β)) ↔
    x ∈ (↑(SProd.sprod (α := UpperSet α) (β := UpperSet β) (upperClosure s) (upperClosure t)) : Set (α × β))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
⊢ lowerClosure (s ×ˢ t) = SProd.sprod (α := LowerSet α) (β := LowerSet β) (lowerClosure s) (lowerClosure t)
have a : ∀ (x : α × β),
  x ∈ (↑(lowerClosure (s ×ˢ t)) : Set (α × β)) ↔
    x ∈ (↑(SProd.sprod (α := LowerSet α) (β := LowerSet β) (lowerClosure s) (lowerClosure t)) : Set (α × β))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
have inl : ∀ (h : b ∈ s), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
Tactic: cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
Cleared hypotheses: mb
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
mb : b ∈ s ∪ t
inl : ∀ (h : b ∈ s), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
have inr : ∀ (h : b ∈ t), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
Tactic: cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
Cleared hypotheses: mb
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
have inl : ∀ (h : b ∈ s), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
Tactic: cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
Cleared hypotheses: mb
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
mb : b ∈ s ∪ t
inl : ∀ (h : b ∈ s), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
have inr : ∀ (h : b ∈ t), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
Tactic: cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
Cleared hypotheses: mb
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t
have simp_all : ∀ (hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s)
  (ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ t),
  b ∈ s ∩ t → ∀ (bs : b ∈ s) (bt : b ∈ t) ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t
Tactic: simp_all only [IsRelUpperSet, true_and]
Cleared hypotheses: hs, ht, h, bs, bt
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t
have simp_all : ∀ (hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s)
  (ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ t),
  b ∈ s ∩ t → ∀ (bs : b ∈ s) (bt : b ∈ t) ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t
Tactic: simp_all only [IsRelLowerSet, true_and]
Cleared hypotheses: hs, ht, h, bs, bt
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S
have obtain : ∀ (s₀ : Set α) (ms₀ : s₀ ∈ S), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S
Tactic: obtain ⟨s₀, ms₀⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S
have obtain : ∀ (s₀ : Set α) (ms₀ : s₀ ∈ S), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S
Tactic: obtain ⟨s₀, ms₀⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
⊢ IsUpperSet s ↔ IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
have refine_1 : ∀ (h : IsUpperSet s) (a : α) (x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s),
  P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
Tactic: refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
refine_1 :
  ∀ (h : IsUpperSet s) (a : α) (x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s),
    P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ IsUpperSet s ↔ IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
have refine_2 : ∀ (h : IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P) (a b : { x : α // P x }) (x : a ≤ b) (y : a ∈ s),
  b ∈ s
Tactic: refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsUpperSet s
a : α
x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
have refine_1 : ∀ (a : { x : α // P x }) (ma : a ∈ s),
  P (↑a : α) ∧ ∀ ⦃b : α⦄, (↑a : α) ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
Tactic: obtain ⟨a, ma, rfl⟩ := x
Cleared hypotheses: a, x
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (hypothesis)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : a ≤ b
y : a ∈ s
⊢ b ∈ s
have ma : (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
Tactic: have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
⊢ IsLowerSet s ↔ IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
have refine_1 : ∀ (h : IsLowerSet s) (a : α) (x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s),
  P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
Tactic: refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
refine_1 :
  ∀ (h : IsLowerSet s) (a : α) (x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s),
    P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ IsLowerSet s ↔ IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
have refine_2 : ∀ (h : IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P) (a b : { x : α // P x }) (x : b ≤ a) (y : a ∈ s),
  b ∈ s
Tactic: refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsLowerSet s
a : α
x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
have refine_1 : ∀ (a : { x : α // P x }) (ma : a ∈ s),
  P (↑a : α) ∧ ∀ ⦃b : α⦄, b ≤ (↑a : α) → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
Tactic: obtain ⟨a, ma, rfl⟩ := x
Cleared hypotheses: a, x
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (hypothesis)
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : b ≤ a
y : a ∈ s
⊢ b ∈ s
have ma : (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
Tactic: have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s_1 t_1 : Set α
a b : α
P : α → Prop
inst : LE α
s t : RelUpperSet P
h : s.carrier (P := P) = t.carrier (P := P)
⊢ s = t
have mk : ∀ (carrier : Set α) (isRelUpperSet' : IsRelUpperSet carrier P)
  (h : (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) = t.carrier (P := P)),
  RelUpperSet.mk (P := P) carrier isRelUpperSet' = t
Tactic: cases s
Cleared hypotheses: s, h