awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
inst : LinearOrder ι'
inst_1 : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite.{u_1 + 1} (↑I : Type u_1)
i : (↑I : Type u_1)
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₁ ≤ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₂

Tactic:
preimage_mono <| hs i i.2 h

Premises used: Set.preimage_mono, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
inst : LinearOrder ι'
inst_1 : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite.{u_1 + 1} (↑I : Type u_1)
i : (↑I : Type u_1)
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₁ ≤ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₂

Tactic:
exact preimage_mono <| hs i i.2 h

Premises used: Set.preimage_mono, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
inst : LinearOrder ι'
inst_1 : Nonempty ι'
inst_2 : Finite ι
α : ι → Type u_3
s : (i : ι) → ι' → Set (α i)
hs : ∀ (i : ι), Monotone (s i)
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), pi (α := α) univ fun (i : ι) ↦ s i j)
    (pi (α := α) univ fun (i : ι) ↦ ⋃ (j : ι'), s i j)

Tactic:
iUnion_pi_of_monotone finite_univ fun i _ => hs i

Premises used: Set.iUnion_pi_of_monotone, Set.finite_univ
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort v
κ : ι → Sort w
inst : Order.Frame α
inst_1 : Finite ι
f : (a : ι) → κ a → α
this :
  ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))

Tactic:
simpa [← Equiv.plift.symm.iInf_comp, ← Equiv.plift.symm.iSup_comp,
        ← (Equiv.plift.piCongr fun a => @Equiv.plift (κ a.down)).symm.iSup_comp] using
      this (κ := fun a => PLift (κ a.down)) fun (a : PLift ι) b => f a.down b.down

Premises used: Equiv.iSup_comp, PLift.down, Equiv.iInf_comp, Equiv.plift, Equiv.piCongr, Equiv.symm
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort v
κ : ι → Sort w
inst : Order.Frame α
inst_1 : Finite ι
f : (a : ι) → κ a → α
suffices :
  ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))

Tactic:
suffices ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : Π a, κ a → α),
      ⨅ a, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a, f a (g a) by
    simpa [← Equiv.plift.symm.iInf_comp, ← Equiv.plift.symm.iSup_comp,
        ← (Equiv.plift.piCongr fun a => @Equiv.plift (κ a.down)).symm.iSup_comp] using
      this (κ := fun a => PLift (κ a.down)) fun (a : PLift ι) b => f a.down b.down
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f : (a : ι_1) → κ_1 a → α
ι : Type v
κ : ι → Type w
_ :
  ∀ [Finite ι] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
⊢ ∀ [Finite ι] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))

Tactic:
_
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
inst_2 : Finite ι
α_1 β : Type v
e : α_1 ≃ β
h :
  ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a))
κ : β → Type w
f : (a : β) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ (a : β), ⨆ (b : κ a), f a b) (⨆ (g : (a : β) → κ a), ⨅ (a : β), f a (g a))

Tactic:
simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]

Premises used: Equiv.iSup_comp, Equiv.piCongrLeft, Equiv.iInf_comp
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
inst_2 : Finite ι
κ : PEmpty.{v + 1} → Type w
f : (a : PEmpty.{v + 1}) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ (a : PEmpty.{v + 1}), ⨆ (b : κ a), f a b)
    (⨆ (g : (a : PEmpty.{v + 1}) → κ a), ⨅ (a : PEmpty.{v + 1}), f a (g a))

Tactic:
simp [iInf_of_empty, iSup_const]

Premises used: iInf_of_empty, iSup_const
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
inst_2 : Finite ι
α_1 : Type v
inst_3 : Fintype α_1
h :
  ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a))
κ : Option α_1 → Type w
f : (a : Option α_1) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ (a : Option α_1), ⨆ (b : κ a), f a b)
    (⨆ (g : (a : Option α_1) → κ a), ⨅ (a : Option α_1), f a (g a))

Tactic:
simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]

Premises used: Equiv.piOptionEquivProd_symm_apply, iInf_option, Equiv.piOptionEquivProd, Equiv.iSup_comp, iSup_inf_eq, inf_iSup_eq, Equiv.symm, iSup_prod
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι_1 : Sort v
κ_1 : ι_1 → Sort w
inst : Order.Frame α
inst_1 : Finite ι_1
f_1 : (a : ι_1) → κ_1 a → α
ι : Type v
κ : ι → Type w
inst_2 : Finite ι
f : (a : ι) → κ a → α
of_equiv :
  ∀ {α_1 β : Type v} (e : α_1 ≃ β)
    (h :
      ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
        Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a)))
    {κ : β → Type w} (f : (a : β) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : β), ⨆ (b : κ a), f a b) (⨆ (g : (a : β) → κ a), ⨅ (a : β), f a (g a))
h_empty :
  ∀ {κ : PEmpty.{v + 1} → Type w} (f : (a : PEmpty.{v + 1}) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : PEmpty.{v + 1}), ⨆ (b : κ a), f a b)
      (⨆ (g : (a : PEmpty.{v + 1}) → κ a), ⨅ (a : PEmpty.{v + 1}), f a (g a))
h_option :
  ∀ {α_1 : Type v} [Fintype α_1]
    (h :
      ∀ {κ : α_1 → Type w} (f : (a : α_1) → κ a → α),
        Eq.{u + 1} (α := α) (⨅ (a : α_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : α_1) → κ a), ⨅ (a : α_1), f a (g a)))
    {κ : Option α_1 → Type w} (f : (a : Option α_1) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ (a : Option α_1), ⨆ (b : κ a), f a b)
      (⨆ (g : (a : Option α_1) → κ a), ⨅ (a : Option α_1), f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))

Tactic:
induction ι using Finite.induction_empty_option with
  | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
  | h_empty => simp [iInf_of_empty, iSup_const]
  | h_option h =>
    simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]

Premises used: Equiv.piOptionEquivProd_symm_apply, iInf_of_empty, Finite.induction_empty_option, iInf_option, iSup_inf_eq, inf_iSup_eq, iSup_const, iSup_prod
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort v
κ : ι → Sort w
inst : Order.Coframe α
inst_1 : Finite ι
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨆ (a : ι), ⨅ (b : κ a), f a b) (⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a))

Tactic:
iInf_iSup_eq_of_finite (α := αᵒᵈ)

Premises used: iInf, iSup, OrderDual, iInf_iSup_eq_of_finite
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ Nonempty ((a : ι) → PLift (κ a))

Tactic:
haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
this : Nonempty ((a : ι) → PLift (κ a))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))

Tactic:
simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down

Premises used: Equiv.iSup_comp, PLift.down, Equiv.plift, Equiv.piCongrRight, Equiv.symm
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
suffices :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))

Tactic:
suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ_1 : ι → Sort w
inst : Nonempty ((a : ι) → κ_1 a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ_1 a → α
κ : ι → Type w
_ :
  ∀ [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ ∀ [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))

Tactic:
_
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ_1 : ι → Sort w
inst : Nonempty ((a : ι) → κ_1 a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f_1 : (a : ι) → κ_1 a → α
κ : ι → Type w
inst_2 : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
⊢ Finite.{v + 1} (↑s : Type v)

Tactic:
haveI := hs.to_subtype
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ_1 : ι → Sort w
inst : Nonempty ((a : ι) → κ_1 a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f_1 : (a : ι) → κ_1 a → α
κ : ι → Type w
inst_2 : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
this : Finite.{v + 1} (↑s : Type v)
⊢ Nonempty ((a : { a : ι // a ∉ s }) → κ (↑a : ι))

Tactic:
haveI : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ_1 : ι → Sort w
inst : Nonempty ((a : ι) → κ_1 a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f_1 : (a : ι) → κ_1 a → α
κ : ι → Type w
inst_2 : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
this_1 : Finite.{v + 1} (↑s : Type v)
this : Nonempty ((a : { a : ι // a ∉ s }) → κ (↑a : ι))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))

Tactic:
simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]

Premises used: Equiv.iSup_comp, Membership.mem, iInf_subtype'', Equiv.piEquivPiSubtypeProd, iSup_const, Equiv.symm, iInf_iSup_eq_of_finite, iSup_prod
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
suffices suffices₁ suffices₂ suffices₃ :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
suffices₄ :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α) (this : Finite.{v + 1} (↑s : Type v)),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
suffices₅ :
  ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α) (this : Finite.{v + 1} (↑s : Type v))
    (this : Nonempty ((a : { a : ι // a ∉ s }) → κ (↑a : ι))),
    Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))
⊢ Eq.{u + 1} (α := α) (⨅ a ∈ s, ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ a ∈ s, f a (g a))

Tactic:
classical
  suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    haveI : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  haveI := hs.to_subtype
  haveI : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]

Premises used: iInf_subtype'', iSup_const, iSup_prod
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type v
κ : ι → Sort w
inst : Nonempty ((a : ι) → κ a)
inst_1 : Order.Coframe α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨆ a ∈ s, ⨅ (b : κ a), f a b) (⨅ (g : (a : ι) → κ a), ⨆ a ∈ s, f a (g a))

Tactic:
hs.biInf_iSup_eq (α := αᵒᵈ)

Premises used: iInf, iSup, Set.Finite.biInf_iSup_eq, OrderDual
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
s : Set α
hs : s.Finite
⊢ BddAbove s

Tactic:
Finite.induction_on _ hs bddAbove_empty fun _ _ h => h.insert _

Premises used: Set.Finite.induction_on
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
I : Set β
S : β → Set α
⊢ BddAbove.{u} (α := α) (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), S i) ↔
    ∀ (i : β), Membership.mem (γ := Set β) ∅ i → BddAbove (S i)

Tactic:
simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]

Premises used: Set.biUnion_empty, bddAbove_empty, Set.forall_mem_empty
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
I : Set β
S : β → Set α
a : β
s : Set β
h : a ∉ s
hs_1 : s.Finite
hs : BddAbove.{u} (α := α) (⋃ i ∈ s, S i) ↔ ∀ i ∈ s, BddAbove (S i)
⊢ BddAbove.{u} (α := α) (⋃ i ∈ insert a s, S i) ↔ ∀ i ∈ insert a s, BddAbove (S i)

Tactic:
simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

Premises used: Set.forall_mem_insert, bddAbove_union, Set.biUnion_insert
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
empty :
  BddAbove.{u} (α := α) (⋃ (i : β), ⋃ (_ : Membership.mem (γ := Set β) ∅ i), S i) ↔
    ∀ (i : β), Membership.mem (γ := Set β) ∅ i → BddAbove (S i)
insert :
  ∀ {a : β} {s : Set β},
    a ∉ s →
      s.Finite →
        ∀ (hs : BddAbove.{u} (α := α) (⋃ i ∈ s, S i) ↔ ∀ i ∈ s, BddAbove (S i)),
          BddAbove.{u} (α := α) (⋃ i ∈ Insert.insert a s, S i) ↔ ∀ i ∈ Insert.insert a s, BddAbove (S i)
⊢ BddAbove.{u} (α := α) (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)

Tactic:
induction I, H using Set.Finite.induction_on with
  | empty => simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]
  | insert _ _ hs => simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

Premises used: Set.forall_mem_insert, bddAbove_union, Set.biUnion_empty, Set.biUnion_insert, Insert.insert, bddAbove_empty, Set.forall_mem_empty
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
s : Set α
⊢ ¬BddAbove s → s.Infinite

Tactic:
mt Finite.bddAbove

Premises used: mt, Set.Finite.bddAbove, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : Nonempty α
s : Finset α
⊢ BddAbove (↑s : Set α)

Tactic:
s.finite_toSet.bddAbove

Premises used: Finset.finite_toSet, Set.Finite.bddAbove
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
inst : LinearOrder α
s : Set α
⊢ (s \ ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y).Finite

Tactic:
Set.finite_of_forall_not_lt_lt fun _x hx _y hy _z hz hxy hyz => hy.2 <| mem_iUnion₂_of_mem hx.1 <|
    mem_iUnion₂_of_mem hz.1 ⟨hxy, hyz⟩

Premises used: Set.mem_iUnion₂_of_mem, And.right, And.left, And.intro, Set.finite_of_forall_not_lt_lt
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
inst : LinearOrder α
s : Set α
⊢ (s \ ⋃ (x : (↑s : Type u) × (↑s : Type u)), Ioo (↑x.1 : α) (↑x.2 : α)).Finite

Tactic:
simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_diff_iUnion_Ioo

Premises used: Set.finite_diff_iUnion_Ioo, iSup_subtype, Set.iUnion, iSup_prod
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
hs : (↑∅ : Set α) ⊆ ⋃ (i : ι), f i
⊢ ∃ (i : ι), (↑∅ : Set α) ⊆ f i

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (↑(Finset.cons b t hbt) : Set α) ⊆ ⋃ (i : ι), f i
cons : ∀ (hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
⊢ ∃ (i : ι), (↑(Finset.cons b t hbt) : Set α) ⊆ f i

Tactic:
simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢

Premises used: Finset.coe_cons, Set.mem_iUnion, Set.insert_subset_iff
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i
cons : ∀ (i : ι) (hi : b ∈ f i) (j : ι) (hj : (↑t : Set α) ⊆ f j), ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
⊢ ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i

Tactic:
rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩

Premises used: And.imp_right
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i
i : ι
hi : b ∈ f i
j : ι
hj : (↑t : Set α) ⊆ f j
cons : ∀ (k : ι) (hik : f i ⊆ f k) (hjk : f j ⊆ f k), ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i
⊢ ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i

Tactic:
rcases h i j with ⟨k, hik, hjk⟩
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i
i : ι
hi : b ∈ f i
j : ι
hj : (↑t : Set α) ⊆ f j
k : ι
hik : f i ⊆ f k
hjk : f j ⊆ f k
⊢ ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i

Tactic:
⟨k, hik hi, hj.trans hjk⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i
hs : (∃ (i : ι), b ∈ f i) ∧ (↑t : Set α) ⊆ ⋃ (i : ι), f i
i : ι
hi : b ∈ f i
j : ι
hj : (↑t : Set α) ⊆ f j
k : ι
hik : f i ⊆ f k
hjk : f j ⊆ f k
⊢ ∃ (i : ι), b ∈ f i ∧ (↑t : Set α) ⊆ f i

Tactic:
exact ⟨k, hik hi, hj.trans hjk⟩
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : Nonempty ι
f : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ (i : ι), f i
empty : ∀ (hs : (↑∅ : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑∅ : Set α) ⊆ f i
cons :
  ∀ (b : α) (t : Finset α) (hbt : b ∉ t) (iht : ∀ (hs : (↑t : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑t : Set α) ⊆ f i)
    (hs : (↑(Finset.cons b t hbt) : Set α) ⊆ ⋃ (i : ι), f i), ∃ (i : ι), (↑(Finset.cons b t hbt) : Set α) ⊆ f i
⊢ ∃ (i : ι), (↑s : Set α) ⊆ f i

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons b t hbt iht =>
    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩

Premises used: Finset.coe_cons, Set.mem_iUnion, Set.insert_subset_iff
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun (i j : ι) ↦ f i ⊆ f j) c
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ i ∈ c, f i
⊢ (↑s : Set α) ⊆ ⋃ (x : (↑c : Type u_2)), f (↑x : ι)

Tactic:
rw [Set.biUnion_eq_iUnion] at hs

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun (i j : ι) ↦ f i ⊆ f j) c
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ (x : (↑c : Type u_2)), f (↑x : ι)
⊢ Nonempty.{u_2 + 1} (↑c : Type u_2)

Tactic:
haveI := hn.coe_sort
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun (i j : ι) ↦ f i ⊆ f j) c
s : Finset α
hs : (↑s : Set α) ⊆ ⋃ (x : (↑c : Type u_2)), f (↑x : ι)
this : Nonempty.{u_2 + 1} (↑c : Type u_2)
⊢ ∃ i ∈ c, (↑s : Set α) ⊆ f i

Tactic:
simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

Premises used: Iff.mpr, DirectedOn.directed_val, directed_comp, Directed.exists_mem_subset_of_finset_subset_biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ (↑(hs.toFinset (s := s)) : Set α) ⊆ ⋃ i ∈ c, i

Tactic:
rw [← hs.coe_toFinset, sUnion_eq_biUnion] at hsc

Premises used: Set.Finite.coe_toFinset, Set.sUnion_eq_biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : (↑(hs.toFinset (s := s)) : Set α) ⊆ ⋃ i ∈ c, i
⊢ ∃ i ∈ c, (↑(hs.toFinset (s := s)) : Set α) ⊆ i

Tactic:
have := DirectedOn.exists_mem_subset_of_finset_subset_biUnion hn hc hsc
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : (↑(hs.toFinset (s := s)) : Set α) ⊆ ⋃ i ∈ c, i
this : ∃ i ∈ c, (↑(hs.toFinset (s := s)) : Set α) ⊆ i
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
hs.coe_toFinset ▸ this

Premises used: Eq.rec, Set.Finite.coe_toFinset
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : (↑(hs.toFinset (s := s)) : Set α) ⊆ ⋃ i ∈ c, i
this : ∃ i ∈ c, (↑(hs.toFinset (s := s)) : Set α) ⊆ i
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
exact hs.coe_toFinset ▸ this