awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α)
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' ⋯ 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 α)),
  ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.inf' sorry fun (x : α) ↦ x) (t.inf' sorry fun (x : α) ↦ x)
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
β : Type u_4
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
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 (α × β)) ((infClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.inf' hu id, v.inf' 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 : SemilatticeInf α
inst_1 : SemilatticeInf β
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 (α × β)) ((infClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.inf' hu id, v.inf' hv id)
have refine_2 : (u ×ˢ v).inf' sorry id = (u.inf' hu id, v.inf' hv id)
Tactic: refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : Lattice α
s : Set α
p : (a : α) → Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a → Prop
mem : ∀ (a : α) (has : a ∈ s), p a ⋯
sup :
  ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
    (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
    p a has → p b hbs → p (a ⊔ b) ⋯
inf :
  ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
    (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
    p a has → p b hbs → p (a ⊓ b) ⋯
a : α
has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a
⊢ p a has
have have : ∀
  (h :
    IsSublattice.{u_3} (α := α)
      {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has}),
  p a has
Tactic: have h : IsSublattice { a : α | ∃ has : a ∈ latticeClosure s, p a has } := {
    supClosed := fun a ⟨has, hpa⟩ b ⟨hbs, hpb⟩ =>
      ⟨isSublattice_latticeClosure.supClosed has hbs, sup a has b hbs hpa hpb⟩
    infClosed := fun a ⟨has, hpa⟩ b ⟨hbs, hpb⟩ =>
      ⟨isSublattice_latticeClosure.infClosed has hbs, inf a has b hbs hpa hpb⟩ }
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : Lattice α
s : Set α
p : (a : α) → Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a → Prop
mem : ∀ (a : α) (has : a ∈ s), p a ⋯
sup :
  ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
    (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
    p a has → p b hbs → p (a ⊔ b) ⋯
inf :
  ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
    (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
    p a has → p b hbs → p (a ⊓ b) ⋯
a : α
has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a
h :
  IsSublattice.{u_3} (α := α)
    {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has}
⊢ p a has
have refine : ∀ (a : α) (ha : a ∈ s),
  Membership.mem (γ := Set α)
    {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has} a
Tactic: refine (latticeClosure_min (fun a ha ↦ ?_) h has).choose_spec
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ f '' (latticeClosure : (a : Set α) → Set α) s = (latticeClosure : (a : Set β) → Set β) (f '' s)
have simp : (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) ∧
  (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
Tactic: simp only [subset_antisymm_iff, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) ∧
    (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
have left : (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
left : (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
⊢ (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) ∧
    (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
have right : (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
have left : ∀ (a : α) (has : a ∈ s), a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
Tactic: apply latticeClosure_sup_inf_induction
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
left : ∀ (a : α) (has : a ∈ s), a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
⊢ (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
have left₁ : ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
  (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
  a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) →
    b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) →
      a ⊔ b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
Tactic: apply latticeClosure_sup_inf_induction
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
left : ∀ (a : α) (has : a ∈ s), a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
left₁ :
  ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
    (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
    a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) →
      b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) →
        a ⊔ b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
⊢ (latticeClosure : (a : Set α) → Set α) s ⊆ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
have left₂ : ∀ (a : α) (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a) (b : α)
  (hbs : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b),
  a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) →
    b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s) →
      a ⊓ b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
Tactic: apply latticeClosure_sup_inf_induction
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
have right : ∀ (a : β) (has : a ∈ f '' s), a ∈ f '' (latticeClosure : (a : Set α) → Set α) s
Tactic: apply latticeClosure_sup_inf_induction
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
right : ∀ (a : β) (has : a ∈ f '' s), a ∈ f '' (latticeClosure : (a : Set α) → Set α) s
⊢ (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
have right₁ : ∀ (a : β) (has : Membership.mem (γ := Set β) ((latticeClosure : (a : Set β) → Set β) (f '' s) : Set β) a) (b : β)
  (hbs : Membership.mem (γ := Set β) ((latticeClosure : (a : Set β) → Set β) (f '' s) : Set β) b),
  a ∈ f '' (latticeClosure : (a : Set α) → Set α) s →
    b ∈ f '' (latticeClosure : (a : Set α) → Set α) s → a ⊔ b ∈ f '' (latticeClosure : (a : Set α) → Set α) s
Tactic: apply latticeClosure_sup_inf_induction
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Lattice α
inst_1 : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
right : ∀ (a : β) (has : a ∈ f '' s), a ∈ f '' (latticeClosure : (a : Set α) → Set α) s
right₁ :
  ∀ (a : β) (has : Membership.mem (γ := Set β) ((latticeClosure : (a : Set β) → Set β) (f '' s) : Set β) a) (b : β)
    (hbs : Membership.mem (γ := Set β) ((latticeClosure : (a : Set β) → Set β) (f '' s) : Set β) b),
    a ∈ f '' (latticeClosure : (a : Set α) → Set α) s →
      b ∈ f '' (latticeClosure : (a : Set α) → Set α) s → a ⊔ b ∈ f '' (latticeClosure : (a : Set α) → Set α) s
⊢ (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) s
have right₂ : ∀ (a : β) (has : Membership.mem (γ := Set β) ((latticeClosure : (a : Set β) → Set β) (f '' s) : Set β) a) (b : β)
  (hbs : Membership.mem (γ := Set β) ((latticeClosure : (a : Set β) → Set β) (f '' s) : Set β) b),
  a ∈ f '' (latticeClosure : (a : Set α) → Set α) s →
    b ∈ f '' (latticeClosure : (a : Set α) → Set α) s → a ⊓ b ∈ f '' (latticeClosure : (a : Set α) → Set α) s
Tactic: apply latticeClosure_sup_inf_induction
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ Eq.{u_3 + 1} (α := Set αᵒᵈ)
    (Set.preimage (β := α) (⇑ofDual : (a : αᵒᵈ) → α) ((latticeClosure : (a : Set α) → Set α) s))
    ((latticeClosure : (a : Set αᵒᵈ) → Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s))
have h : ∀ (x : αᵒᵈ),
  Membership.mem (γ := Set αᵒᵈ)
      (Set.preimage (β := α) (⇑ofDual : (a : αᵒᵈ) → α) ((latticeClosure : (a : Set α) → Set α) s)) x ↔
    Membership.mem (γ := Set αᵒᵈ)
      ((latticeClosure : (a : Set αᵒᵈ) → Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) : Set αᵒᵈ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α) (t.inf' ht id ⊔ u.inf' hu id)
have rw : Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α)
  ((t ×ˢ u).inf' sorry fun (i : α × α) ↦ id i.1 ⊔ id i.2)
Tactic: rw [inf'_sup_inf']
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ s
u : Finset α
hu : u.Nonempty
hus : (↑u : Set α) ⊆ s
⊢ Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α) (t.sup' ht id ⊓ u.sup' hu id)
have rw : Membership.mem (γ := Set α) ((supClosure : (a : Set α) → Set α) s : Set α)
  ((t ×ˢ u).sup' sorry fun (i : α × α) ↦ id i.1 ⊓ id i.2)
Tactic: rw [sup'_inf_sup']
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : DistribLattice α
s : Set α
hs : s.Finite
⊢ Set.Finite.{u_3} (α := α) ((_root_.latticeClosure : (a : Set α) → Set α) s)
have rw : Set.Finite.{u_3} (α := α) ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α))
Tactic: rw [← supClosure_infClosure]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
β : Type u_4
inst : DistribLattice α
inst_1 : DistribLattice β
s : Set α
t : Set β
⊢ (latticeClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) =
    SProd.sprod (α := Set α) (β := Set β) ((latticeClosure : (a : Set α) → Set α) s : Set α)
      ((latticeClosure : (a : Set β) → Set β) t : Set β)
have simp_rw : (supClosure : (a : Set (α × β)) → Set (α × β)) ((infClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t)) =
  SProd.sprod (α := Set α) (β := Set β)
    ((supClosure : (a : Set α) → Set α) ((infClosure : (a : Set α) → Set α) s : Set α) : Set α)
    ((supClosure : (a : Set β) → Set β) ((infClosure : (a : Set β) → Set β) t : Set β) : Set β)
Tactic: simp_rw [← supClosure_infClosure]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ (i : ι), f i ∈ s
have intro : ∀ (val : Fintype (PLift ι)), ⨆ (i : ι), f i ∈ s
Tactic: cases nonempty_fintype (PLift ι)
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
α : Type u_3
inst : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
inst_2 : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val : Fintype (PLift ι)
⊢ ⨆ (i : ι), f i ∈ s
have intro : (sup' univ sorry fun (i : PLift ι) ↦ f i.down) ∈ s
Tactic: rw [← iSup_plift_down, ← Finset.sup'_univ_eq_ciSup]
-- Lean 4 proof step from Mathlib.Order.SupClosed (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
⊢ sSup t ∈ s
have this : Finite.{u_3 + 1} (↑t : Type u_3)
Tactic: have := ht.to_subtype
-- Lean 4 proof step from Mathlib.Order.SupClosed (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this : Finite.{u_3 + 1} (↑t : Type u_3)
⊢ sSup t ∈ s
have this₁ : Nonempty.{u_3 + 1} (↑t : Type u_3)
Tactic: have := ht'.to_subtype
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this_1 : Finite.{u_3 + 1} (↑t : Type u_3)
this : Nonempty.{u_3 + 1} (↑t : Type u_3)
⊢ sSup t ∈ s
have rw : ⨆ (a : (↑t : Type u_3)), (↑a : α) ∈ s
Tactic: rw [sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s
have rw : sSup (f '' t) ∈ s
Tactic: rw [← sSup_image]
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ (i : ι), f i ∈ s
have inl : IsEmpty ι → ⨆ (i : ι), f i ∈ s
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
ι : Sort u_1
α : Type u_3
inst : CompleteLattice α
f : ι → α
s : Set α
inst_1 : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
inl : IsEmpty ι → ⨆ (i : ι), f i ∈ s
⊢ ⨆ (i : ι), f i ∈ s
have inr : Nonempty ι → ⨆ (i : ι), f i ∈ s
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.SupClosed (hypothesis)
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
⊢ sSup t ∈ s
have this : Finite.{u_3 + 1} (↑t : Type u_3)
Tactic: have := ht.to_subtype
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite.{u_3 + 1} (↑t : Type u_3)
⊢ sSup t ∈ s
have rw : ⨆ (a : (↑t : Type u_3)), (↑a : α) ∈ s
Tactic: rw [sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.Order.SupClosed (goal)
Goal:
α : Type u_3
inst : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s
have rw : sSup (f '' t) ∈ s
Tactic: rw [← sSup_image]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : Membership.mem (γ := Finset ι) {i} j
hj : j ∉ s
⊢ Disjoint (f j) (s.sup f)
have rw : Disjoint (f j) ⊥
Tactic: rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
⊢ f i ≤ t.sup f ↔ i ∈ t
have refine : ∀ (h : f i ≤ t.sup f), i ∈ t
Tactic: refine ⟨fun h => ?_, le_sup⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ t.sup f
⊢ i ∈ t
have by_contra : ∀ (hit : i ∉ t), False
Tactic: by_contra hit
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
hi : i ∈ image g s
hit : i ∉ t
⊢ Disjoint (f i) (t.sup f)
have rcases : ∀ (t : Finset ι') (hts : t ⊆ s) (ht : image g t ⊆ image g s) (hit : i ∉ image g t), Disjoint (f i) ((image g t).sup f)
Tactic: rcases subset_image_iff.mp ht with ⟨t, hts, rfl⟩
Cleared hypotheses: t, ht, hit
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
i : ι
hi : i ∈ image g s
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
hit : i ∉ image g t
⊢ Disjoint (f i) ((image g t).sup f)
have rcases : ∀ (i : ι') (his : i ∈ s) (hi : g i ∈ image g s) (hit : g i ∉ image g t), Disjoint (f (g i)) ((image g t).sup f)
Tactic: rcases mem_image.mp hi with ⟨i, his, rfl⟩
Cleared hypotheses: i, hi, hit
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) ((image g t).sup f)
have rw : Disjoint (f (g i)) (t.sup (f ∘ g))
Tactic: rw [sup_image]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
have refine_1 : ∀ (hs : (map g s).SupIndep f) (t : Finset ι') (ht : t ⊆ s) (i : ι') (hi : i ∈ s) (hit : i ∉ t),
  Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) (t.sup (f ∘ (⇑g : (a : ι') → ι)))
Tactic: refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
refine_1 :
  ∀ (hs : (map g s).SupIndep f) (t : Finset ι') (ht : t ⊆ s) (i : ι') (hi : i ∈ s) (hit : i ∉ t),
    Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) (t.sup (f ∘ (⇑g : (a : ι') → ι)))
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
have refine_2 : ∀ (hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))), (map g s).SupIndep f
Tactic: refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) (t.sup (f ∘ (⇑g : (a : ι') → ι)))
have refine_1 : Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) ((map g t).sup f)
Tactic: rw [← sup_map]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
⊢ (map g s).SupIndep f
have refine_2 : SupIndep (image (⇑g : (a : ι') → ι) s) f
Tactic: rw [map_eq_image]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
⊢ (map g s).SupIndep f
have refine_2 : SupIndep (image (⇑g : (a : ι') → ι) s) f
Tactic: classical
    rw [map_eq_image]
    exact hs.image
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ SupIndep {i, j} f ↔ Disjoint (f i) (f j)
have suffices : Disjoint (f i) (f j) → Disjoint (f j) ((erase {i, j} j).sup f)
Tactic: suffices Disjoint (f i) (f j) → Disjoint (f j) ((Finset.erase {i, j} j).sup f) by
    simpa [supIndep_iff_disjoint_erase, hij]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) ((erase {i, j} j).sup f)
have rw : Disjoint (f i) (f j) → Disjoint (f j) ((erase {j, i} j).sup f)
Tactic: rw [pair_comm]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb : b ∈ s.biUnion g
hab : b ∉ a
⊢ Disjoint (f b) (a.sup f)
have obtain : ∀ (i' : ι') (hi' : i' ∈ s) (hb : b ∈ g i'), Disjoint (f b) (a.sup f)
Tactic: obtain ⟨i', hi', hb⟩ := mem_biUnion.mp hb