awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v
have huv₁ : Ne.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [hu, hv] at huv
Cleared hypotheses: huv, hu, hv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
⊢ Disjoint u v
have hu₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u
Tactic: rw [memPartition_succ] at hu hv
Cleared hypotheses: hu, hv, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
hu₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u
⊢ Disjoint u v
have hv₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v
Tactic: rw [memPartition_succ] at hu hv
Cleared hypotheses: hu, hv, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u
hv : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v
huv : u ≠ v
⊢ Disjoint u v
have succ : ∀ (u' : Set α) (hu' : u' ∈ memPartition f n) (hu'_eq : u = u' ∩ f n ∨ u = u' \ f n), Disjoint u v
Tactic: obtain ⟨u', hu', hu'_eq⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hv : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
⊢ Disjoint u v
have succ : ∀ (v' : Set α) (hv' : v' ∈ memPartition f n) (hv'_eq : v = v' ∩ f n ∨ v = v' \ f n), Disjoint u v
Tactic: obtain ⟨v', hv', hv'_eq⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
⊢ Disjoint u v
have succ : ∀ (huv : u' ∩ f n ≠ v), Disjoint (u' ∩ f n) v
Tactic: rcases hu'_eq with rfl | rfl
Cleared hypotheses: u, huv, hu'_eq
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
succ : ∀ (huv : u' ∩ f n ≠ v), Disjoint (u' ∩ f n) v
⊢ Disjoint u v
have succ₁ : ∀ (huv : u' \ f n ≠ v), Disjoint (u' \ f n) v
Tactic: rcases hu'_eq with rfl | rfl
Cleared hypotheses: u, huv, hu'_eq
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' ∩ f n ≠ v
⊢ Disjoint (u' ∩ f n) v
have succ : ∀ (huv : u' ∩ f n ≠ v' ∩ f n), Disjoint (u' ∩ f n) (v' ∩ f n)
Tactic: rcases hv'_eq with rfl | rfl
Cleared hypotheses: v, hv'_eq, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' ∩ f n ≠ v
succ : ∀ (huv : u' ∩ f n ≠ v' ∩ f n), Disjoint (u' ∩ f n) (v' ∩ f n)
⊢ Disjoint (u' ∩ f n) v
have succ₁ : ∀ (huv : u' ∩ f n ≠ v' \ f n), Disjoint (u' ∩ f n) (v' \ f n)
Tactic: rcases hv'_eq with rfl | rfl
Cleared hypotheses: v, hv'_eq, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' \ f n ≠ v
⊢ Disjoint (u' \ f n) v
have succ : ∀ (huv : u' \ f n ≠ v' ∩ f n), Disjoint (u' \ f n) (v' ∩ f n)
Tactic: rcases hv'_eq with rfl | rfl
Cleared hypotheses: v, hv'_eq, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' \ f n ≠ v
succ : ∀ (huv : u' \ f n ≠ v' ∩ f n), Disjoint (u' \ f n) (v' ∩ f n)
⊢ Disjoint (u' \ f n) v
have succ₁ : ∀ (huv : u' \ f n ≠ v' \ f n), Disjoint (u' \ f n) (v' \ f n)
Tactic: rcases hv'_eq with rfl | rfl
Cleared hypotheses: v, hv'_eq, huv
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ Disjoint (u' ∩ f n) (v' ∩ f n)
have succ : u' ≠ v'
Tactic: refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ Disjoint (u' \ f n) (v' \ f n)
have succ : u' ≠ v'
Tactic: refine Disjoint.mono diff_subset diff_subset (ih hu' hv' ?_)
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
have zero : ∀ {u v : Set α} (hu : u ∈ memPartition f 0) (hv : v ∈ memPartition f 0) (huv : u ≠ v), Disjoint u v
Tactic: induction n with
  | zero =>
    intro u v hu hv huv
    simp only [memPartition_zero, mem_singleton_iff] at hu hv
    rw [hu, hv] at huv
    exact absurd rfl huv
  | succ n ih =>
    intro u v hu hv huv
    rw [memPartition_succ] at hu hv
    obtain ⟨u', hu', hu'_eq⟩ := hu
    obtain ⟨v', hv', hv'_eq⟩ := hv
    rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl
    · refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)
    · exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right
    · exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left
    · refine Disjoint.mono diff_subset diff_subset (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
zero : ∀ {u v : Set α} (hu : u ∈ memPartition f 0) (hv : v ∈ memPartition f 0) (huv : u ≠ v), Disjoint u v
⊢ ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
have succ : ∀ (n : ℕ) (ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v)
  {u v : Set α} (hu : u ∈ memPartition f (n + 1)) (hv : v ∈ memPartition f (n + 1)) (huv : u ≠ v), Disjoint u v
Tactic: induction n with
  | zero =>
    intro u v hu hv huv
    simp only [memPartition_zero, mem_singleton_iff] at hu hv
    rw [hu, hv] at huv
    exact absurd rfl huv
  | succ n ih =>
    intro u v hu hv huv
    rw [memPartition_succ] at hu hv
    obtain ⟨u', hu', hu'_eq⟩ := hu
    obtain ⟨v', hv', hv'_eq⟩ := hv
    rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl
    · refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)
    · exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right
    · exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left
    · refine Disjoint.mono diff_subset diff_subset (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) univ
have succ : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) x ↔
    Membership.mem (γ := Set α) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
⊢ Membership.mem (γ := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) x ↔
    Membership.mem (γ := Set α) univ x
have this : x ∈ ⋃₀ memPartition f n
Tactic: have : x ∈ ⋃₀ memPartition f n := by simp [ih]
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : x ∈ ⋃₀ memPartition f n
⊢ Membership.mem (γ := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) x ↔
    Membership.mem (γ := Set α) univ x
have succ : ∀ (this : ∃ t ∈ memPartition f n, x ∈ t),
  ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
Tactic: simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : ∃ t ∈ memPartition f n, x ∈ t
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
have succ : ∀ (t : Set α) (ht : t ∈ memPartition f n) (hxt : x ∈ t),
  ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
Tactic: obtain ⟨t, ht, hxt⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
have pos : ∀ (hxf : x ∈ f n),
  ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
Tactic: by_cases hxf : x ∈ f n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
pos :
  ∀ (hxf : x ∈ f n),
    ∃ (t : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
have neg : ∀ (hxf : x ∉ f n),
  ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
Tactic: by_cases hxf : x ∈ f n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ ⋃₀ memPartition f n = univ
have zero : ⋃₀ memPartition f 0 = univ
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    ext x
    have : x ∈ ⋃₀ memPartition f n := by simp [ih]
    simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢
    obtain ⟨t, ht, hxt⟩ := this
    by_cases hxf : x ∈ f n
    · exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
    · exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
zero : ⋃₀ memPartition f 0 = univ
⊢ ⋃₀ memPartition f n = univ
have succ : ∀ (n : ℕ) (ih : ⋃₀ memPartition f n = univ), ⋃₀ memPartition f (n + 1) = univ
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    ext x
    have : x ∈ ⋃₀ memPartition f n := by simp [ih]
    simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢
    obtain ⟨t, ht, hxt⟩ := this
    by_cases hxf : x ∈ f n
    · exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
    · exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ Set.Finite.{u_1} (α := Set α) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
have this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
Tactic: have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
⊢ Finite.{u_1 + 1} (↑{s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} : Type u_1)
have succ : Finite.{u_1 + 1} (↑(⋃ i ∈ memPartition f n, {a : Set α | a = i ∩ f n} ∪ {a : Set α | a = i \ f n}) : Type u_1)
Tactic: simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
⊢ Finite.{u_1 + 1} (↑(⋃ i ∈ memPartition f n, {a : Set α | a = i ∩ f n} ∪ {a : Set α | a = i \ f n}) : Type u_1)
have succ : ∀ u ∈ memPartition f n, Finite.{u_1 + 1} (↑({a : Set α | a = u ∩ f n} ∪ {a : Set α | a = u \ f n}) : Type u_1)
Tactic: refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ (memPartition f n).Finite
have zero : (memPartition f 0).Finite
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
zero : (memPartition f 0).Finite
⊢ (memPartition f n).Finite
have succ : ∀ (n : ℕ) (ih : (memPartition f n).Finite), (memPartition f (n + 1)).Finite
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n)
have succ : memPartitionSet f n a ∈ memPartition f n ∧
  ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)
Tactic: refine ⟨memPartitionSet f n a, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)
have pos : a ∈ f n →
  memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
pos :
  a ∈ f n →
    memPartitionSet f n a ∈ memPartition f n ∧
      (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
        memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)
have neg : a ∉ f n →
  memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a \ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a \ f n = memPartitionSet f n a \ f n)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)
have succ : (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈ memPartition f (n + 1)
Tactic: classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
succ : (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈ memPartition f (n + 1)
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)
have succ₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
  (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n)
Tactic: classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
succ : (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈ memPartition f (n + 1)
succ₁ succ₂ succ₃ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n)
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)
have succ₄ : memPartitionSet f n a ∈ memPartition f n ∧
  ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)
Tactic: classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
⊢ memPartitionSet f n a ∈ memPartition f n
have zero : memPartitionSet f 0 a ∈ memPartition f 0
Tactic: induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
zero : memPartitionSet f 0 a ∈ memPartition f 0
⊢ memPartitionSet f n a ∈ memPartition f n
have succ : ∀ (n : ℕ) (ih : memPartitionSet f n a ∈ memPartition f n), memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)
Tactic: induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
have pos : ∀ (h : a ∈ f n), a ∈ memPartitionSet f n a ∩ f n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
pos : ∀ (h : a ∈ f n), a ∈ memPartitionSet f n a ∩ f n
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
have neg : ∀ (h : a ∉ f n), a ∈ memPartitionSet f n a \ f n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ memPartitionSet f (n + 1) a
have succ : a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
Tactic: classical
    rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
⊢ a ∈ memPartitionSet f n a
have zero : a ∈ memPartitionSet f 0 a
Tactic: induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
zero : a ∈ memPartitionSet f 0 a
⊢ a ∈ memPartitionSet f n a
have succ : ∀ (n : ℕ) (ih : a ∈ memPartitionSet f n a), a ∈ memPartitionSet f (n + 1) a
Tactic: induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
⊢ memPartitionSet f n a = s ↔ a ∈ s
have refine : ∀ (h : a ∈ s), memPartitionSet f n a = s
Tactic: refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
⊢ memPartitionSet f n a = s
have by_contra : ∀ (h_ne : ¬memPartitionSet f n a = s), False
Tactic: by_contra h_ne
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (hypothesis)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
⊢ False
have h_disj : Disjoint s (memPartitionSet f n a)
Tactic: have h_disj : Disjoint s (memPartitionSet f n a) :=
    disjoint_memPartition f n hs (memPartitionSet_mem f n a) (Ne.symm h_ne)
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ False
have refine : ¬Disjoint s (memPartitionSet f n a)
Tactic: refine absurd h_disj ?_