awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s : Set α
⊢ ⋃ (_ : s.Nonempty), s = s
have rw : ⋃ x ∈ s, s = s
Tactic: rw [iUnion_nonempty_index, biUnion_self]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s : Set α
rw : ⋃ x ∈ s, s = s
⊢ ⋃ (_ : s.Nonempty), s = s
have rw₁ : s = s
Tactic: rw [iUnion_nonempty_index, biUnion_self]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) {a, b} x), s x = s a ∩ s b
have rw : s a ∩ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) {b} x), s x = s a ∩ s b
Tactic: rw [biInter_insert, biInter_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
a b : α
s : α → Set β
rw : s a ∩ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) {b} x), s x = s a ∩ s b
⊢ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) {a, b} x), s x = s a ∩ s b
have rw₁ : s a ∩ s b = s a ∩ s b
Tactic: rw [biInter_insert, biInter_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
Goal:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
have this : Nonempty.{u_12 + 1} (↑s : Type u_12)
Tactic: haveI : Nonempty s := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i
have rw : Eq.{u_13 + 1} (α := Set α) (⋂ i ∈ s, t ∩ f i) (⋂ i ∈ s, f i ∩ t)
Tactic: rw [inter_comm, ← biInter_inter hs]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ
have rw : (⋃₀ S)ᶜᶜ = (⋂₀ (compl '' S))ᶜ
Tactic: rw [← compl_compl (⋃₀ S), compl_sUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : (⋃₀ S)ᶜᶜ = (⋂₀ (compl '' S))ᶜ
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ
have rw₁ : (⋂₀ (compl '' S))ᶜ = (⋂₀ (compl '' S))ᶜ
Tactic: rw [← compl_compl (⋃₀ S), compl_sUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)
have rw : (⋂₀ S)ᶜ = (⋂₀ (compl '' compl '' S))ᶜ
Tactic: rw [sUnion_eq_compl_sInter_compl, compl_compl_image]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : (⋂₀ S)ᶜ = (⋂₀ (compl '' compl '' S))ᶜ
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)
have rw₁ : (⋂₀ S)ᶜ = (⋂₀ S)ᶜ
Tactic: rw [sUnion_eq_compl_sInter_compl, compl_compl_image]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ
have rw : (⋂₀ S)ᶜᶜ = (⋃₀ (compl '' S))ᶜ
Tactic: rw [← compl_compl (⋂₀ S), compl_sInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
S : Set (Set α)
rw : (⋂₀ S)ᶜᶜ = (⋃₀ (compl '' S))ᶜ
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ
have rw₁ : (⋃₀ (compl '' S))ᶜ = (⋃₀ (compl '' S))ᶜ
Tactic: rw [← compl_compl (⋂₀ S), compl_sInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ ∅
have rw : s ∩ t ⊆ s ∩ ⋃₀ S
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
⊢ ⋃ (i : ι), Sigma.mk (β := fun (i : ι) ↦ σ i) i '' Sigma.mk (β := σ) i ⁻¹' s = s
have h : ∀ (x : (i : ι) × σ i),
  Membership.mem (γ := Set ((i : ι) × σ i))
      (⋃ (i : ι), Sigma.mk (β := fun (i : ι) ↦ σ i) i '' Sigma.mk (β := σ) i ⁻¹' s) x ↔
    x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ Membership.mem (γ := Set ((i : ι) × σ i))
      (⋃ (i : ι), Sigma.mk (β := fun (i : ι) ↦ σ i) i '' Sigma.mk (β := σ) i ⁻¹' s) x ↔
    x ∈ s
have h : (∃ (i : ι) (x_1 : σ i), Sigma.mk (β := σ) i x_1 ∈ s ∧ Sigma.mk (β := fun (i : ι) ↦ σ i) i x_1 = x) ↔ x ∈ s
Tactic: simp only [mem_iUnion, mem_image, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ (x : α), {f x} = range f
have h : ∀ (x : β), Membership.mem (γ := Set β) (⋃ (x : α), {f x}) x ↔ x ∈ range f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ (i : ι), insert (x i) (t i) = range x ∪ ⋃ (i : ι), t i
have simp_rw : ⋃ (i : ι), t i ∪ {x i} = range x ∪ ⋃ (i : ι), t i
Tactic: simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
simp_rw : ⋃ (i : ι), t i ∪ {x i} = range x ∪ ⋃ (i : ι), t i
⊢ ⋃ (i : ι), insert (x i) (t i) = range x ∪ ⋃ (i : ι), t i
have simp_rw₁ : (⋃ (i : ι), t i) ∪ ⋃ (i : ι), {x i} = range x ∪ ⋃ (i : ι), t i
Tactic: simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
simp_rw : ⋃ (i : ι), t i ∪ {x i} = range x ∪ ⋃ (i : ι), t i
simp_rw₁ : (⋃ (i : ι), t i) ∪ ⋃ (i : ι), {x i} = range x ∪ ⋃ (i : ι), t i
⊢ ⋃ (i : ι), insert (x i) (t i) = range x ∪ ⋃ (i : ι), t i
have simp_rw₂ : (⋃ (i : ι), t i) ∪ ⋃ (i : ι), {x i} = (⋃ (i : ι), t i) ∪ range x
Tactic: simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ i ∈ s, i
have rw : ⋃₀ s = ⋃₀ ((fun (i : Set α) ↦ i) '' s)
Tactic: rw [← sUnion_image, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s : Set (Set α)
rw : ⋃₀ s = ⋃₀ ((fun (i : Set α) ↦ i) '' s)
⊢ ⋃₀ s = ⋃ i ∈ s, i
have rw₁ : ⋃₀ s = ⋃₀ s
Tactic: rw [← sUnion_image, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i ∈ s, i
have rw : ⋂₀ s = ⋂₀ ((fun (i : Set α) ↦ i) '' s)
Tactic: rw [← sInter_image, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
s : Set (Set α)
rw : ⋂₀ s = ⋂₀ ((fun (i : Set α) ↦ i) '' s)
⊢ ⋂₀ s = ⋂ i ∈ s, i
have rw₁ : ⋂₀ s = ⋂₀ s
Tactic: rw [← sInter_image, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) = ⋃₀ C
have h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x ↔ x ∈ ⋃₀ C
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : α
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x ↔ x ∈ ⋃₀ C
have h : Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x → x ∈ ⋃₀ C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : α
h : Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x → x ∈ ⋃₀ C
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x ↔ x ∈ ⋃₀ C
have h₁ : x ∈ ⋃₀ C → Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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) ∈ ⋃₀ C
have h : (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) ∈ s
Tactic: refine ⟨_, hs, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x
have 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
Tactic: obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
have h : (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) = x
Tactic: refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → (↑(C x) : Type u_1)
hf : ∀ (x : ι), Surjective (f x)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (y : β), range fun (x : ι) ↦ (↑(f x y) : α)) (⋃ (x : ι), C x)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃ (y : β), range fun (x : ι) ↦ (↑(f x y) : α)) x ↔
    Membership.mem (γ := Set α) (⋃ (x : ι), C x) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : α
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (x : ι) ↦ (↑(f x y) : α)) x ↔
    Membership.mem (γ := Set α) (⋃ (x : ι), C x) x
have h : (∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) ↔ ∃ (i : ι), x ∈ C i
Tactic: rw [mem_iUnion, mem_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) ↔ ∃ (i : ι), x ∈ C i
have h : (∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) → ∃ (i : ι), x ∈ C i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
⊢ (∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x) ↔ ∃ (i : ι), x ∈ C i
have h₁ : (∃ (i : ι), x ∈ C i) → ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
⊢ ∃ (i : β), Membership.mem (γ := Set α) (range fun (x : ι) ↦ (↑(f x i) : α)) x
have 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
Tactic: obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι ⊕ σ), Sum.elim s t x) ((⋃ (x : ι), s x) ∪ ⋃ (x : σ), t x)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃ (x : ι ⊕ σ), Sum.elim s t x) x ↔
    Membership.mem (γ := Set α) ((⋃ (x : ι), s x) ∪ ⋃ (x : σ), t x) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
⊢ i.pi (α := π) s = ⋂ a ∈ i, eval (β := π) a ⁻¹' s a
have h : ∀ (x : (i : α) → π i),
  x ∈ i.pi (α := π) s ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ a ∈ i, eval (β := π) a ⁻¹' s a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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)
have 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
Tactic: refine diff_subset_comm.2 fun x hx a ha => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
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
⊢ x a ∈ t a
have 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
Tactic: simp only [mem_diff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
⊢ Eq (α := Set ((i : α) → π i)) (⋃ (x : (a : α) → ι a), pi (α := π) univ fun (a : α) ↦ t a (x a))
    (pi (α := π) univ fun (a : α) ↦ ⋃ (j : ι a), t a j)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
⊢ pi (α := π) (⋃ (i : α'), s i) t = ⋂ (i : α'), (s i).pi (α := π) t
have h : ∀ (f : (i : α) → π i),
  f ∈ pi (α := π) (⋃ (i : α'), s i) t ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ (i : α'), (s i).pi (α := π) t) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
⊢ f ∈ pi (α := π) (⋃ (i : α'), s i) t ↔ Membership.mem (γ := Set ((i : α) → π i)) (⋂ (i : α'), (s i).pi (α := π) t) f
have h : (∀ (i : α) (x : α') (h : i ∈ s x), f i ∈ t i) ↔ ∀ (i : α'), ∀ i_1 ∈ s i, f i_1 ∈ t i_1
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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)
⊢ DirectedOn r (⋃ (x : ι), f x)
have 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
Tactic: simp only [DirectedOn, mem_iUnion, exists_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 (⋃₀ S)
have rw : DirectedOn r (⋃ (i : (↑S : Type u_1)), (↑i : Set α))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 ι
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, Es i)ᶜ (⋃ i ∈ Iᶜ, Es i)
have h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : α
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
have h : ∀ (i : ι) (hix : x ∈ Es i),
  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]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
have refine : ∀ (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⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
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
have x_in_U₁ : ∃ i ∈ J, x ∈ Es i
Tactic: simp only [mem_iUnion, exists_prop] at x_in_U
Cleared hypotheses: x_in_U
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 : ∃ i ∈ J, x ∈ Es i
⊢ i ∈ J
have obtain : ∀ (j : ι) (j_in_J : j ∈ J) (hjx : x ∈ Es j), i ∈ J
Tactic: obtain ⟨j, j_in_J, hjx⟩ := x_in_U
Cleared hypotheses: x_in_U
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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 ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
⊢ i = j
have by_contra : ∀ (i_ne_j : ¬i = j), False
Tactic: by_contra i_ne_j
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
have obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
Tactic: have obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J := by
    refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩
    intro x_in_U
    simp only [mem_iUnion, exists_prop] at x_in_U
    obtain ⟨j, j_in_J, hjx⟩ := x_in_U
    rwa [show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
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
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
have obs' : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J
Tactic: have obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J :=
    fun J ↦ by simpa only [mem_compl_iff, not_iff_not] using obs J
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
obs' : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
have h : Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ i ∈ Iᶜ
Tactic: rw [obs, obs', mem_compl_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
obs' : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J
h : Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ i ∈ Iᶜ
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
have h₁ : i ∉ I ↔ i ∈ Iᶜ
Tactic: rw [obs, obs', mem_compl_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
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
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
obs' : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J
h : Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ i ∈ Iᶜ
h₁ : i ∉ I ↔ i ∈ Iᶜ
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x
have h₂ : i ∉ I ↔ i ∉ I
Tactic: rw [obs, obs', mem_compl_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
⊢ ⋂ (i : ι), Iic (f i) = lowerBounds (range f)
have h : ∀ (c : α), Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) c ↔ c ∈ lowerBounds (range f)
Tactic: ext c
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (hypothesis)
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ι), Iic (f i)) ↔ BddBelow (range f)
have this : ⋂ (i : ι), Iic (f i) = lowerBounds (range f)
Tactic: have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
    ext c; simp [lowerBounds]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ Ici (sSup s) = ⋂ a ∈ s, Ici a
have rw : Eq.{u_1 + 1} (α := Set α) (Ici (⨆ a ∈ s, a)) (⋂ a ∈ s, Ici a)
Tactic: rw [sSup_eq_iSup, Ici_iSup₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : Eq.{u_1 + 1} (α := Set α) (Ici (⨆ a ∈ s, a)) (⋂ a ∈ s, Ici a)
⊢ Ici (sSup s) = ⋂ a ∈ s, Ici a
have rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ s, Ici i) (⋂ a ∈ s, Ici a)
Tactic: rw [sSup_eq_iSup, Ici_iSup₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ Iic (sInf s) = ⋂ a ∈ s, Iic a
have rw : Eq.{u_1 + 1} (α := Set α) (Iic (⨅ a ∈ s, a)) (⋂ a ∈ s, Iic a)
Tactic: rw [sInf_eq_iInf, Iic_iInf₂]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : Eq.{u_1 + 1} (α := Set α) (Iic (⨅ a ∈ s, a)) (⋂ a ∈ s, Iic a)
⊢ Iic (sInf s) = ⋂ a ∈ s, Iic a
have rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ s, Iic i) (⋂ a ∈ s, Iic a)
Tactic: rw [sInf_eq_iInf, Iic_iInf₂]