awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.PiInduction (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
hne : (Finset.sigma (α := α) univ f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs :
  ∀ t ⊂ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
hr : r i x (g i)
hx' : x ∉ g i
intro :
  ∃ x_1 ∈ Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i))),
    x_1 ∉ Finset.sigma (α := α) univ g
⊢ Finset.sigma (α := α) univ g ⊂
    Finset.sigma (α := α) univ (update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)))
have rw : ∀ (i_1 : ι), g i_1 ⊆ update (β := fun (a : ι) ↦ Finset (α a)) g i (insert x (g i)) i_1
Tactic: rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : (i : ι) → Decidable (Membership.mem (γ := Finset ι) ∅ i)
⊢ piecewise (π := π) ∅ f g = g
have h : ∀ (i : ι), piecewise (π := π) ∅ f g i = g i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
⊢ (↑s : Set ι).piecewise (β := π) f g = s.piecewise (π := π) f g
have h : ∀ (x : ι), (↑s : Set ι).piecewise (β := π) f g x = s.piecewise (π := π) f g x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise (π := π) f g = update (β := π) (s.piecewise (π := π) f g) j (f j)
have simp : (↑(insert j s) : Set ι).piecewise (β := π) f g = (insert j (↑s : Set ι)).piecewise (β := π) f g
Tactic: simp only [← piecewise_coe, ← Set.piecewise_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise (π := π) f g = update (β := π) (s.piecewise (π := π) f g) j (f j)
have classical : (↑(insert j s) : Set ι).piecewise (β := π) f g = (insert j (↑s : Set ι)).piecewise (β := π) f g
Tactic: classical simp only [← piecewise_coe, ← Set.piecewise_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
⊢ (↑(insert j s) : Set ι).piecewise (β := π) f g = (insert j (↑s : Set ι)).piecewise (β := π) f g
have h : ∀ (x : ι), (↑(insert j s) : Set ι).piecewise (β := π) f g x = (insert j (↑s : Set ι)).piecewise (β := π) f g x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
x : ι
⊢ (↑(insert j s) : Set ι).piecewise (β := π) f g x = (insert j (↑s : Set ι)).piecewise (β := π) f g x
have h : (↑(insert j s) : Set ι) = insert j (↑s : Set ι)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
⊢ p (s.piecewise (π := π) f g i)
have pos : ∀ (hi : i ∈ s), p (s.piecewise (π := π) f g i)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
pos : ∀ (hi : i ∈ s), p (s.piecewise (π := π) f g i)
⊢ p (s.piecewise (π := π) f g i)
have neg : ∀ (hi : i ∉ s), p (s.piecewise (π := π) f g i)
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : DecidableEq ι
i : ι
⊢ piecewise (π := π) {i} f g = update (β := π) g i (f i)
have rw : piecewise (π := π) (insert i ∅) f g = update (β := π) g i (f i)
Tactic: rw [← insert_empty_eq, piecewise_insert, piecewise_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : DecidableEq ι
i : ι
rw : piecewise (π := π) (insert i ∅) f g = update (β := π) g i (f i)
⊢ piecewise (π := π) {i} f g = update (β := π) g i (f i)
have rw₁ : update (β := π) (piecewise (π := π) ∅ f g) i (f i) = update (β := π) g i (f i)
Tactic: rw [← insert_empty_eq, piecewise_insert, piecewise_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : DecidableEq ι
i : ι
rw : piecewise (π := π) (insert i ∅) f g = update (β := π) g i (f i)
rw₁ : update (β := π) (piecewise (π := π) ∅ f g) i (f i) = update (β := π) g i (f i)
⊢ piecewise (π := π) {i} f g = update (β := π) g i (f i)
have rw₂ : update (β := π) g i (f i) = update (β := π) g i (f i)
Tactic: rw [← insert_empty_eq, piecewise_insert, piecewise_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
⊢ update (β := π) (s.piecewise (π := π) f g) i v = s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v)
have h : ∀ (j : ι),
  update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
have h : ∀ (v : π j),
  update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
Tactic: rcases em (j = i) with (rfl | hj)
Cleared hypotheses: i, v
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
h :
  ∀ (v : π j),
    update (β := π) (s.piecewise (π := π) f g) j v j =
      s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
have h₁ : ∀ (hj : ¬j = i),
  update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
Tactic: rcases em (j = i) with (rfl | hj)
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
v : π j
⊢ update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
have pos : ∀ (hs : j ∈ s),
  update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
Tactic: by_cases hs : j ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
v : π j
pos :
  ∀ (hs : j ∈ s),
    update (β := π) (s.piecewise (π := π) f g) j v j =
      s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
⊢ update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
have neg : ∀ (hs : j ∉ s),
  update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
Tactic: by_cases hs : j ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
have pos : ∀ (hs : j ∈ s),
  update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
Tactic: by_cases hs : j ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
pos :
  ∀ (hs : j ∈ s),
    update (β := π) (s.piecewise (π := π) f g) i v j =
      s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
have neg : ∀ (hs : j ∉ s),
  update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
Tactic: by_cases hs : j ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ update (β := π) (s.piecewise (π := π) f g) i v = s.piecewise (π := π) (update (β := π) f i v) g
have rw : s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) (update (β := π) f i v) g
Tactic: rw [update_piecewise]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) (update (β := π) f i v) g
have refine : ∀ (j : ι) (hj : j ∉ s), j ≠ i
Tactic: refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ update (β := π) (s.piecewise (π := π) f g) i v = s.piecewise (π := π) f (update (β := π) g i v)
have rw : s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) f (update (β := π) g i v)
Tactic: rw [update_piecewise]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) f (update (β := π) g i v)
have refine : ∀ (j : ι) (hj : j ∈ s), j ≠ i
Tactic: refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
⊢ s.piecewise (π := π) f f = f
have h : ∀ (i : ι), s.piecewise (π := π) f f i = f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
⊢ s.piecewise (π := π) f f i = f i
have pos : ∀ (h : i ∈ s), s.piecewise (π := π) f f i = f i
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
pos : ∀ (h : i ∈ s), s.piecewise (π := π) f f i = f i
⊢ s.piecewise (π := π) f f i = f i
have neg : ∀ (h : i ∉ s), s.piecewise (π := π) f f i = f i
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : (i : ι) → Decidable (Membership.mem (γ := Finset ι) univ i)
f g : (i : ι) → π i
⊢ piecewise (π := π) univ f g = f
have h : ∀ (i : ι), piecewise (π := π) univ f g i = f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
s : Finset ι
inst_2 : (i : ι) → Decidable (i ∈ s)
inst_3 : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
⊢ sᶜ.piecewise (π := π) f g = s.piecewise (π := π) g f
have h : ∀ (i : ι), sᶜ.piecewise (π := π) f g i = s.piecewise (π := π) g f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ (erase univ i).piecewise (π := π) f g = update (β := π) f i (g i)
have rw : piecewise (π := π) {i}ᶜ f g = update (β := π) f i (g i)
Tactic: rw [← compl_singleton, piecewise_compl, piecewise_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
i : ι
f g : (i : ι) → π i
rw : piecewise (π := π) {i}ᶜ f g = update (β := π) f i (g i)
⊢ (erase univ i).piecewise (π := π) f g = update (β := π) f i (g i)
have rw₁ : piecewise (π := π) {i} g f = update (β := π) f i (g i)
Tactic: rw [← compl_singleton, piecewise_compl, piecewise_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
i : ι
f g : (i : ι) → π i
rw : piecewise (π := π) {i}ᶜ f g = update (β := π) f i (g i)
rw₁ : piecewise (π := π) {i} g f = update (β := π) f i (g i)
⊢ (erase univ i).piecewise (π := π) f g = update (β := π) f i (g i)
have rw₂ : update (β := π) f i (g i) = update (β := π) f i (g i)
Tactic: rw [← compl_singleton, piecewise_compl, piecewise_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi (α := π) t'
hg : g ∈ t.pi (α := π) t'
⊢ s.piecewise (π := π) f g ∈ t.pi (α := π) t'
have rw : (↑s : Set ι).piecewise (β := π) f g ∈ t.pi (α := π) t'
Tactic: rw [← piecewise_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi (α := π) t'
hg : g ∈ t.pi (α := π) t'
⊢ s.piecewise (π := π) f g ∈ t.pi (α := π) t'
have classical : (↑s : Set ι).piecewise (β := π) f g ∈ t.pi (α := π) t'
Tactic: classical rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
⊢ s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
have pos : ∀ (hx : x ∈ s), s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Piecewise (goal)
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
pos : ∀ (hx : x ∈ s), s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
⊢ s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
have neg : ∀ (hx : x ∉ s), s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s t : Finset α
⊢ s ∈ t.powerset ↔ s ⊆ t
have mk : ∀ (val : Multiset α) (nodup : val.Nodup),
  { val := val, nodup := nodup : Finset α } ∈ t.powerset ↔ { val := val, nodup := nodup : Finset α } ⊆ t
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (↑s.powerset : Set (Finset α)) = SetLike.coe ⁻¹' 𝒫 (↑s : Set α)
have h : ∀ (x : Finset α),
  x ∈ (↑s.powerset : Set (Finset α)) ↔ Membership.mem (γ := Set (Finset α)) (SetLike.coe ⁻¹' 𝒫 (↑s : Set α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
⊢ s.powerset = {∅} ↔ s = ∅
have rw : s.powerset = powerset ∅ ↔ s = ∅
Tactic: rw [← powerset_empty, powerset_inj]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
rw : s.powerset = powerset ∅ ↔ s = ∅
⊢ s.powerset = {∅} ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [← powerset_empty, powerset_inj]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (hypothesis)
Goal:
α : Type u_1
s : Finset α
β : Type u_2
inst : DecidableEq β
f : α → β
H : Set.InjOn f (↑s : Set α)
⊢ Set.InjOn.{u_1, u_2} (β := Finset β) (fun (x : Finset α) ↦ image f x) (↑s.powerset : Set (Finset α))
have this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
Tactic: have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∉ t
have apply : a ∈ t → a ∈ s
Tactic: apply mt _ h
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).powerset = s.powerset ∪ image (insert a) s.powerset
have h : ∀ (t : Finset α), t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset
Tactic: ext t
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset
have h : t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t
Tactic: simp only [mem_powerset, mem_image, mem_union, subset_insert_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
⊢ (↑s.powerset : Set (Finset α)).PairwiseDisjoint (α := Set (Finset α)) fun (t : Finset α) ↦ {t, insert a t}
have simp_rw : ∀ ⦃i : Finset α⦄,
  i ⊆ s → ∀ ⦃j : Finset α⦄, j ⊆ s → Set.Nonempty (α := Finset α) ({i, insert a i} ∩ {j, insert a j}) → i = j
Tactic: simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ Set.Nonempty (α := Finset α) ({i, insert a i} ∩ {j, insert a j}) → i = j
have simp : (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)
Tactic: simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)
have refine_1 : i = insert a j → i = j
Tactic: refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
refine_1 : i = insert a j → i = j
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)
have refine_2 : insert a i = j → i = j
Tactic: refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ t ∈ s.ssubsets ↔ t ⊂ s
have rw : t ∈ s.powerset.erase s ↔ t ⊂ s
Tactic: rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∈ s.powerset.erase s ↔ t ⊂ s
⊢ t ∈ s.ssubsets ↔ t ⊂ s
have rw₁ : t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s
Tactic: rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∈ s.powerset.erase s ↔ t ⊂ s
rw₁ : t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s
⊢ t ∈ s.ssubsets ↔ t ⊂ s
have rw₂ : t ≠ s ∧ t ⊆ s ↔ t ⊂ s
Tactic: rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∈ s.powerset.erase s ↔ t ⊂ s
rw₁ : t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s
rw₂ : t ≠ s ∧ t ⊆ s ↔ t ⊂ s
⊢ t ∈ s.ssubsets ↔ t ⊂ s
have rw₃ : t ≠ s ∧ t ⊆ s ↔ t ⊆ s ∧ t ≠ s
Tactic: rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : t ∈ s.powerset.erase s ↔ t ⊂ s
rw₁ : t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s
rw₂ : t ≠ s ∧ t ⊆ s ↔ t ⊂ s
rw₃ : t ≠ s ∧ t ⊆ s ↔ t ⊆ s ∧ t ≠ s
⊢ t ∈ s.ssubsets ↔ t ⊂ s
have rw₄ : t ⊆ s ∧ t ≠ s ↔ t ⊆ s ∧ t ≠ s
Tactic: rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ∈ s.ssubsets
have rw : ∅ ⊆ s ∧ ∅ ≠ s
Tactic: rw [mem_ssubsets, ssubset_iff_subset_ne]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s t : Finset α
⊢ s ∈ powersetCard n t ↔ s ⊆ t ∧ #s = n
have mk : ∀ (val : Multiset α) (nodup : val.Nodup),
  { val := val, nodup := nodup : Finset α } ∈ powersetCard n t ↔
    { val := val, nodup := nodup : Finset α } ⊆ t ∧ #{ val := val, nodup := nodup : Finset α } = n
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
⊢ #({x ∈ powersetCard n t | s ⊆ x}) = (#t - #s).choose (n - #s)
have hinj : Set.InjOn (β := Finset α) (fun (x : Finset α) ↦ x ∪ s) (↑(powersetCard (n - #s) (t \ s)) : Set (Finset α))
Tactic: have hinj : Set.InjOn (· ∪ s) ↑((t \ s).powersetCard (n - #s)) := fun a ha b hb hab =>
    (union_sdiff_cancel_right
      (disjoint_of_subset_left (mem_powersetCard.mp ha).1 disjoint_sdiff_self_left)).symm.trans
    ((congrArg (· \ s) hab).trans
      (union_sdiff_cancel_right
        (disjoint_of_subset_left (mem_powersetCard.mp hb).1 disjoint_sdiff_self_left)))
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ #(powersetCard n s) = 0
have rw : (#s).choose n = 0
Tactic: rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
h : #s < n
rw : (#s).choose n = 0
⊢ #(powersetCard n s) = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Finset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ ↔ #s < n
have refine : powersetCard n s = ∅ → #s < n
Tactic: refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩