awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : Finite ι
f : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(f i) : Type u)
this_1 : Fintype (PLift ι)
this : (i : ι) → Fintype (↑(f i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)

Tactic:
apply (fintypeiUnion _).finite

Premises used: Fintype.finite, Set.fintypeiUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst : Finite ι
f : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(f i) : Type u)
this_1 : Fintype (PLift ι)
this : (i : ι) → Fintype (↑(f i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (i : ι), f i) : Type u)

Tactic:
classical apply (fintypeiUnion _).finite

Premises used: Fintype.finite, Set.fintypeiUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst : Finite.{u + 1} (↑s : Type u)
H : ∀ (t : (↑s : Type u)), Finite.{u + 1} (↑(↑t : Set α) : Type u)
rw : Finite.{u + 1} (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)
⊢ Finite.{u + 1} (↑(⋃₀ s) : Type u)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst : Finite.{u + 1} (↑s : Type u)
H : ∀ (t : (↑s : Type u)), Finite.{u + 1} (↑(↑t : Set α) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)

Tactic:
@Finite.Set.finite_iUnion _ _ _ _ H

Premises used: Finite.Set.finite_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst : Finite.{u + 1} (↑s : Type u)
H : ∀ (t : (↑s : Type u)), Finite.{u + 1} (↑(↑t : Set α) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (i : (↑s : Type u)), (↑i : Set α)) : Type u)

Tactic:
exact @Finite.Set.finite_iUnion _ _ _ _ H

Premises used: Finite.Set.finite_iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : Set ι
inst : Finite.{u_1 + 1} (↑s : Type u_1)
t : ι → Set α
H : ∀ i ∈ s, Finite.{u + 1} (↑(t i) : Type u)
rw : Finite.{u + 1} (↑(⋃ (x : (↑s : Type u_1)), t (↑x : ι)) : Type u)
⊢ Finite.{u + 1} (↑(⋃ x ∈ s, t x) : Type u)

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 ι
inst : Finite.{u_1 + 1} (↑s : Type u_1)
t : ι → Set α
H : ∀ i ∈ s, Finite.{u + 1} (↑(t i) : Type u)
⊢ ∀ (i : (↑s : Type u_1)), Finite.{u + 1} (↑(t (↑i : ι)) : Type u)

Tactic:
haveI : ∀ i : s, Finite (t i) := fun i => H i i.property
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : Set ι
inst : Finite.{u_1 + 1} (↑s : Type u_1)
t : ι → Set α
H : ∀ i ∈ s, Finite.{u + 1} (↑(t i) : Type u)
this : ∀ (i : (↑s : Type u_1)), Finite.{u + 1} (↑(t (↑i : ι)) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (x : (↑s : Type u_1)), t (↑x : ι)) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι_1 : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst : Finite.{u_1 + 1} (↑s : Type u_1)
t : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(t i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ x ∈ s, t x) : Type u)

Tactic:
finite_biUnion s t fun _ _ => inferInstance

Premises used: inferInstance, Finite.Set.finite_biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι_1 : Sort w
γ : Type x
ι : Type u_1
p : ι → Prop
h : Finite.{u_1 + 1} (↑{x : ι | p x} : Type u_1)
t : ι → Set α
inst : ∀ (i : ι), Finite.{u + 1} (↑(t i) : Type u)
⊢ Finite.{u + 1} (↑(⋃ (x : ι), ⋃ (_ : p x), t x) : Type u)

Tactic:
@Finite.Set.finite_biUnion' _ _ (setOf p) h t _

Premises used: Set.Mem, setOf, Finite.Set.finite_biUnion'
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
ι_1 : Sort w
γ : Type x
ι : Sort u_1
inst : Nonempty ι
t : ι → Set α
inst_1 : ∀ (i : ι), Finite.{u + 1} (↑(t i) : Type u)
⊢ Finite.{u + 1} (↑(⋂ (i : ι), t i) : Type u)

Tactic:
Finite.Set.subset (t <| Classical.arbitrary ι) (iInter_subset _ _)

Premises used: Finite.Set.subset, Classical.arbitrary, Set.iInter_subset
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort w
inst : Finite ι
f : ι → Set α
H : ∀ (i : ι), (f i).Finite
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), f i)

Tactic:
haveI := fun i => (H i).to_subtype
  toFinite _

Premises used: Set.toFinite, Set.iUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

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

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 ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Set.Finite.{u} (α := α) (⋃ (x : (↑s : Type u_1)), t (↑x : ι) ⋯)

Tactic:
apply finite_iUnion fun i : s => ht i.1 i.2

Premises used: Set.finite_iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : ι → Set α
ht : ∀ i ∈ s, (t i).Finite
⊢ Set.Finite.{u} (α := α) (⋃ i ∈ s, t i)

Tactic:
hs.biUnion' ht

Premises used: Set.Finite.biUnion'
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
s : Set (Set α)
hs : s.Finite
H : ∀ t ∈ s, t.Finite
⊢ (⋃₀ s).Finite

Tactic:
simpa only [sUnion_eq_biUnion] using hs.biUnion H

Premises used: Set.sUnion_eq_biUnion, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : t ∈ s
hf : t.Finite
⊢ (⋂₀ s).Finite

Tactic:
hf.subset (sInter_subset_of_mem ht)

Premises used: Set.Finite.subset, Set.sInter_subset_of_mem
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
this : Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
(ht.biUnion hs).subset this

Premises used: Set.Finite.subset, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
this : Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
exact (ht.biUnion hs).subset this

Premises used: Set.Finite.subset, Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
suffices : Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
suffices ⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)

Tactic:
iUnion_subset fun i x hx => ?_

Premises used: Set.iUnion_subset
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
refine : ∀ (i : ι) (x : α) (hx : x ∈ s i), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
⊢ Subset.{u} (α := Set α) (⋃ (i : ι), s i) (⋃ i ∈ t, s i)

Tactic:
refine iUnion_subset fun i x hx => ?_

Premises used: Set.iUnion_subset
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
pos : ∀ (hi : i ∈ t), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
neg : ∀ (hi : i ∉ t), Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x

Tactic:
by_cases hi : i ∈ t
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x

Tactic:
mem_biUnion hi hx

Premises used: Set.mem_biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x

Tactic:
exact mem_biUnion hi hx

Premises used: Set.mem_biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ False

Tactic:
rw [he i hi, mem_empty_iff_false] at hx

Premises used: Set.mem_empty_iff_false
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
hx₁ : False
⊢ i ∉ t

Tactic:
rw [he i hi, mem_empty_iff_false] at hx

Premises used: Set.mem_empty_iff_false
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : False
hi : i ∉ t
⊢ Membership.mem (γ := Set α) (⋃ i ∈ t, s i) x

Tactic:
contradiction
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
⊢ (∀ (i : ι), (s i).Finite) ∧ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}

Tactic:
⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩

Premises used: Set.Finite.subset, Set.subset_iUnion, And.intro
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
refine : Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}
⊢ (∀ (i : ι), (s i).Finite) ∧ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}

Tactic:
refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
a :
  (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) : ι) =
    (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
⊢ Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi =
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj

Tactic:
ext
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) : ι) =
    (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)

Tactic:
hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩

Premises used: Iff.mpr, Exists.choose_spec, Pairwise.eq, Set.not_disjoint_iff, Subtype.mk, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
a :
  (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi)) : α) ∈
    s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) : ι) =
    (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)

Tactic:
refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩

Premises used: Iff.mpr, Pairwise.eq, Set.not_disjoint_iff, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
a :
  (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)) : α) ∈
    s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)
⊢ (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi)) : α) ∈
    s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)

Tactic:
rw [hij]
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
⊢ (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)) : α) ∈
    s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)

Tactic:
hj.choose_spec

Premises used: Exists.choose_spec, Set.Mem, Classical.choose
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} j
hij :
  u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) i hi) =
    u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)
⊢ (↑(u (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj)) : α) ∈
    s (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i : ι | (s i).Nonempty} x) j hj) : ι)

Tactic:
exact hj.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
⊢ Injective u

Tactic:
have u_inj : Function.Injective u := by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      ext
      refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
      rw [hij]
      exact hj.choose_spec
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
u_inj : Injective u
⊢ Finite.{u + 1} (↑(⋃ (i : ι), s i) : Type u)

Tactic:
have : Finite (⋃ i, s i) := h
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
u_inj : Injective u
this : Finite.{u + 1} (↑(⋃ (i : ι), s i) : Type u)
⊢ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}

Tactic:
.of_injective u u_inj

Premises used: Set.Finite, Finite.of_injective
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : Set.Finite.{u} (α := α) (⋃ (i : ι), s i)
u : (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) → (↑(⋃ (i : ι), s i) : Type u) :=
  fun (i : (↑{i : ι | (s i).Nonempty} : Type u_1)) ↦
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x)
      (Exists.choose (p := Membership.mem (s (↑i : ι))) ⋯) ⋯
u_inj : Injective u
this : Finite.{u + 1} (↑(⋃ (i : ι), s i) : Type u)
⊢ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}

Tactic:
exact .of_injective u u_inj
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun (i j : ι) ↦ Disjoint (s i) (s j)
h : (∀ (i : ι), (s i).Finite) ∧ Set.Finite.{u_1} (α := ι) {i : ι | (s i).Nonempty}
⊢ ∀ i ∉ {i : ι | (s i).Nonempty}, s i = ∅

Tactic:
simp [not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort u_1
s : ι → Set α
i : ι
hi : (s i).Infinite
⊢ Set.Infinite.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
fun h ↦ hi (h.subset (Set.subset_iUnion s i))

Premises used: Set.Finite.subset, Set.subset_iUnion, Not, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → Set α
i : ι
j : κ i
hij : (s i j).Infinite
⊢ Set.Infinite.{u} (α := α) (⋃ (i : ι), ⋃ (j : κ i), s i j)

Tactic:
fun hc ↦ hij (hc.subset <| subset_iUnion₂ _ _)

Premises used: Set.subset_iUnion₂, Set.Finite.subset, Not, Set.Infinite
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort u_1
inst : Subsingleton ι
s : ι → Set α
rw :
  (∀ (i : PLift ι), (s i.down).Finite) ∧ Set.Finite.{u_1} (α := PLift ι) {i : PLift ι | (s i.down).Nonempty} ↔
    ∀ (i : ι), (s i).Finite
⊢ Set.Finite.{u} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), (s i).Finite

Tactic:
rw [← iUnion_plift_down, finite_iUnion_iff _root_.Subsingleton.pairwise]

Premises used: Set.iUnion_plift_down, Set.finite_iUnion_iff, Subsingleton.pairwise
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
ι : Sort u_1
inst : Subsingleton ι
s : ι → Set α
⊢ (∀ (i : PLift ι), (s i.down).Finite) ∧ Set.Finite.{u_1} (α := PLift ι) {i : PLift ι | (s i.down).Nonempty} ↔
    ∀ (i : ι), (s i).Finite

Tactic:
simp [PLift.forall, Finite.of_subsingleton]

Premises used: PLift.forall, Set.Finite.of_subsingleton
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ Pairwise fun (i j : β) ↦ Disjoint.{u} (α := Set α) (⋃ (_ : i ∈ s), f i) (⋃ (_ : j ∈ s), f j)

Tactic:
aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise])

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Pairwise
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
rw :
  (∀ (i : β), Set.Finite.{u} (α := α) (⋃ (_ : i ∈ s), f i)) ∧
      Set.Finite.{v} (α := β) {i : β | Set.Nonempty.{u} (α := α) (⋃ (_ : i ∈ s), f i)} ↔
    (∀ i ∈ s, (f i).Finite) ∧ Set.Finite.{v} (α := β) {i : β | i ∈ s ∧ (f i).Nonempty}
⊢ Set.Finite.{u} (α := α) (⋃ i ∈ s, f i) ↔
    (∀ i ∈ s, (f i).Finite) ∧ Set.Finite.{v} (α := β) {i : β | i ∈ s ∧ (f i).Nonempty}

Tactic:
rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]

Premises used: Set.finite_iUnion_iff
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (∀ (i : β), Set.Finite.{u} (α := α) (⋃ (_ : i ∈ s), f i)) ∧
      Set.Finite.{v} (α := β) {i : β | Set.Nonempty.{u} (α := α) (⋃ (_ : i ∈ s), f i)} ↔
    (∀ i ∈ s, (f i).Finite) ∧ Set.Finite.{v} (α := β) {i : β | i ∈ s ∧ (f i).Nonempty}

Tactic:
simp
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
rw : Set.Finite.{u} (α := α) (⋃ y ∈ s, f ⁻¹' {y})
⊢ (f ⁻¹' s).Finite

Tactic:
rw [← Set.biUnion_preimage_singleton]

Premises used: Set.biUnion_preimage_singleton
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ Set.Finite.{u} (α := α) (⋃ y ∈ s, f ⁻¹' {y})

Tactic:
Set.Finite.biUnion h hf

Premises used: Set.Finite.biUnion
-- Module: Mathlib.Data.Set.Finite.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ Set.Finite.{u} (α := α) (⋃ y ∈ s, f ⁻¹' {y})

Tactic:
exact Set.Finite.biUnion h hf

Premises used: Set.Finite.biUnion