awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
a : (i : ι) → α i
⊢ Eq (α := (f : ((i : ι) → α i) → β) → (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) → β)
    (finLiftOn (α := α) fun (x : ι) ↦ ⟦a x⟧)
    fun (f : ((i : ι) → α i) → β) (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) ↦ f a
have h : ∀ (f : ((i : ι) → α i) → β) (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b),
  finLiftOn (α := α) (fun (x : ι) ↦ ⟦a x⟧) f h = f a
Tactic: ext f h
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ finLiftOn (α := α) (fun (x : ι) ↦ ⟦a x⟧) f h = f a
have h₁ : Quotient.liftOn (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) f h = f a
Tactic: dsimp [finLiftOn]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ Quotient.liftOn (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) f h = f a
have h₁ : Quotient.liftOn (s := piSetoid (α := α)) ⟦a⟧ f h = f a
Tactic: rw [finChoice_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
⊢ (finChoice (α := α) q).eval (α := α) = q
have refine : ∀ (a : (i : ι) → α i),
  Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)) fun (x : ι) ↦ ⟦a x⟧
Tactic: refine induction_on_fintype_pi q (fun a ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)) fun (x : ι) ↦ ⟦a x⟧
have rw : Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) ⟦a⟧) fun (x : ι) ↦ ⟦a x⟧
Tactic: rw [finChoice_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))
⊢ finChoice (α := α) (q.eval (α := α)) = q
have a : ∀ (a : (i : ι) → α i),
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α))) (finChoice (α := α) (eval (α := α) ⟦a⟧)) ⟦a⟧
Tactic: induction q using Quotient.ind
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ Eq (α :=
    (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧) →
      (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b) → C fun (x : ι) ↦ ⟦a x⟧)
    (finHRecOn (α := α) (C := C) fun (x : ι) ↦ ⟦a x⟧)
    fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧)
      (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b) ↦
    f a
have h : ∀ (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧) (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b),
  finHRecOn (α := α) (C := C) (fun (x : ι) ↦ ⟦a x⟧) f h = f a
Tactic: ext f h
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ finHRecOn (α := α) (C := C) (fun (x : ι) ↦ ⟦a x⟧) f h = f a
have h₁ : HEq (α := C (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)))
  (Quotient.hrecOn (motive := fun (x : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦ C (x.eval (α := α)))
      (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) f h :
    C (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)))
  (f a)
Tactic: refine eq_of_heq ((eqRec_heq _ _).trans ?_)
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ HEq (α := C (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)))
    (Quotient.hrecOn (motive := fun (x : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦ C (x.eval (α := α)))
        (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) f h :
      C (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)))
    (f a)
have h₁ : HEq (α := C (eval (α := α) ⟦a⟧))
  (Quotient.hrecOn (motive := fun (x : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦ C (x.eval (α := α))) ⟦a⟧ f
      h :
    C (eval (α := α) ⟦a⟧))
  (f a)
Tactic: rw [finChoice_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ Eq (α :=
    (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧) →
      (h : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), Eq.ndrec (motive := C) (f a) ⋯ = f b) →
        C fun (x : ι) ↦ ⟦a x⟧)
    (finRecOn (α := α) (C := C) fun (x : ι) ↦ ⟦a x⟧)
    fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧)
      (x : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), Eq.ndrec (motive := C) (f a) ⋯ = f b) ↦
    f a
have unfold : Eq (α :=
  (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧) →
    (h : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), Eq.ndrec (motive := C) (f a) sorry = f b) →
      C fun (x : ι) ↦ ⟦a x⟧)
  (fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧)
      (h : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), Eq.ndrec (motive := C) (f a) sorry = f b) ↦
    finHRecOn (α := α) (C := fun (x : (i : ι) → Quotient (S i)) ↦ C x) (fun (x : ι) ↦ ⟦a x⟧) f sorry)
  fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ ⟦a x⟧)
    (x : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), Eq.ndrec (motive := C) (f a) sorry = f b) ↦
  f a
Tactic: unfold finRecOn
-- Lean 4 proof step from Mathlib.Data.Fintype.Quotient (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
⊢ Eq (α :=
    (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x)) →
      (h : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) ⋯ = f b) → C fun (x : ι) ↦ ⟦a x⟧)
    (finRecOn (α := α) (C := C) fun (x : ι) ↦ ⟦a x⟧)
    fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x))
      (x : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) ⋯ = f b) ↦
    f a
have unfold : Eq (α :=
  (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x)) →
    (h : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) sorry = f b) → C fun (x : ι) ↦ ⟦a x⟧)
  (fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x))
      (h : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) sorry = f b) ↦
    Quotient.finRecOn (α := α) (C := fun (x : (i : ι) → Trunc (α i)) ↦ C x) (fun (x : ι) ↦ ⟦a x⟧)
      (fun (x : (i : ι) → α i) ↦ f x) sorry)
  fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x))
    (x : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) sorry = f b) ↦
  f a
Tactic: unfold finRecOn
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : s = t
⊢ s.toFinset = t.toFinset
have subst : ∀ [inst_2 : Fintype (↑s : Type u_1)], s.toFinset = s.toFinset
Tactic: subst h
Cleared hypotheses: t, inst_1, h
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p.toFinset ↔ x ∈ s
have rw : x ∈ p ↔ x ∈ s
Tactic: rw [@mem_toFinset _ _ (id _), H]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
rw : x ∈ p ↔ x ∈ s
⊢ x ∈ p.toFinset ↔ x ∈ s
have rw₁ : x ∈ p ↔ x ∈ p
Tactic: rw [@mem_toFinset _ _ (id _), H]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ s.toFinset.Nonempty ↔ s.Nonempty
have rw : (↑s.toFinset : Set α).Nonempty ↔ s.Nonempty
Tactic: rw [← Finset.coe_nonempty, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
rw : (↑s.toFinset : Set α).Nonempty ↔ s.Nonempty
⊢ s.toFinset.Nonempty ↔ s.Nonempty
have rw₁ : s.Nonempty ↔ s.Nonempty
Tactic: rw [← Finset.coe_nonempty, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : s.toFinset = t.toFinset
⊢ s = t
have rw : (↑s.toFinset : Set α) = t
Tactic: rw [← s.coe_toFinset, h, t.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : s.toFinset = t.toFinset
rw : (↑s.toFinset : Set α) = t
⊢ s = t
have rw₁ : (↑t.toFinset : Set α) = t
Tactic: rw [← s.coe_toFinset, h, t.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : s.toFinset = t.toFinset
rw : (↑s.toFinset : Set α) = t
rw₁ : (↑t.toFinset : Set α) = t
⊢ s = t
have rw₂ : t = t
Tactic: rw [← s.coe_toFinset, h, t.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
t : Finset α
⊢ s.toFinset ⊂ t ↔ s ⊂ (↑t : Set α)
have rw : (↑s.toFinset : Set α) ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
Tactic: rw [← Finset.coe_ssubset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
t : Finset α
rw : (↑s.toFinset : Set α) ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
⊢ s.toFinset ⊂ t ↔ s ⊂ (↑t : Set α)
have rw₁ : s ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
Tactic: rw [← Finset.coe_ssubset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
t : Set α
s : Finset α
inst : Fintype (↑t : Type u_1)
⊢ s ⊆ t.toFinset ↔ (↑s : Set α) ⊆ t
have rw : (↑s : Set α) ⊆ (↑t.toFinset : Set α) ↔ (↑s : Set α) ⊆ t
Tactic: rw [← Finset.coe_subset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
t : Set α
s : Finset α
inst : Fintype (↑t : Type u_1)
rw : (↑s : Set α) ⊆ (↑t.toFinset : Set α) ↔ (↑s : Set α) ⊆ t
⊢ s ⊆ t.toFinset ↔ (↑s : Set α) ⊆ t
have rw₁ : (↑s : Set α) ⊆ t ↔ (↑s : Set α) ⊆ t
Tactic: rw [← Finset.coe_subset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
t : Set α
s : Finset α
inst : Fintype (↑t : Type u_1)
⊢ s ⊂ t.toFinset ↔ (↑s : Set α) ⊂ t
have rw : (↑s : Set α) ⊂ (↑t.toFinset : Set α) ↔ (↑s : Set α) ⊂ t
Tactic: rw [← Finset.coe_ssubset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
t : Set α
s : Finset α
inst : Fintype (↑t : Type u_1)
rw : (↑s : Set α) ⊂ (↑t.toFinset : Set α) ↔ (↑s : Set α) ⊂ t
⊢ s ⊂ t.toFinset ↔ (↑s : Set α) ⊂ t
have rw₁ : (↑s : Set α) ⊂ t ↔ (↑s : Set α) ⊂ t
Tactic: rw [← Finset.coe_ssubset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
t : Finset α
⊢ s.toFinset ⊆ t ↔ s ⊆ (↑t : Set α)
have rw : (↑s.toFinset : Set α) ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
Tactic: rw [← Finset.coe_subset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
t : Finset α
rw : (↑s.toFinset : Set α) ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
⊢ s.toFinset ⊆ t ↔ s ⊆ (↑t : Set α)
have rw₁ : s ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
Tactic: rw [← Finset.coe_subset, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial
have rw : (↑s.toFinset : Set α).Nontrivial ↔ s.Nontrivial
Tactic: rw [Finset.Nontrivial, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
rw : (↑s.toFinset : Set α).Nontrivial ↔ s.Nontrivial
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial
have rw₁ : s.Nontrivial ↔ s.Nontrivial
Tactic: rw [Finset.Nontrivial, coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑t : Type u_1)
inst_3 : Fintype (↑(s ∩ t) : Type u_1)
⊢ (s ∩ t).toFinset = s.toFinset ∩ t.toFinset
have h : ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑t : Type u_1)
inst_3 : Fintype (↑(s ∪ t) : Type u_1)
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
have h : ∀ (a : α), a ∈ (s ∪ t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑t : Type u_1)
inst_3 : Fintype (↑(s \ t) : Type u_1)
⊢ (s \ t).toFinset = s.toFinset \ t.toFinset
have h : ∀ (a : α), a ∈ (s \ t).toFinset ↔ a ∈ s.toFinset \ t.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s t : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑t : Type u_1)
inst_3 : Fintype (↑(s ∆ t) : Type u_1)
⊢ (s ∆ t).toFinset = s.toFinset ∆ t.toFinset
have h : ∀ (a : α), a ∈ (s ∆ t).toFinset ↔ a ∈ s.toFinset ∆ t.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype α
inst_3 : Fintype (↑sᶜ : Type u_1)
⊢ sᶜ.toFinset = s.toFinsetᶜ
have h : ∀ (a : α), a ∈ sᶜ.toFinset ↔ a ∈ s.toFinsetᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : Fintype (↑∅ : Type u_1)
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset ∅) ∅
have h : ∀ (a : α), Membership.mem (γ := Finset α) (toFinset ∅) a ↔ Membership.mem (γ := Finset α) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Fintype (↑univ : Type u_1)
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset univ) Finset.univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) (toFinset univ) a ↔ Membership.mem (γ := Finset α) Finset.univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
A : Fintype (↑∅ : Type u_1) := Fintype.ofIsEmpty
⊢ s.toFinset = ∅ ↔ s = ∅
have rw : s.toFinset = toFinset ∅ ↔ s = ∅
Tactic: rw [← toFinset_empty, toFinset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
A : Fintype (↑∅ : Type u_1) := Fintype.ofIsEmpty
rw : s.toFinset = toFinset ∅ ↔ s = ∅
⊢ s.toFinset = ∅ ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [← toFinset_empty, toFinset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype α
inst_1 : Fintype (↑s : Type u_1)
⊢ s.toFinset = Finset.univ ↔ s = univ
have rw : (↑s.toFinset : Set α) = (↑Finset.univ : Set α) ↔ s = univ
Tactic: rw [← coe_inj, coe_toFinset, coe_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype α
inst_1 : Fintype (↑s : Type u_1)
rw : (↑s.toFinset : Set α) = (↑Finset.univ : Set α) ↔ s = univ
⊢ s.toFinset = Finset.univ ↔ s = univ
have rw₁ : s = (↑Finset.univ : Set α) ↔ s = univ
Tactic: rw [← coe_inj, coe_toFinset, coe_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype α
inst_1 : Fintype (↑s : Type u_1)
rw : (↑s.toFinset : Set α) = (↑Finset.univ : Set α) ↔ s = univ
rw₁ : s = (↑Finset.univ : Set α) ↔ s = univ
⊢ s.toFinset = Finset.univ ↔ s = univ
have rw₂ : s = univ ↔ s = univ
Tactic: rw [← coe_inj, coe_toFinset, coe_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype (↑{x : α | p x} : Type u_1)
⊢ toFinset {x : α | p x} = filter p Finset.univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) (toFinset {x : α | p x}) a ↔ a ∈ filter p Finset.univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : Fintype β
f : β → α
inst_2 : Fintype (↑(range f) : Type u_1)
⊢ (range f).toFinset = Finset.image f Finset.univ
have h : ∀ (a : α), a ∈ (range f).toFinset ↔ a ∈ Finset.image f Finset.univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
a : α
inst : Fintype (↑{a} : Type u_1)
⊢ Eq (α := Finset α) (toFinset {a}) {a}
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) (toFinset {a}) a_1 ↔ Membership.mem (γ := Finset α) {a} a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Set α
inst_1 : Fintype (↑(insert a s) : Type u_1)
inst_2 : Fintype (↑s : Type u_1)
⊢ (insert a s).toFinset = insert a s.toFinset
have h : ∀ (a_1 : α), a_1 ∈ (insert a s).toFinset ↔ a_1 ∈ insert a s.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ {x : α | x ∈ s} = s.toFinset
have h : ∀ (a : α), Membership.mem (γ := Finset α) {x : α | x ∈ s} a ↔ a ∈ s.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
⊢ Membership.mem (γ := Finset α) {x : α | x ∈ s} a ↔ a ∈ s.toFinset
have h : a ∈ s ↔ a ∈ s.toFinset
Tactic: rw [mem_filter_univ, mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
h : a ∈ s ↔ a ∈ s.toFinset
⊢ Membership.mem (γ := Finset α) {x : α | x ∈ s} a ↔ a ∈ s.toFinset
have h₁ : a ∈ s ↔ a ∈ s
Tactic: rw [mem_filter_univ, mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sets (goal)
Goal:
⊢ Eq (α := Multiset Prop) (val univ) (val {True, False})
have simp : val univ = True ::ₘ {False}
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
⊢ Eq.{u_3 + 1} (α := Finset α) (toLeft.{u_3, u_4} (β := β) univ) univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) (toLeft.{u_3, u_4} (β := β) univ) a ↔ Membership.mem (γ := Finset α) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
⊢ Eq.{u_4 + 1} (α := Finset β) (toRight.{u_3, u_4} (α := α) univ) univ
have h : ∀ (a : β), Membership.mem (γ := Finset β) (toRight.{u_3, u_4} (α := α) univ) a ↔ Membership.mem (γ := Finset β) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
⊢ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ = (image b univ).erase k
have a : image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ ⊆ (image b univ).erase k
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
a : image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ ⊆ (image b univ).erase k
⊢ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ = (image b univ).erase k
have a₁ : (image b univ).erase k ⊆ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
⊢ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ ⊆ (image b univ).erase k
have a : ∀ (x : { a : α // b a ≠ k }),
  Membership.mem (γ := Finset { a : α // b a ≠ k }) univ x → b (↑x : α) ∈ (image b univ).erase k
Tactic: rw [image_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ Membership.mem (γ := Finset β) (image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ) i
have a : ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i
Tactic: rw [mem_image]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i
have a : ∀ (a : α),
  Membership.mem (γ := Finset α) univ a →
    ∀ (ha : b a = i),
      ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i
Tactic: rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a : α
left : Membership.mem (γ := Finset α) univ a
ha : b a = i
⊢ ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i
have a₁ : ∀ (hi : b a ∈ (image b univ).erase k),
  ∃ (a_1 : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a_1 ∧ b (↑a_1 : α) = b a
Tactic: subst ha
Cleared hypotheses: i, hi, ha
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
⊢ Nonempty (Equiv.{u_1 + 1, u_2 + 1} α ↥t)
have rwa : Fintype.card α = Fintype.card.{u_2} ↥t
Tactic: rwa [← Fintype.card_eq, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
have empty : ∀ (e : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
  ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
e : Equiv.{u_1 + 1, u_2 + 1} α ↥t
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
have h : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((e : (a : α) → ↥t) i) : β) = f i
Tactic: use e