awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) ∈ s

Tactic:
exact (f ⟨s, hs⟩ y).2

Premises used: Subtype.mk, Subtype.property
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
h :
  ∀ (y : β)
    (hy :
      f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) y =
        Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) : Set α)) x hx),
    Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x

Tactic:
obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy :
  f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) y =
    Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) : Set α)) x hx
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x

Tactic:
⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩

Premises used: Set.Mem, iSup, setOf, Subtype.mk, And.intro, Exists.intro, Set.iUnion, rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy :
  f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) y =
    Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) : Set α)) x hx
h : (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) = x
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x

Tactic:
refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy :
  f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) y =
    Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) : Set α)) x hx
⊢ (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) = x

Tactic:
congr_arg Subtype.val hy

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy :
  f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) y =
    Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) : Set α)) x hx
⊢ (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) = x

Tactic:
exact congr_arg Subtype.val hy

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (y : β), range fun (x : ι) ↦ (↑(f x y) : α)) x ↔
      Membership.mem (γ := Set α) (⋃ (x : ι), C x) x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (y : β), range fun (x : ι) ↦ (↑(f x y) : α)) (⋃ (x : ι), C x)

Tactic:
ext x
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
x : α
h : (∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) ↔ ∃ (i : ι), x ∈ C i
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (x : ι) ↦ (↑(f x y) : α)) x ↔
    Membership.mem (γ := Set α) (⋃ (x : ι), C x) x

Tactic:
rw [mem_iUnion, mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
x : α
h : (∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) → ∃ (i : ι), x ∈ C i
h₁ : (∃ (i : ι), x ∈ C i) → ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x
⊢ (∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) ↔ ∃ (i : ι), x ∈ C i

Tactic:
constructor
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ (i_1 : ι), (fun (x : ι) ↦ (↑(f x y) : α)) i ∈ C i_1

Tactic:
⟨i, (f i y).2⟩

Premises used: Exists.intro, Subtype.property
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ (i_1 : ι), (fun (x : ι) ↦ (↑(f x y) : α)) i ∈ C i_1

Tactic:
exact ⟨i, (f i y).2⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
h :
  ∀ (y : β) (hy : f i y = Subtype.mk (p := fun (x : α) ↦ x ∈ C i) x hx),
    ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x
⊢ ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x

Tactic:
obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
y : β
hy : f i y = Subtype.mk (p := fun (x : α) ↦ x ∈ C i) x hx
⊢ ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x

Tactic:
⟨y, i, congr_arg Subtype.val hy⟩

Premises used: congr_arg, Exists.intro, Subtype.val
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
y : β
hy : f i y = Subtype.mk (p := fun (x : α) ↦ x ∈ C i) x hx
⊢ ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x

Tactic:
exact ⟨y, i, congr_arg Subtype.val hy⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (x : ι ⊕ σ), Sum.elim s t x) x ↔
      Membership.mem (γ := Set α) ((⋃ (x : ι), s x) ∪ ⋃ (x : σ), t x) x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι ⊕ σ), Sum.elim s t x) ((⋃ (x : ι), s x) ∪ ⋃ (x : σ), t x)

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
x : α
⊢ Membership.mem (γ := Set α) (⋃ (x : ι ⊕ σ), Sum.elim s t x) x ↔
    Membership.mem (γ := Set α) ((⋃ (x : ι), s x) ∪ ⋃ (x : σ), t x) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
t : Set α
⊢ t ∪ ⋂ (i : ι), s i = ⋂ (i : ι), t ∪ s i

Tactic:
sup_iInf_eq _ _

Premises used: Set.iInter, sup_iInf_eq
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ (i : ι), ⋂ (j : κ i), t i j = ⋂ (i : ι), ⋂ (j : κ i), s ∪ t i j

Tactic:
simp_rw [union_distrib_iInter_left]

Premises used: Set.union_distrib_iInter_left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
t : Set α
⊢ (⋂ (i : ι), s i) ∪ t = ⋂ (i : ι), s i ∪ t

Tactic:
iInf_sup_eq _ _

Premises used: Set.iInter, iInf_sup_eq
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι), ⋂ (j : κ i), s i j) ∪ t = ⋂ (i : ι), ⋂ (j : κ i), s i j ∪ t

Tactic:
simp_rw [union_distrib_iInter_right]

Premises used: Set.union_distrib_iInter_right
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : NoMaxOrder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (n : α), ⋃ (m : α), ⋃ (_ : m < n), s m) (⋃ (n : α), s n)

Tactic:
biSup_lt_eq_iSup

Premises used: biSup_lt_eq_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (n : α), ⋃ (m : α), ⋃ (_ : m ≤ n), s m) (⋃ (n : α), s n)

Tactic:
biSup_le_eq_iSup

Premises used: biSup_le_eq_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : NoMaxOrder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (n : α), ⋂ (m : α), ⋂ (_ : m < n), s m) (⋂ (n : α), s n)

Tactic:
biInf_lt_eq_iInf

Premises used: biInf_lt_eq_iInf, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (n : α), ⋂ (m : α), ⋂ (_ : m ≤ n), s m) (⋂ (n : α), s n)

Tactic:
biInf_le_eq_iInf

Premises used: Set.iInter, biInf_le_eq_iInf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : NoMinOrder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (n : α), ⋃ (m : α), ⋃ (_ : m > n), s m) (⋃ (n : α), s n)

Tactic:
biSup_gt_eq_iSup

Premises used: biSup_gt_eq_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (n : α), ⋃ (m : α), ⋃ (_ : m ≥ n), s m) (⋃ (n : α), s n)

Tactic:
biSup_ge_eq_iSup

Premises used: Set.iUnion, biSup_ge_eq_iSup
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : NoMinOrder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (n : α), ⋂ (m : α), ⋂ (_ : m > n), s m) (⋂ (n : α), s n)

Tactic:
biInf_gt_eq_iInf

Premises used: biInf_gt_eq_iInf, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (n : α), ⋂ (m : α), ⋂ (_ : m ≥ n), s m) (⋂ (n : α), s n)

Tactic:
biInf_ge_eq_iInf

Premises used: Set.iInter, biInf_ge_eq_iInf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
inst : PartialOrder ι
s : ι → Set α
i : ι
⊢ ⋃ (j : ι), ⋃ (_ : j ≤ i), s j = (⋃ (j : ι), ⋃ (_ : j < i), s j) ∪ s i

Tactic:
biSup_le_eq_sup s i

Premises used: biSup_le_eq_sup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
inst : PartialOrder ι
s : ι → Set α
i : ι
⊢ ⋂ (j : ι), ⋂ (_ : j ≤ i), s j = (⋂ (j : ι), ⋂ (_ : j < i), s j) ∩ s i

Tactic:
biInf_le_eq_inf s i

Premises used: Set.iInter, biInf_le_eq_inf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
inst : PartialOrder ι
s : ι → Set α
i : ι
⊢ ⋃ (j : ι), ⋃ (_ : j ≥ i), s j = s i ∪ ⋃ (j : ι), ⋃ (_ : j > i), s j

Tactic:
biSup_ge_eq_sup s i

Premises used: biSup_ge_eq_sup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
inst : PartialOrder ι
s : ι → Set α
i : ι
⊢ ⋂ (j : ι), ⋂ (_ : j ≥ i), s j = s i ∩ ⋂ (j : ι), ⋂ (_ : j > i), s j

Tactic:
biInf_ge_eq_inf s i

Premises used: Set.iInter, biInf_ge_eq_inf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
h :
  ∀ (x : (i : α) → π i),
    x ∈ i.pi (α := π) s ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ a ∈ i, eval (β := π) a ⁻¹' s a) x
⊢ i.pi (α := π) s = ⋂ a ∈ i, eval (β := π) a ⁻¹' s a

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
x : (i : α) → π i
⊢ x ∈ i.pi (α := π) s ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ a ∈ i, eval (β := π) a ⁻¹' s a) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
t : (i : α) → Set (π i)
⊢ pi (α := π) univ t = ⋂ (i : α), eval (β := π) i ⁻¹' t i

Tactic:
simp only [pi_def, iInter_true, mem_univ]

Premises used: Set.mem_univ, Set.iInter_true, Set.pi_def
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
⊢ i.pi (α := π) s \ i.pi (α := π) t ⊆ ⋃ a ∈ i, eval (β := π) a ⁻¹' (s a \ t a)

Tactic:
diff_subset_comm.2 fun x hx a ha => ?_

Premises used: Iff.mpr, Set.diff_subset_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
refine :
  ∀ (x : (i : α) → π i) (hx : x ∈ i.pi (α := π) s \ ⋃ a ∈ i, eval (β := π) a ⁻¹' (s a \ t a)) (a : α) (ha : a ∈ i),
    x a ∈ t a
⊢ i.pi (α := π) s \ i.pi (α := π) t ⊆ ⋃ a ∈ i, eval (β := π) a ⁻¹' (s a \ t a)

Tactic:
refine diff_subset_comm.2 fun x hx a ha => ?_
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ i.pi (α := π) s \ ⋃ a ∈ i, eval (β := π) a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ (x_1 : α) (x_2 : x_1 ∈ i), eval (β := π) x_1 x ∈ s x_1 → eval (β := π) x_1 x ∈ t x_1

Tactic:
simp only [mem_diff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not] at hx

Premises used: Classical.not_not, Set.mem_iUnion, not_exists, Set.mem_pi, Set.mem_diff, not_and, Set.mem_preimage
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ (x_1 : α) (x_2 : x_1 ∈ i), eval (β := π) x_1 x ∈ s x_1 → eval (β := π) x_1 x ∈ t x_1
⊢ x a ∈ t a

Tactic:
hx.2 _ ha (hx.1 _ ha)

Premises used: Set.Mem, And.right, And.left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ (x_1 : α) (x_2 : x_1 ∈ i), eval (β := π) x_1 x ∈ s x_1 → eval (β := π) x_1 x ∈ t x_1
⊢ x a ∈ t a

Tactic:
exact hx.2 _ ha (hx.1 _ ha)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
h :
  ∀ (x : (i : α) → π i),
    Membership.mem (γ := Set ((i : α) → π i)) (⋃ (x : (a : α) → ι a), pi (α := π) univ fun (a : α) ↦ t a (x a)) x ↔
      Membership.mem (γ := Set ((i : α) → π i)) (pi (α := π) univ fun (a : α) ↦ ⋃ (j : ι a), t a j) x
⊢ Eq (α := Set ((i : α) → π i)) (⋃ (x : (a : α) → ι a), pi (α := π) univ fun (a : α) ↦ t a (x a))
    (pi (α := π) univ fun (a : α) ↦ ⋃ (j : ι a), t a j)

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
x : (i : α) → π i
⊢ Membership.mem (γ := Set ((i : α) → π i)) (⋃ (x : (a : α) → ι a), pi (α := π) univ fun (a : α) ↦ t a (x a)) x ↔
    Membership.mem (γ := Set ((i : α) → π i)) (pi (α := π) univ fun (a : α) ↦ ⋃ (j : ι a), t a j) x

Tactic:
simp [Classical.skolem]

Premises used: Classical.skolem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
h :
  ∀ (x : (i : α) → π i),
    Membership.mem (γ := Set ((i : α) → π i)) (⋃ x ∈ pi (α := ι) univ s, pi (α := π) univ fun (a : α) ↦ t a (x a)) x ↔
      Membership.mem (γ := Set ((i : α) → π i)) (pi (α := π) univ fun (a : α) ↦ ⋃ j ∈ s a, t a j) x
⊢ Eq (α := Set ((i : α) → π i)) (⋃ x ∈ pi (α := ι) univ s, pi (α := π) univ fun (a : α) ↦ t a (x a))
    (pi (α := π) univ fun (a : α) ↦ ⋃ j ∈ s a, t a j)

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
x : (i : α) → π i
⊢ Membership.mem (γ := Set ((i : α) → π i)) (⋃ x ∈ pi (α := ι) univ s, pi (α := π) univ fun (a : α) ↦ t a (x a)) x ↔
    Membership.mem (γ := Set ((i : α) → π i)) (pi (α := π) univ fun (a : α) ↦ ⋃ j ∈ s a, t a j) x

Tactic:
simp [Classical.skolem, forall_and]

Premises used: Classical.skolem, forall_and
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
h :
  ∀ (f : (i : α) → π i),
    f ∈ pi (α := π) (⋃ (i : α'), s i) t ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ (i : α'), (s i).pi (α := π) t) f
⊢ pi (α := π) (⋃ (i : α'), s i) t = ⋂ (i : α'), (s i).pi (α := π) t

Tactic:
ext f
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
h : (∀ (i : α) (x : α') (h : i ∈ s x), f i ∈ t i) ↔ ∀ (i : α'), ∀ i_1 ∈ s i, f i_1 ∈ t i_1
⊢ f ∈ pi (α := π) (⋃ (i : α'), s i) t ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ (i : α'), (s i).pi (α := π) t) f

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
⊢ (∀ (i : α) (x : α') (h : i ∈ s x), f i ∈ t i) ↔ ∀ (i : α'), ∀ i_1 ∈ s i, f i_1 ∈ t i_1

Tactic:
grind
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
simp : ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ (z : α), (∃ (i : ι), z ∈ f i) ∧ r x z ∧ r y z
⊢ DirectedOn r (⋃ (x : ι), f x)

Tactic:
simp only [DirectedOn, mem_iUnion, exists_imp]

Premises used: Set.mem_iUnion, DirectedOn, exists_imp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ (z : α), (∃ (i : ι), z ∈ f i) ∧ r x z ∧ r y z

Tactic:
fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
    let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
    let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
    ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩

Premises used: Membership.mem, Exists, _private.0.Set.directedOn_iUnion.match_2, And, And.intro, Exists.intro, _private.0.Set.directedOn_iUnion.match_1
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ (z : α), (∃ (i : ι), z ∈ f i) ∧ r x z ∧ r y z

Tactic:
exact fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
    let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
    let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
    ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
rw : DirectedOn r (⋃ (i : (↑S : Type u_1)), (↑i : Set α))
⊢ DirectedOn r (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ (i : (↑S : Type u_1)), (↑i : Set α))

Tactic:
directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

Premises used: directedOn_iff_directed, Iff.mp, Set.directedOn_iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ (i : (↑S : Type u_1)), (↑i : Set α))

Tactic:
exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

Premises used: directedOn_iff_directed, Iff.mp, Set.directedOn_iUnion, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι₂ : Sort u_7
f : ι → ι₂
hf : Surjective f
g : ι₂ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι), g (f x)) (⋃ (y : ι₂), g y)

Tactic:
hf.iSup_comp g

Premises used: Function.Surjective.iSup_comp, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι₂ : Sort u_7
f : ι → ι₂
hf : Surjective f
g : ι₂ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (x : ι), g (f x)) (⋂ (y : ι₂), g y)

Tactic:
hf.iInf_comp g

Premises used: Set.iInter, Function.Surjective.iInf_comp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
t : Set α
ι : Sort u_12
s : ι → Set α
⊢ Disjoint (⋃ (i : ι), s i) t ↔ ∀ (i : ι), Disjoint (s i) t

Tactic:
iSup_disjoint_iff

Premises used: iSup_disjoint_iff, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
t : Set α
ι : Sort u_12
s : ι → Set α
⊢ Disjoint t (⋃ (i : ι), s i) ↔ ∀ (i : ι), Disjoint t (s i)

Tactic:
disjoint_iSup_iff

Premises used: disjoint_iSup_iff, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ Disjoint (⋃ (i : ι), ⋃ (j : κ i), s i j) t ↔ ∀ (i : ι) (j : κ i), Disjoint (s i j) t

Tactic:
iSup₂_disjoint_iff

Premises used: iSup₂_disjoint_iff, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ Disjoint s (⋃ (i : ι), ⋃ (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), Disjoint s (t i j)

Tactic:
disjoint_iSup₂_iff

Premises used: Set.iUnion, disjoint_iSup₂_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
t : Set α
⊢ Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t

Tactic:
sSup_disjoint_iff

Premises used: sSup_disjoint_iff, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
S : Set (Set α)
⊢ Disjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t

Tactic:
disjoint_sSup_iff

Premises used: Set.sUnion, disjoint_sSup_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, Es i)ᶜ (⋃ i ∈ Iᶜ, Es i)

Tactic:
ext x
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
⊢ ∃ (i : ι), x ∈ Es i

Tactic:
simp [← mem_iUnion, Es_union]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
h :
  ∀ (i : ι) (hix : x ∈ Es i),
    Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x

Tactic:
obtain ⟨i, hix⟩ : ∃ i, x ∈ Es i := by simp [← mem_iUnion, Es_union]
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
i_in_J : i ∈ J
⊢ Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x

Tactic:
simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
refine : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x → i ∈ J
⊢ ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J

Tactic:
refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
x_in_U : Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x
⊢ ∃ i ∈ J, x ∈ Es i

Tactic:
simp only [mem_iUnion, exists_prop] at x_in_U

Premises used: Set.mem_iUnion, exists_prop