awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
rw : Set.Finite.{v} (α := β) (⋃ x ∈ range f, (↑x : Set β))
⊢ Set.Finite.{v} (α := β) (⋃ (a : α), (↑(f a) : Set β))

Tactic:
rw [← biUnion_range]

Premises used: Set.biUnion_range
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ Set.Finite.{v} (α := β) (⋃ x ∈ range f, (↑x : Set β))

Tactic:
h.biUnion fun y _ => y.finite_toSet

Premises used: Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ Set.Finite.{v} (α := β) (⋃ x ∈ range f, (↑x : Set β))

Tactic:
exact h.biUnion fun y _ => y.finite_toSet

Premises used: Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
himage : (f '' s).Finite
hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite
x : α
⊢ x ∈ s → Membership.mem (γ := Set α) (⋃ i ∈ f '' s, s ∩ f ⁻¹' {i}) x

Tactic:
aesop
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
⊢ ∀ (x : (↑s : Type u)), ∃ (i : ι), (↑x : α) ∈ t i

Tactic:
simpa [subset_def] using h

Premises used: Set.subset_def
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
choose :
  ∀ (f : (x : (↑s : Type u)) → ι) (hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)),
    ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
⊢ ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
⊢ ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
⟨range f, finite_range f, fun x hx => ?_⟩

Premises used: Set.finite_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
refine : ∀ (x : α) (hx : x ∈ s), Membership.mem (γ := Set α) (⋃ i ∈ range f, t i) x
⊢ ∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
refine ⟨range f, finite_range f, fun x hx => ?_⟩
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
x : α
hx : x ∈ s
rw : ∃ (i : (↑s : Type u)), x ∈ t (f i)
⊢ Membership.mem (γ := Set α) (⋃ i ∈ range f, t i) x

Tactic:
rw [biUnion_range, mem_iUnion]

Premises used: Set.mem_iUnion, Set.biUnion_range
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ (i : (↑s : Type u)), x ∈ t (f i)

Tactic:
⟨⟨x, hx⟩, hf _⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
this : Finite.{u + 1} (↑s : Type u)
f : (x : (↑s : Type u)) → ι
hf : ∀ (x : (↑s : Type u)), (↑x : α) ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ (i : (↑s : Type u)), x ∈ t (f i)

Tactic:
exact ⟨⟨x, hx⟩, hf _⟩
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
h₁ :
  ∀ (x : α),
    x ∈ t ↔
      Membership.mem (γ := Set α)
        (⋃ (i : (↑{i : ι | i ∈ I} : Type u_1)), (fun (x : (↑{i : ι | i ∈ I} : Type u_1)) ↦ s (↑x : ι) ∩ t) i) x
⊢ t = ⋃ (i : (↑{i : ι | i ∈ I} : Type u_1)), (fun (x : (↑{i : ι | i ∈ I} : Type u_1)) ↦ s (↑x : ι) ∩ t) i

Tactic:
ext x
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
h₁ : x ∈ t ↔ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
⊢ x ∈ t ↔
    Membership.mem (γ := Set α)
      (⋃ (i : (↑{i : ι | i ∈ I} : Type u_1)), (fun (x : (↑{i : ι | i ∈ I} : Type u_1)) ↦ s (↑x : ι) ∩ t) i) x

Tactic:
rw [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
h₁ : x ∈ t → ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
h₂ : (∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t) → x ∈ t
⊢ x ∈ t ↔ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t

Tactic:
constructor
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
h₁ :
  ∀ (i : ι) (hi : i ∈ I) (H : Membership.mem (γ := Set α) ((fun (h : i ∈ I) ↦ s i) hi) x),
    ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t
⊢ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t

Tactic:
rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩

Premises used: Set.mem_iUnion, Iff.mp, rfl
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : Membership.mem (γ := Set α) ((fun (h : i ∈ I) ↦ s i) hi) x
⊢ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t

Tactic:
⟨⟨i, hi⟩, ⟨H, x_in⟩⟩

Premises used: Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : Membership.mem (γ := Set α) ((fun (h : i ∈ I) ↦ s i) hi) x
⊢ ∃ (i : (↑{i : ι | i ∈ I} : Type u_1)), x ∈ s (↑i : ι) ∩ t

Tactic:
exact ⟨⟨i, hi⟩, ⟨H, x_in⟩⟩
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
i : (↑{i : ι | i ∈ I} : Type u_1)
H : x ∈ t
⊢ x ∈ t

Tactic:
H
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
i : (↑{i : ι | i ∈ I} : Type u_1)
H : x ∈ t
⊢ x ∈ t

Tactic:
exact H
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
inst : Infinite ι
s : ι → Set α
hs : Injective s
hfin : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
i j : ι
h_eq :
  Eq.{u + 1} (α := (↑{b : Set α | b ⊆ ⋃ (i : ι), s i} : Type u))
    ((fun (i : ι) ↦
        (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ ⋃ (i : ι), s i} x) (s i)
            ⋯ :
          { x : Set α // Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ ⋃ (i : ι), s i} x }))
      i)
    ((fun (i : ι) ↦
        (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ ⋃ (i : ι), s i} x) (s i)
            ⋯ :
          { x : Set α // Membership.mem (γ := Set (Set α)) {b : Set α | b ⊆ ⋃ (i : ι), s i} x }))
      j)
⊢ s i = s j

Tactic:
simpa using h_eq
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
rw : Set.Infinite.{u} (α := α) (⋃ (x : (↑a : Type u_1)), s (↑x : ι))
⊢ Set.Infinite.{u} (α := α) (⋃ i ∈ a, s i)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ Infinite.{u_1 + 1} (↑a : Type u_1)

Tactic:
have _ := ha.to_subtype
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
h : Infinite.{u_1 + 1} (↑a : Type u_1)
x x_1 : (↑a : Type u_1)
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
hij : s (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ a) i hi) : ι) = s (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ a) j hj) : ι)
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ a) i hi = Subtype.mk (p := fun (x : ι) ↦ x ∈ a) j hj

Tactic:
simp [hs hi hj hij]
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
h : Infinite.{u_1 + 1} (↑a : Type u_1)
⊢ Set.Infinite.{u} (α := α) (⋃ (x : (↑a : Type u_1)), s (↑x : ι))

Tactic:
exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]

Premises used: Set.infinite_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set (Set α)
hs : s.Infinite
rw : Set.Infinite.{u} (α := α) (⋃ (i : (↑s : Type u)), (↑i : Set α))
⊢ (⋃₀ s).Infinite

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ Infinite.{u + 1} (↑s : Type u)

Tactic:
have _ := hs.to_subtype
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set (Set α)
hs : s.Infinite
h : Infinite.{u + 1} (↑s : Type u)
⊢ Set.Infinite.{u} (α := α) (⋃ (i : (↑s : Type u)), (↑i : Set α))

Tactic:
infinite_iUnion Subtype.coe_injective

Premises used: Subtype.coe_injective, Set.infinite_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set (Set α)
hs : s.Infinite
h : Infinite.{u + 1} (↑s : Type u)
⊢ Set.Infinite.{u} (α := α) (⋃ (i : (↑s : Type u)), (↑i : Set α))

Tactic:
exact infinite_iUnion Subtype.coe_injective

Premises used: Subtype.coe_injective, Set.infinite_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (hs.toFinset (s := s).sup g) : β)
    (hs.toFinset (s := s).sup ((⇑f : (a : α) → β) ∘ g) : β)

Tactic:
have := map_finset_sup f hs.toFinset g
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this :
  Eq.{v + 1} (α := β) ((f : (a : α) → β) (hs.toFinset (s := s).sup g) : β)
    (hs.toFinset (s := s).sup ((⇑f : (a : α) → β) ∘ g) : β)
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ a ∈ s, g a) : β) (⨆ a ∈ s, (f : (a : α) → β) (g a) : β)

Tactic:
simp only [Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply] at this

Premises used: Set.Finite.mem_toFinset, Finset.sup_eq_iSup, Function.comp_apply
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ a ∈ s, g a) : β) (⨆ a ∈ s, (f : (a : α) → β) (g a) : β)
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ x ∈ s, g x) : β) (⨆ x ∈ s, (f : (a : α) → β) (g x) : β)

Tactic:
this
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ a ∈ s, g a) : β) (⨆ a ∈ s, (f : (a : α) → β) (g a) : β)
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ x ∈ s, g x) : β) (⨆ x ∈ s, (f : (a : α) → β) (g x) : β)

Tactic:
exact this
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
inst_4 : Finite ι
f : F
g : ι → α
rw :
  Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), g x) : β)
    (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), (f : (a : α) → β) (g x) : β)
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ (i : ι), g i) : β) (⨆ (i : ι), (f : (a : α) → β) (g i) : β)

Tactic:
rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]

Premises used: iSup_univ
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
inst_4 : Finite ι
f : F
g : ι → α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), g x) : β)
    (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), (f : (a : α) → β) (g x) : β)

Tactic:
map_finite_biSup finite_univ f g

Premises used: Set.map_finite_biSup, Set.finite_univ
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : FunLike F α β
inst_3 : SupBotHomClass F α β
inst_4 : Finite ι
f : F
g : ι → α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), g x) : β)
    (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ x), (f : (a : α) → β) (g x) : β)

Tactic:
exact map_finite_biSup finite_univ f g

Premises used: Set.map_finite_biSup, Set.finite_univ
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
hf : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Monotone (f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), f i j)
    (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), ⨆ (j : ι'), f i j)

Tactic:
simp [iSup_const]

Premises used: iSup_const
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
ihs :
  ∀ (hf : ∀ i ∈ s_1, Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s_1, f i j) (⨅ i ∈ s_1, ⨆ (j : ι'), f i j)
hf : ∀ i ∈ insert a s_1, Monotone (f i)
⊢ Monotone (f a) ∧ ∀ x ∈ s_1, Monotone (f x)

Tactic:
rw [forall_mem_insert] at hf

Premises used: Set.forall_mem_insert
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
ihs :
  ∀ (hf : ∀ i ∈ s_1, Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s_1, f i j) (⨅ i ∈ s_1, ⨆ (j : ι'), f i j)
hf : Monotone (f a) ∧ ∀ x ∈ s_1, Monotone (f x)
insert :
  Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), f a j ⊓ ⨅ x ∈ s_1, f x j) ((⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ i ∈ s_1, f i j)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ Insert.insert a s_1, f i j) (⨅ i ∈ Insert.insert a s_1, ⨆ (j : ι'), f i j)

Tactic:
simp only [iInf_insert, ← ihs hf.2]

Premises used: And.right, iInf_insert
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
ihs :
  ∀ (hf : ∀ i ∈ s_1, Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s_1, f i j) (⨅ i ∈ s_1, ⨆ (j : ι'), f i j)
hf : Monotone (f a) ∧ ∀ x ∈ s_1, Monotone (f x)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), f a j ⊓ ⨅ x ∈ s_1, f x j) ((⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ i ∈ s_1, f i j)

Tactic:
iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

Premises used: iInf₂_mono, And.right, And.left, iSup_inf_of_monotone
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
f : ι → ι' → α
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
ihs :
  ∀ (hf : ∀ i ∈ s_1, Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s_1, f i j) (⨅ i ∈ s_1, ⨆ (j : ι'), f i j)
hf : Monotone (f a) ∧ ∀ x ∈ s_1, Monotone (f x)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), f a j ⊓ ⨅ x ∈ s_1, f x j) ((⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ i ∈ s_1, f i j)

Tactic:
exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

Premises used: iInf₂_mono, And.right, And.left, iSup_inf_of_monotone
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
hs : s.Finite
f : ι → ι' → α
hf : ∀ i ∈ s, Monotone (f i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Monotone (f i)),
    Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), f i j)
      (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), ⨆ (j : ι'), f i j)
insert :
  ∀ {a : ι} {s : Set ι},
    a ∉ s →
      s.Finite →
        ∀
          (ihs :
            ∀ (hf : ∀ i ∈ s, Monotone (f i)),
              Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s, f i j) (⨅ i ∈ s, ⨆ (j : ι'), f i j))
          (hf : ∀ i ∈ Insert.insert a s, Monotone (f i)),
          Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ Insert.insert a s, f i j)
            (⨅ i ∈ Insert.insert a s, ⨆ (j : ι'), f i j)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s, f i j) (⨅ i ∈ s, ⨆ (j : ι'), f i j)

Tactic:
induction s, hs using Set.Finite.induction_on with
  | empty => simp [iSup_const]
  | insert _ _ ihs =>
    rw [forall_mem_insert] at hf
    simp only [iInf_insert, ← ihs hf.2]
    exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

Premises used: Set.forall_mem_insert, Insert.insert, iSup_const, iInf_insert
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι'
inst_1 : Nonempty ι'
inst_2 : IsCodirectedOrder ι'
inst_3 : Order.Frame α
s : Set ι
hs : s.Finite
f : ι → ι' → α
hf : ∀ i ∈ s, Antitone (f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ i ∈ s, f i j) (⨅ i ∈ s, ⨆ (j : ι'), f i j)

Tactic:
@Finite.iSup_biInf_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ hs _ fun i hi => (hf i hi).dual_left

Premises used: Set.Finite.iSup_biInf_of_monotone, Antitone.dual_left, OrderDual
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Finite ι
inst_1 : Preorder ι'
inst_2 : Nonempty ι'
inst_3 : IsDirectedOrder ι'
inst_4 : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ (i : ι), f i j) (⨅ (i : ι), ⨆ (j : ι'), f i j)

Tactic:
simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i

Premises used: Set.Finite.iSup_biInf_of_monotone, Set.finite_univ, iInf_univ
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Finite ι
inst_1 : Preorder ι'
inst_2 : Nonempty ι'
inst_3 : IsCodirectedOrder ι'
inst_4 : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Antitone (f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (j : ι'), ⨅ (i : ι), f i j) (⨅ (i : ι), ⨆ (j : ι'), f i j)

Tactic:
@iSup_iInf_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ _ fun i => (hf i).dual_left

Premises used: iSup_iInf_of_monotone, Antitone.dual_left, OrderDual
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Finite ι
inst_1 : Preorder ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Nonempty ι'
s : ι → ι' → Set α
hs : ∀ (i : ι), Monotone (s i)
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ (j : ι'), ⋂ (i : ι), s i j) (⋂ (i : ι), ⋃ (j : ι'), s i j)

Tactic:
iSup_iInf_of_monotone hs

Premises used: Set.iInter, iSup_iInf_of_monotone, Set.iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Finite ι
inst_1 : Preorder ι'
inst_2 : IsCodirectedOrder ι'
inst_3 : Nonempty ι'
s : ι → ι' → Set α
hs : ∀ (i : ι), Antitone (s i)
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ (j : ι'), ⋂ (i : ι), s i j) (⋂ (i : ι), ⋃ (j : ι'), s i j)

Tactic:
iSup_iInf_of_antitone hs

Premises used: Set.iInter, iSup_iInf_of_antitone, Set.iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Finite ι
inst_1 : Preorder ι'
inst_2 : IsCodirectedOrder ι'
inst_3 : Nonempty ι'
s : ι → ι' → Set α
hs : ∀ (i : ι), Monotone (s i)
⊢ Eq.{u_3 + 1} (α := Set α) (⋂ (j : ι'), ⋃ (i : ι), s i j) (⋃ (i : ι), ⋂ (j : ι'), s i j)

Tactic:
iInf_iSup_of_monotone hs

Premises used: Set.iInter, iInf_iSup_of_monotone, Set.iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Finite ι
inst_1 : Preorder ι'
inst_2 : IsDirectedOrder ι'
inst_3 : Nonempty ι'
s : ι → ι' → Set α
hs : ∀ (i : ι), Antitone (s i)
⊢ Eq.{u_3 + 1} (α := Set α) (⋂ (j : ι'), ⋃ (i : ι), s i j) (⋃ (i : ι), ⋂ (j : ι'), s i j)

Tactic:
iInf_iSup_of_antitone hs

Premises used: iInf_iSup_of_antitone, Set.iInter, Set.iUnion
-- 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)
simp :
  Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) j)
    (⋂ (x : (↑I : Type u_1)), ⋃ (i : ι'), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) i)
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), I.pi (α := α) fun (i : ι) ↦ s i j)
    (I.pi (α := α) fun (i : ι) ↦ ⋃ (j : ι'), s i j)

Tactic:
simp only [pi_def, biInter_eq_iInter, preimage_iUnion]

Premises used: Set.biInter_eq_iInter, Set.preimage_iUnion, Set.pi_def
-- 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)
⊢ Finite.{u_1 + 1} (↑I : Type u_1)

Tactic:
haveI := hI.fintype.finite
-- 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)
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) j)
    (⋂ (x : (↑I : Type u_1)), ⋃ (i : ι'), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) i)

Tactic:
iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)

Premises used: Set.iUnion_iInter_of_monotone
-- 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)
refine :
  ∀ (i : (↑I : Type u_1)) (j₁ j₂ : ι') (h : j₁ ≤ j₂),
    eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₁ ≤ eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) j₂
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (j : ι'), ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) j)
    (⋂ (x : (↑I : Type u_1)), ⋃ (i : ι'), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) i)

Tactic:
refine iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)

Premises used: Set.iUnion_iInter_of_monotone