awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
simp : ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.inf' ⋯ fun (x : α) ↦ x) (t.inf' ⋯ fun (x : α) ↦ x)
⊢ t.inf' ht id ∈
    (↑(Finset.image (fun (t : ↥({t ∈ s.powerset | t.Nonempty})) ↦ (↑t : Finset α).inf' ⋯ id)
          {t ∈ s.powerset | t.Nonempty}.attach) :
      Set α)

Tactic:
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, mem_filter]

Premises used: Finset.mem_attach, Set.mem_image, Subtype.exists, Finset.coe_image, Finset.mem_powerset, Finset.mem_filter, Finset.mem_coe, true_and, id_eq
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
⊢ ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.inf' ⋯ fun (x : α) ↦ x) (t.inf' ⋯ fun (x : α) ↦ x)

Tactic:
⟨t, ⟨hts, ht⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : (↑t : Set α) ⊆ (↑s : Set α)
⊢ ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.inf' ⋯ fun (x : α) ↦ x) (t.inf' ⋯ fun (x : α) ↦ x)

Tactic:
exact ⟨t, ⟨hts, ht⟩, rfl⟩
-- Module: Mathlib.Order.SupClosed
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 α)
refine₂ :
  ∀ (t : Finset α) (ht : t.Nonempty) (hts : (↑t : Set α) ⊆ (↑s : Set α)),
    ∃ (a : Finset α) (h : a ⊆ s ∧ a.Nonempty), Eq (α := α) (a.inf' ⋯ fun (x : α) ↦ x) (t.inf' ⋯ fun (x : α) ↦ x)
⊢ Set.Finite.{u_3} (α := α) ((infClosure : (a : Set α) → Set α) (↑s : 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⟩

Premises used: Finset.mem_attach, Set.mem_image, Subtype.exists, Finset.coe_image, Set.Finite.subset, Finset.mem_powerset, Finset.attach, Finset.powerset, Finset.mem_filter, Finset.finite_toSet, Finset.filter, Finset.image, Finset.mem_coe, rfl, true_and, id_eq
-- Module: Mathlib.Order.SupClosed
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)

Tactic:
⟨u ×ˢ v, hu.product hv, ?_, ?_⟩

Premises used: SProd.sprod, Set.Mem, setOf, Finset.Nonempty.product, And.intro, Exists.intro
-- Module: Mathlib.Order.SupClosed
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
refine_2 : (u ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)
⊢ Membership.mem (γ := Set (α × β)) ((infClosure : (a : Set (α × β)) → Set (α × β)) (s ×ˢ t) : Set (α × β))
    (u.inf' hu id, v.inf' hv id)

Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
-- Module: Mathlib.Order.SupClosed
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
⊢ (↑(u ×ˢ v) : Set (α × β)) ⊆ s ×ˢ t

Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt

Premises used: Finset.coe_product, Set.prod_mono
-- Module: Mathlib.Order.SupClosed
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
⊢ (u ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)

Tactic:
simp [prodMk_inf'_inf']

Premises used: Finset.prodMk_inf'_inf'
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ s ⊆ (latticeClosure : (a : Set α) → Set α) s

Tactic:
latticeClosure.le_closure _

Premises used: ClosureOperator.le_closure, latticeClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ IsSublattice.{u_3} (α := α) ((latticeClosure : (a : Set α) → Set α) s)

Tactic:
latticeClosure.isClosed_closure _

Premises used: latticeClosure, ClosureOperator.isClosed_closure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s t : Set α
⊢ s ⊆ t → IsSublattice t → (latticeClosure : (a : Set α) → Set α) s ⊆ t

Tactic:
latticeClosure.closure_min

Premises used: ClosureOperator.closure_min
-- Module: Mathlib.Order.SupClosed
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
have :
  ∀
    (h :
      IsSublattice.{u_3} (α := α)
        {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has}),
    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⟩ }
-- Module: Mathlib.Order.SupClosed
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

Tactic:
(latticeClosure_min (fun a ha ↦ ?_) h has).choose_spec

Premises used: Exists.choose_spec, latticeClosure_min
-- Module: Mathlib.Order.SupClosed
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}
refine :
  ∀ (a : α) (ha : a ∈ s),
    Membership.mem (γ := Set α)
      {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has} a
⊢ p a has

Tactic:
refine (latticeClosure_min (fun a ha ↦ ?_) h has).choose_spec

Premises used: Exists.choose_spec, latticeClosure_min
-- Module: Mathlib.Order.SupClosed
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_1 : α
has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a_1
h :
  IsSublattice.{u_3} (α := α)
    {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has}
a : α
ha : a ∈ s
⊢ Membership.mem (γ := Set α)
    {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has} a

Tactic:
⟨subset_latticeClosure ha, mem a ha⟩

Premises used: Set.Mem, setOf, subset_latticeClosure, Exists.intro
-- Module: Mathlib.Order.SupClosed
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_1 : α
has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a_1
h :
  IsSublattice.{u_3} (α := α)
    {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has}
a : α
ha : a ∈ s
⊢ Membership.mem (γ := Set α)
    {a : α | ∃ (has : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a), p a has} a

Tactic:
exact ⟨subset_latticeClosure ha, mem a ha⟩
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
⊢ Monotone.{u_3, u_3} (α := Set α) (β := Set α) (⇑latticeClosure : (a : Set α) → Set α)

Tactic:
latticeClosure.monotone

Premises used: ClosureOperator.monotone, latticeClosure
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ (latticeClosure : (a : Set α) → Set α) s = s ↔ IsSublattice s

Tactic:
latticeClosure.isClosed_iff.symm

Premises used: ClosureOperator.isClosed_iff, latticeClosure, Iff.symm
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
⊢ Eq (α := Set α) ((latticeClosure : (a : Set α) → Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) : Set α)
    ((latticeClosure : (a : Set α) → Set α) s : Set α)

Tactic:
latticeClosure.idempotent _

Premises used: latticeClosure, ClosureOperator.idempotent
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
⊢ Eq.{u_3 + 1} (α := Set α) ((latticeClosure : (a : Set α) → Set α) ∅ : Set α) (∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
a : α
⊢ Eq (α := Set α) ((latticeClosure : (a : Set α) → Set α) {a} : Set α) ({a} : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
⊢ Eq.{u_3 + 1} (α := Set α) ((latticeClosure : (a : Set α) → Set α) Set.univ : Set α) (Set.univ : Set α)

Tactic:
simp
-- Module: Mathlib.Order.SupClosed
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
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
⊢ f '' (latticeClosure : (a : Set α) → Set α) s = (latticeClosure : (a : Set β) → Set β) (f '' s)

Tactic:
simp only [subset_antisymm_iff, Set.image_subset_iff]

Premises used: subset_antisymm_iff, Set.image_subset_iff
-- Module: Mathlib.Order.SupClosed
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)
right : (latticeClosure : (a : Set β) → Set β) (f '' s) ⊆ f '' (latticeClosure : (a : Set α) → Set α) 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

Tactic:
constructor
-- Module: Mathlib.Order.SupClosed
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)
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)

Tactic:
apply latticeClosure_sup_inf_induction

Premises used: latticeClosure_sup_inf_induction
-- Module: Mathlib.Order.SupClosed
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
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

Tactic:
apply latticeClosure_sup_inf_induction

Premises used: latticeClosure_sup_inf_induction
-- Module: Mathlib.Order.SupClosed
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
⊢ ∀ (a : α) (has : a ∈ s), a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)

Tactic:
fun a ha ↦ subset_latticeClosure <| Set.mem_image_of_mem _ ha

Premises used: Set.Mem, setOf, subset_latticeClosure, Set.preimage, Set.mem_image_of_mem
-- Module: Mathlib.Order.SupClosed
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
⊢ ∀ (a : α) (has : a ∈ s), a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)

Tactic:
exact fun a ha ↦ subset_latticeClosure <| Set.mem_image_of_mem _ ha

Premises used: subset_latticeClosure, Set.mem_image_of_mem
-- Module: Mathlib.Order.SupClosed
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
a b : α
ha : a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
hb : b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
⊢ a ⊔ b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)

Tactic:
simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb

Premises used: isSublattice_latticeClosure, IsSublattice.supClosed
-- Module: Mathlib.Order.SupClosed
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
a b : α
ha : a ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
hb : b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)
⊢ a ⊓ b ∈ f ⁻¹' (latticeClosure : (a : Set β) → Set β) (f '' s)

Tactic:
simpa [map_inf] using isSublattice_latticeClosure.infClosed ha hb

Premises used: isSublattice_latticeClosure, IsSublattice.infClosed
-- Module: Mathlib.Order.SupClosed
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
⊢ ∀ (a : β) (has : a ∈ f '' s), a ∈ f '' (latticeClosure : (a : Set α) → Set α) s

Tactic:
Set.image_mono subset_latticeClosure

Premises used: Set.image_mono, subset_latticeClosure, Set.Subset
-- Module: Mathlib.Order.SupClosed
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
⊢ ∀ (a : β) (has : a ∈ f '' s), a ∈ f '' (latticeClosure : (a : Set α) → Set α) s

Tactic:
exact Set.image_mono subset_latticeClosure

Premises used: Set.image_mono, subset_latticeClosure
-- Module: Mathlib.Order.SupClosed
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
a : α
ha : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a
b : α
hb : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b
⊢ f a ⊔ f b ∈ f '' (latticeClosure : (a : Set α) → Set α) s

Tactic:
⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩

Premises used: isSublattice_latticeClosure, Set.Mem, setOf, IsSublattice.supClosed, Max.max, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Order.SupClosed
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
a : α
ha : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a
b : α
hb : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b
⊢ f a ⊔ f b ∈ f '' (latticeClosure : (a : Set α) → Set α) s

Tactic:
exact ⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩
-- Module: Mathlib.Order.SupClosed
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
a : α
ha : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a
b : α
hb : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b
⊢ f a ⊓ f b ∈ f '' (latticeClosure : (a : Set α) → Set α) s

Tactic:
⟨a ⊓ b, isSublattice_latticeClosure.infClosed ha hb, map_inf ..⟩

Premises used: isSublattice_latticeClosure, Set.Mem, setOf, And.intro, Exists.intro, Set.image, IsSublattice.infClosed, Min.min
-- Module: Mathlib.Order.SupClosed
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
a : α
ha : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) a
b : α
hb : Membership.mem (γ := Set α) ((latticeClosure : (a : Set α) → Set α) s : Set α) b
⊢ f a ⊓ f b ∈ f '' (latticeClosure : (a : Set α) → Set α) s

Tactic:
exact ⟨a ⊓ b, isSublattice_latticeClosure.infClosed ha hb, map_inf ..⟩
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
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
⊢ Eq.{u_3 + 1} (α := Set αᵒᵈ)
    (Set.preimage (β := α) (⇑ofDual : (a : αᵒᵈ) → α) ((latticeClosure : (a : Set α) → Set α) s))
    ((latticeClosure : (a : Set αᵒᵈ) → Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s))

Tactic:
ext
-- Module: Mathlib.Order.SupClosed
Goal:
α : Type u_3
inst : Lattice α
s : Set α
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:
simp [latticeClosure, (Equiv.Set.congr toDual).surjective.forall, Equiv.image_eq_preimage_symm]

Premises used: OrderDual.toDual, Function.Surjective.forall, Equiv.Set.congr, Equiv.image_eq_preimage_symm, Equiv.surjective, latticeClosure
-- Module: Mathlib.Order.SupClosed
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)

Tactic:
simpa only [Set.image_comp, Equiv.image_symm_eq_preimage, ← ofDual_preimage_latticeClosure]
    using image_latticeClosure s (ofDual.symm ∘ f) map_sup map_inf

Premises used: OrderDual.ofDual, ofDual_preimage_latticeClosure, Function.comp, image_latticeClosure, Set.image_comp, Equiv.symm, DFunLike.coe, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Order.SupClosed
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
rw :
  Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α)
    ((t ×ˢ u).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)
⊢ Membership.mem (γ := Set α) ((infClosure : (a : Set α) → Set α) s : Set α) (t.inf' ht id ⊔ u.inf' hu id)

Tactic:
rw [inf'_sup_inf']

Premises used: Finset.inf'_sup_inf'