awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
⊢ t₁ = t₂
have inr : t₁.root = t₂.root
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ Function.onFun Disjoint SetLike.coe t₁ t₂
have rw : ∀ ⦃a : (↑t : Type u_2)⦄, a ∈ (↑t₁ : Set (↑t : Type u_2)) → a ∉ (↑t₂ : Set (↑t : Type u_2))
Tactic: rw [Function.onFun_apply, Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : (↑t : Type u_2)
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
⊢ False
have h₁ : a = ⊥
Tactic: rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h
Cleared hypotheses: h, ha, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : (↑t : Type u_2)
h : a = ⊥
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
⊢ False
have ha₁ : ⊥ ∈ (↑t₁ : Set (↑t : Type u_2))
Tactic: subst h
Cleared hypotheses: a, h, ha, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : (↑t : Type u_2)
h : a = ⊥
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
ha₁ : ⊥ ∈ (↑t₁ : Set (↑t : Type u_2))
⊢ False
have hb₁ : ⊥ ∈ (↑t₂ : Set (↑t : Type u_2))
Tactic: subst h
Cleared hypotheses: a, h, ha, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
ha : ⊥ ∈ (↑t₁ : Set (↑t : Type u_2))
hb : ⊥ ∈ (↑t₂ : Set (↑t : Type u_2))
⊢ False
have ha₁ : t₁.root = ⊥
Tactic: simp only [SetLike.mem_coe, SubRootedTree.bot_mem_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
a : WithBot α
⊢ a.succ = ⊥ ↔ a = ⊥
have bot : Eq.{u_2 + 1} (α := α) (succ ⊥) ⊥ ↔ Eq.{u_2 + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
a : WithBot α
bot : Eq.{u_2 + 1} (α := α) (succ ⊥) ⊥ ↔ Eq.{u_2 + 1} (α := WithBot α) ⊥ ⊥
⊢ a.succ = ⊥ ↔ a = ⊥
have coe : ∀ (a : α), (↑a : WithBot α).succ = ⊥ ↔ (↑a : WithBot α) = ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : PredOrder α
a : WithTop α
⊢ a.pred = ⊤ ↔ a = ⊤
have top : Eq.{u_2 + 1} (α := α) (pred ⊤) ⊤ ↔ Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_2
inst : Nontrivial α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : PredOrder α
a : WithTop α
top : Eq.{u_2 + 1} (α := α) (pred ⊤) ⊤ ↔ Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
⊢ a.pred = ⊤ ↔ a = ⊤
have coe : ∀ (a : α), (↑a : WithTop α).pred = ⊤ ↔ (↑a : WithTop α) = ⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s)
    ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have rw : Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊔ b) : β)
Tactic: rw [← map_sup]
-- Lean 4 proof step from Mathlib.Order.SupClosed (hypothesis)
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s
have ha' : ∀ b ∈ s, a ≤ b
Tactic: have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s : Set α
inst_2 : FunLike F α β
inst_3 : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s)
    ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have rw : Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) (a ⊓ b) : β)
Tactic: rw [← map_inf]
-- Lean 4 proof step from Mathlib.Order.SupClosed (hypothesis)
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s
have ha' : ∀ b ∈ s, b ≤ a
Tactic: have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ max a b ∈ s
have inl : a ≤ b → max a b ∈ s
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : a ≤ b → max a b ∈ s
⊢ max a b ∈ s
have inr : b ≤ a → max a b ∈ s
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ min a b ∈ s
have inl : a ≤ b → min a b ∈ s
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : a ≤ b → min a b ∈ s
⊢ min a b ∈ s
have inr : b ≤ a → min a b ∈ s
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α)) s)
    (t.sup' ht id ⊔ u.sup' hu id)
have refine : (↑(t ∪ u) : Set α) ⊆ s
Tactic: refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ (↑(t ∪ u) : Set α) ⊆ s
have rw : (↑t : Set α) ∪ (↑u : Set α) ⊆ s
Tactic: rw [coe_union]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ (x : Set α),
    SupClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        x)
have rintro : ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
  (hus : (↑u : Set α) ⊆ s),
  Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α)) s)
    (t.sup' ht id ⊔ u.sup' hu id)
Tactic: classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s t : Set α
a b : α
rintro :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s),
    Membership.mem (γ := Set α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        s)
      (t.sup' ht id ⊔ u.sup' hu id)
⊢ ∀ (x : Set α),
    SupClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        x)
have rintro₁ : ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
  (hus : (↑u : Set α) ⊆ s), (↑(t ∪ u) : Set α) ⊆ s
Tactic: classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s t : Set α
a b : α
rintro :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s),
    Membership.mem (γ := Set α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        s)
      (t.sup' ht id ⊔ u.sup' hu id)
rintro₁ :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s), (↑(t ∪ u) : Set α) ⊆ s
⊢ ∀ (x : Set α),
    SupClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.sup' ht id = a} : Set α))
        x)
have rintro₂ : ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
  (hus : (↑u : Set α) ⊆ s), (↑t : Set α) ∪ (↑u : Set α) ⊆ s
Tactic: classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Set α
hs : s.Finite
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) s)
have lift : ∀ (s : Finset α), Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))
have refine : (supClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
  (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' sorry id)
        {t ∈ s.powerset | t.Nonempty}.attach) :
    Set α)
Tactic: refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
⊢ t.sup' ht id ∈
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
have simp : ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.sup' sorry fun (x : α) ↦ x) (t.sup' sorry fun (x : α) ↦ x)
Tactic: simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))
have refine : (supClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
  (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' sorry id)
        {t ∈ s.powerset | t.Nonempty}.attach) :
    Set α)
Tactic: classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
refine :
  (supClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))
have refine₁ : ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
  t.sup' ht id ∈
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' sorry id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
Tactic: classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
s : Finset α
refine :
  (supClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
refine₁ :
  ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
    t.sup' ht id ∈
      (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).sup' ⋯ id)
            {t ∈ s.powerset | t.Nonempty}.attach) :
        Set α)
⊢ Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) (↑s : Set α))
have refine₂ : ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
  ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.sup' sorry fun (x : α) ↦ x) (t.sup' sorry fun (x : α) ↦ x)
Tactic: classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
v : Finset β
hv : v.Nonempty
hvt : (↑v : Set β) ⊆ t
⊢ Membership.mem (γ := Set (α × β)) ((supClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.sup' hu id, v.sup' hv id)
have refine_1 : (↑(u ×ˢ v) : Set (α × β)) ⊆ s ×ˢ t
Tactic: refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
v : Finset β
hv : v.Nonempty
hvt : (↑v : Set β) ⊆ t
refine_1 : (↑(u ×ˢ v) : Set (α × β)) ⊆ s ×ˢ t
⊢ Membership.mem (γ := Set (α × β)) ((supClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.sup' hu id, v.sup' hv id)
have refine_2 : (u ×ˢ v).sup' sorry id = (u.sup' hu id, v.sup' hv id)
Tactic: refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α)) s)
    (t.inf' ht id ⊓ u.inf' hu id)
have refine : (↑(t ∪ u) : Set α) ⊆ s
Tactic: refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s_1 t_1 : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ (↑(t ∪ u) : Set α) ⊆ s
have rw : (↑t : Set α) ∪ (↑u : Set α) ⊆ s
Tactic: rw [coe_union]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s t : Set α
a b : α
⊢ ∀ (x : Set α),
    InfClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        x)
have rintro : ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
  (hus : (↑u : Set α) ⊆ s),
  Membership.mem (γ := Set α)
    ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α)) s)
    (t.inf' ht id ⊓ u.inf' hu id)
Tactic: classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s t : Set α
a b : α
rintro :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s),
    Membership.mem (γ := Set α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        s)
      (t.inf' ht id ⊓ u.inf' hu id)
⊢ ∀ (x : Set α),
    InfClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        x)
have rintro₁ : ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
  (hus : (↑u : Set α) ⊆ s), (↑(t ∪ u) : Set α) ⊆ s
Tactic: classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
s t : Set α
a b : α
rintro :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s),
    Membership.mem (γ := Set α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        s)
      (t.inf' ht id ⊓ u.inf' hu id)
rintro₁ :
  ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
    (hus : (↑u : Set α) ⊆ s), (↑(t ∪ u) : Set α) ⊆ s
⊢ ∀ (x : Set α),
    InfClosed.{u_3} (α := α)
      ((fun (s : Set α) ↦ ({a : α | ∃ (t : Finset α) (ht : t.Nonempty), (↑t : Set α) ⊆ s ∧ t.inf' ht id = a} : Set α))
        x)
have rintro₂ : ∀ (s : Set α) (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ s) (u : Finset α) (hu : u.Nonempty)
  (hus : (↑u : Set α) ⊆ s), (↑t : Set α) ∪ (↑u : Set α) ⊆ s
Tactic: classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Set α
hs : s.Finite
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) s)
have lift : ∀ (s : Finset α), Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Finset α
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))
have refine : (infClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
  (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' sorry id)
        {t ∈ s.powerset | t.Nonempty}.attach) :
    Set α)
Tactic: refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
⊢ t.inf' ht id ∈
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
have simp : ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.inf' sorry fun (x : α) ↦ x) (t.inf' sorry fun (x : α) ↦ x)
Tactic: simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Finset α
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))
have refine : (infClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
  (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' sorry id)
        {t ∈ s.powerset | t.Nonempty}.attach) :
    Set α)
Tactic: classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : SemilatticeInf α
s : Finset α
refine :
  (infClosure : (a : Set α) → Set α) (↑s : Set α) ⊆
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : Set α))
have refine₁ : ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
  t.inf' ht id ∈
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' sorry id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)
Tactic: classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩