awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
⊢ Disjoint (accumulate s i) (s j)
have apply : ∀ (x : β) (hx : x ∈ accumulate s i), x ∉ s j
Tactic: apply disjoint_left.2 (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : x ∈ accumulate s i
⊢ x ∉ s j
have hx₁ : ∃ i_1 ≤ i, x ∈ s i_1
Tactic: simp only [accumulate, mem_iUnion, exists_prop] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : ∃ i_1 ≤ i, x ∈ s i_1
⊢ x ∉ s j
have rcases : ∀ (k : α) (hk : k ≤ i) (hx : x ∈ s k), x ∉ s j
Tactic: rcases hx with ⟨k, hk, hx⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
f : ℕ → Set α
⊢ (⇑(partialSups f) : (a : ℕ) → Set α) = accumulate f
have h : ∀ (n : ℕ) (x : α), Membership.mem (γ := Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α) x ↔ x ∈ accumulate f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ ∃ (m : ℕ), accumulate s 0 ⊆ s m
have h : accumulate s 0 ⊆ s 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n : ℕ
hn : ∃ (m : ℕ), accumulate s n ⊆ s m
⊢ ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
have succ : ∀ (m : ℕ) (hm : accumulate s n ⊆ s m), ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
Tactic: obtain ⟨m, hm⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
⊢ ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
have succ : ∀ (k : ℕ) (hk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s m) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s (n + 1)) (s k)),
  ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
Tactic: obtain ⟨k, hk⟩ := hd m (n + 1)
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s (n + 1) ⊆ s k
have simp : accumulate s n ⊆ s k ∧ s (n + 1) ⊆ s k
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n : ℕ
⊢ ∃ (m : ℕ), accumulate s n ⊆ s m
have zero : ∃ (m : ℕ), accumulate s 0 ⊆ s m
Tactic: induction n with
  | zero => use 0; simp [accumulate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    simp at hk
    exact ⟨k, by simp; grind⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n : ℕ
zero : ∃ (m : ℕ), accumulate s 0 ⊆ s m
⊢ ∃ (m : ℕ), accumulate s n ⊆ s m
have succ : ∀ (n : ℕ) (hn : ∃ (m : ℕ), accumulate s n ⊆ s m), ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
Tactic: induction n with
  | zero => use 0; simp [accumulate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    simp at hk
    exact ⟨k, by simp; grind⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ (∃ (n : ℕ), accumulate s n = univ) ↔ ∃ (n : ℕ), s n = univ
have refine : (∃ (n : ℕ), accumulate s n = univ) → ∃ (n : ℕ), s n = univ
Tactic: refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ (∃ (n : ℕ), accumulate s n = univ) → ∃ (n : ℕ), s n = univ
have contrapose! : (∀ (n : ℕ), s n ≠ univ) → ∀ (n : ℕ), accumulate s n ≠ univ
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
n : ℕ
⊢ accumulate s n ≠ univ
have obtain : ∀ (m : ℕ) (hm : accumulate s n ⊆ s m), accumulate s n ≠ univ
Tactic: obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ ¬Nonempty.{u + 1} (↑s : Type u) ↔ s = ∅
have rw : (¬∃ (a : α), a ∈ s) ↔ s = ∅
Tactic: rw [nonempty_subtype, not_exists, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
rw : (¬∃ (a : α), a ∈ s) ↔ s = ∅
⊢ ¬Nonempty.{u + 1} (↑s : Type u) ↔ s = ∅
have rw₁ : (∀ (x : α), ¬x ∈ s) ↔ s = ∅
Tactic: rw [nonempty_subtype, not_exists, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
rw : (¬∃ (a : α), a ∈ s) ↔ s = ∅
rw₁ : (∀ (x : α), ¬x ∈ s) ↔ s = ∅
⊢ ¬Nonempty.{u + 1} (↑s : Type u) ↔ s = ∅
have rw₂ : (∀ (x : α), ¬x ∈ s) ↔ ∀ (x : α), ¬x ∈ s
Tactic: rw [nonempty_subtype, not_exists, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s : Set α
⊢ s ≠ univ ↔ ∃ (a : α), ¬a ∈ s
have rw : s ≠ univ ↔ ¬∀ (x : α), x ∈ s
Tactic: rw [← not_forall, ← eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s : Set α
rw : s ≠ univ ↔ ¬∀ (x : α), x ∈ s
⊢ s ≠ univ ↔ ∃ (a : α), ¬a ∈ s
have rw₁ : s ≠ univ ↔ ¬s = univ
Tactic: rw [← not_forall, ← eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ s ⊂ univ ↔ sᶜ.Nonempty
have rw : (s ⊆ univ ∧ ∃ (a : α), ¬a ∈ s) ↔ ∃ (x : α), x ∈ sᶜ
Tactic: rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ sᶜ ⊂ univ ↔ s.Nonempty
have rw : (sᶜ ⊆ univ ∧ ∃ (a : α), ¬a ∈ sᶜ) ↔ ∃ (x : α), x ∈ s
Tactic: rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s t : Set α
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
have simp : s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅
Tactic: simp only [← subset_empty_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ {x : α | x ∈ s ∧ p x} = s ∩ {x : α | x ∈ t ∧ p x}
have rw : s ∩ {a : α | p a} = s ∩ {x : α | x ∈ t ∧ p x}
Tactic: rw [← inter_setOf_eq_sep s p, ← inter_setOf_eq_sep t p,
    ← inter_assoc, ← left_eq_inter.mpr hst]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
rw : s ∩ {a : α | p a} = s ∩ {x : α | x ∈ t ∧ p x}
⊢ {x : α | x ∈ s ∧ p x} = s ∩ {x : α | x ∈ t ∧ p x}
have rw₁ : s ∩ {a : α | p a} = s ∩ (t ∩ {a : α | p a})
Tactic: rw [← inter_setOf_eq_sep s p, ← inter_setOf_eq_sep t p,
    ← inter_assoc, ← left_eq_inter.mpr hst]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
rw : s ∩ {a : α | p a} = s ∩ {x : α | x ∈ t ∧ p x}
rw₁ : s ∩ {a : α | p a} = s ∩ (t ∩ {a : α | p a})
⊢ {x : α | x ∈ s ∧ p x} = s ∩ {x : α | x ∈ t ∧ p x}
have rw₂ : s ∩ {a : α | p a} = s ∩ t ∩ {a : α | p a}
Tactic: rw [← inter_setOf_eq_sep s p, ← inter_setOf_eq_sep t p,
    ← inter_assoc, ← left_eq_inter.mpr hst]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
rw : s ∩ {a : α | p a} = s ∩ {x : α | x ∈ t ∧ p x}
rw₁ : s ∩ {a : α | p a} = s ∩ (t ∩ {a : α | p a})
rw₂ : s ∩ {a : α | p a} = s ∩ t ∩ {a : α | p a}
⊢ {x : α | x ∈ s ∧ p x} = s ∩ {x : α | x ∈ t ∧ p x}
have rw₃ : s ∩ {a : α | p a} = s ∩ {a : α | p a}
Tactic: rw [← inter_setOf_eq_sep s p, ← inter_setOf_eq_sep t p,
    ← inter_assoc, ← left_eq_inter.mpr hst]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p q : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} {x : α | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
have simp_rw : (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ q x} x) ↔
  ∀ (x : α), x ∈ s → (p x ↔ q x)
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p q : α → Prop
simp_rw :
  (∀ (x : α),
      Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ q x} x) ↔
    ∀ (x : α), x ∈ s → (p x ↔ q x)
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} {x : α | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
have simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ s ∧ q x) ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p : α → Prop
⊢ {x : α | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x
have simp_rw : (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p : α → Prop
simp_rw : (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x
⊢ {x : α | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x
have simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
have simp_rw : (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) ∅ x) ↔
  ∀ (x : α), x ∈ s → ¬p x
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p : α → Prop
simp_rw :
  (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) ∅ x) ↔
    ∀ (x : α), x ∈ s → ¬p x
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
have simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ Membership.mem (γ := Set α) ∅ x) ↔ ∀ (x : α), x ∈ s → ¬p x
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p : α → Prop
simp_rw :
  (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) ∅ x) ↔
    ∀ (x : α), x ∈ s → ¬p x
simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ Membership.mem (γ := Set α) ∅ x) ↔ ∀ (x : α), x ∈ s → ¬p x
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
have simp_rw₂ : (∀ (x : α), x ∈ s ∧ p x ↔ False) ↔ ∀ (x : α), x ∈ s → ¬p x
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
s : Set α
p : α → Prop
simp_rw :
  (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) ∅ x) ↔
    ∀ (x : α), x ∈ s → ¬p x
simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ Membership.mem (γ := Set α) ∅ x) ↔ ∀ (x : α), x ∈ s → ¬p x
simp_rw₂ : (∀ (x : α), x ∈ s ∧ p x ↔ False) ↔ ∀ (x : α), x ∈ s → ¬p x
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
have simp_rw₃ : (∀ (x : α), ¬(x ∈ s ∧ p x)) ↔ ∀ (x : α), x ∈ s → ¬p x
Tactic: simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
⊢ Membership.mem (γ := Set α) (if h : p then univ else t h) x ↔ ∀ (h : ¬p), x ∈ t h
have pos : p → (Membership.mem (γ := Set α) univ x ↔ ∀ (h : ¬p), x ∈ t h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
pos : p → (Membership.mem (γ := Set α) univ x ↔ ∀ (h : ¬p), x ∈ t h)
⊢ Membership.mem (γ := Set α) (if h : p then univ else t h) x ↔ ∀ (h : ¬p), x ∈ t h
have neg : ∀ (h : ¬p), x ∈ t h ↔ ∀ (h : ¬p), x ∈ t h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
p : Prop
inst : Decidable p
t : p → Set α
x : α
⊢ Membership.mem (γ := Set α) (if h : p then t h else ∅) x ↔ ∃ (h : p), x ∈ t h
have simp : (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ (h : p), x ∈ t h
Tactic: simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
⊢ Membership.mem (γ := Set α) (if h : p then ∅ else t h) x ↔ ∃ (h : ¬p), x ∈ t h
have simp : (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h
Tactic: simp only [mem_dite, mem_empty_iff_false, imp_false]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ (f s).Nonempty ↔ s.Nonempty
have rw : f s ≠ ∅ ↔ s.Nonempty
Tactic: rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
rw : f s ≠ ∅ ↔ s.Nonempty
⊢ (f s).Nonempty ↔ s.Nonempty
have rw₁ : f s ≠ f ∅ ↔ s.Nonempty
Tactic: rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
rw : f s ≠ ∅ ↔ s.Nonempty
rw₁ : f s ≠ f ∅ ↔ s.Nonempty
⊢ (f s).Nonempty ↔ s.Nonempty
have rw₂ : f s ≠ f ∅ ↔ s ≠ ∅
Tactic: rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
rw : f s ≠ ∅ ↔ s.Nonempty
rw₁ : f s ≠ f ∅ ↔ s.Nonempty
rw₂ : f s ≠ f ∅ ↔ s ≠ ∅
⊢ (f s).Nonempty ↔ s.Nonempty
have rw₃ : s ≠ ∅ ↔ s ≠ ∅
Tactic: rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : Set { a : α // p a }
⊢ (fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
        ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
      ((fun (s : Set { a : α // p a }) ↦
          (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
              {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
            { s : Set α // ∀ (a : α), a ∈ s → p a }))
        s) =
    s
have h : ∀ (a : { a : α // p a }),
  Membership.mem (γ := Set { a : α // p a })
      ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
          ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
        ((fun (s : Set { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} sorry :
              { s : Set α // ∀ (a : α), a ∈ s → p a }))
          s))
      a ↔
    a ∈ s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Set.Basic (goal)
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : { s : Set α // ∀ (a : α), a ∈ s → p a }
⊢ (fun (s : Set { a : α // p a }) ↦
        (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
            {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
          { s : Set α // ∀ (a : α), a ∈ s → p a }))
      ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
          ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
        s) =
    s
have a : ∀ (x : α),
  Membership.mem (γ := Set α)
      (↑((fun (s : Set { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                  {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} sorry :
                { s : Set α // ∀ (a : α), a ∈ s → p a }))
            ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
                ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
              s)) :
        Set α)
      x ↔
    x ∈ (↑s : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true
have pos : ∀ (h : x ∈ s), x ∈ s ↔ true = true
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
x : α
pos : ∀ (h : x ∈ s), x ∈ s ↔ true = true
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true
have neg : ∀ (h : ¬x ∈ s), x ∈ s ↔ False
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false
have pos : ∀ (h : x ∈ s), ¬x ∈ s ↔ False
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
x : α
pos : ∀ (h : x ∈ s), ¬x ∈ s ↔ False
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false
have neg : ∀ (h : ¬x ∈ s), ¬x ∈ s ↔ false = false
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
⊢ s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have h : ∀ (x : α), x ∈ s.boolIndicator ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ x ∈ s.boolIndicator ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have h : (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
Tactic: simp only [boolIndicator, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have neg₁ : x ∈ s → ¬true ∈ t → ¬false ∈ t → (true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
neg₁ : x ∈ s → ¬true ∈ t → ¬false ∈ t → (true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have pos₂ : ¬x ∈ s → true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ s ∪ sᶜ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
neg₁ : x ∈ s → ¬true ∈ t → ¬false ∈ t → (true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
pos₂ : ¬x ∈ s → true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ s ∪ sᶜ)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have neg₂ : ¬x ∈ s → true ∈ t → ¬false ∈ t → (false ∈ t ↔ x ∈ s ∪ ∅)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
neg₁ : x ∈ s → ¬true ∈ t → ¬false ∈ t → (true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
pos₂ : ¬x ∈ s → true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ s ∪ sᶜ)
neg₂ : ¬x ∈ s → true ∈ t → ¬false ∈ t → (false ∈ t ↔ x ∈ s ∪ ∅)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have pos₃ : ¬x ∈ s → ¬true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ ∅ ∪ sᶜ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
neg₁ : x ∈ s → ¬true ∈ t → ¬false ∈ t → (true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
pos₂ : ¬x ∈ s → true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ s ∪ sᶜ)
neg₂ : ¬x ∈ s → true ∈ t → ¬false ∈ t → (false ∈ t ↔ x ∈ s ∪ ∅)
pos₃ : ¬x ∈ s → ¬true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ ∅ ∪ sᶜ)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
have neg₃ : ¬x ∈ s → ¬true ∈ t → ¬false ∈ t → (false ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
⊢ s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅
have simp : ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
  ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
Tactic: simp only [preimage_boolIndicator_eq_union]
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
have pos : true ∈ t → false ∈ t → s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
pos : true ∈ t → false ∈ t → s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
have neg : true ∈ t → ¬false ∈ t → s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅
Tactic: split_ifs