awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
a : (i : ι) → α i
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
⊢ 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

Tactic:
ext f h
-- Module: Mathlib.Data.Fintype.Quotient
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
h₁ : Quotient.liftOn (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) f h = f a
⊢ finLiftOn (α := α) (fun (x : ι) ↦ ⟦a x⟧) f h = f a

Tactic:
dsimp [finLiftOn]

Premises used: Quotient.finLiftOn
-- Module: Mathlib.Data.Fintype.Quotient
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
h₁ : Quotient.liftOn (s := piSetoid (α := α)) ⟦a⟧ f h = f a
⊢ Quotient.liftOn (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) f h = f a

Tactic:
rw [finChoice_eq]

Premises used: Quotient.finChoice_eq
-- Module: Mathlib.Data.Fintype.Quotient
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 (s := piSetoid (α := α)) ⟦a⟧ f h = f a

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Quotient
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

Tactic:
induction_on_fintype_pi q (fun a ↦ ?_)

Premises used: Quotient.induction_on_fintype_pi
-- Module: Mathlib.Data.Fintype.Quotient
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)
refine :
  ∀ (a : (i : ι) → α i),
    Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)) fun (x : ι) ↦ ⟦a x⟧
⊢ (finChoice (α := α) q).eval (α := α) = q

Tactic:
refine induction_on_fintype_pi q (fun a ↦ ?_)
-- Module: Mathlib.Data.Fintype.Quotient
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
rw : Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) ⟦a⟧) fun (x : ι) ↦ ⟦a x⟧
⊢ Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)) fun (x : ι) ↦ ⟦a x⟧

Tactic:
rw [finChoice_eq]

Premises used: Quotient.finChoice_eq
-- Module: Mathlib.Data.Fintype.Quotient
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 (α := α) ⟦a⟧) fun (x : ι) ↦ ⟦a x⟧

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Quotient
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 (α := α))
a :
  ∀ (a : (i : ι) → α i),
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α))) (finChoice (α := α) (eval (α := α) ⟦a⟧)) ⟦a⟧
⊢ finChoice (α := α) (q.eval (α := α)) = q

Tactic:
induction q using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Data.Fintype.Quotient
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 (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α))) (finChoice (α := α) (eval (α := α) ⟦a⟧)) ⟦a⟧

Tactic:
finChoice_eq _

Premises used: Quotient.map, Quotient.eval, Quotient.finChoice_eq
-- Module: Mathlib.Data.Fintype.Quotient
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 (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α))) (finChoice (α := α) (eval (α := α) ⟦a⟧)) ⟦a⟧

Tactic:
exact finChoice_eq _

Premises used: Quotient.finChoice_eq
-- Module: Mathlib.Data.Fintype.Quotient
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
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
⊢ 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

Tactic:
ext f h
-- Module: Mathlib.Data.Fintype.Quotient
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

Tactic:
eq_of_heq ((eqRec_heq _ _).trans ?_)

Premises used: eqRec_heq, HEq.trans, eq_of_heq
-- Module: Mathlib.Data.Fintype.Quotient
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
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)
⊢ finHRecOn (α := α) (C := C) (fun (x : ι) ↦ ⟦a x⟧) f h = f a

Tactic:
refine eq_of_heq ((eqRec_heq _ _).trans ?_)

Premises used: eqRec_heq, HEq.trans, eq_of_heq
-- Module: Mathlib.Data.Fintype.Quotient
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
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)
⊢ 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:
rw [finChoice_eq]

Premises used: Quotient.finChoice_eq
-- Module: Mathlib.Data.Fintype.Quotient
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 (α := α) ⟦a⟧))
    (Quotient.hrecOn (motive := fun (x : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦ C (x.eval (α := α))) ⟦a⟧ f
        h :
      C (eval (α := α) ⟦a⟧))
    (f a)

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Quotient
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
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) ⋯ = 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) ⋯ = f b) ↦
      finHRecOn (α := α) (C := fun (x : (i : ι) → Quotient (S i)) ↦ C x) (fun (x : ι) ↦ ⟦a x⟧) f ⋯)
    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
⊢ 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

Tactic:
unfold finRecOn
-- Module: Mathlib.Data.Fintype.Quotient
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⟧)
    (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) ⋯ = f b) ↦
      finHRecOn (α := α) (C := fun (x : (i : ι) → Quotient (S i)) ↦ C x) (fun (x : ι) ↦ ⟦a x⟧) f ⋯)
    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

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
α : ι → Sort u_2
f : (i : ι) → α i
⊢ (finChoice (α := α) fun (i : ι) ↦ mk (f i)) = mk f

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
α : ι → Sort u_2
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Trunc (α i)
⊢ Eq (α := (f : ((i : ι) → α i) → β) → (h : ∀ (a b : (i : ι) → α i), f a = f b) → β) (finLiftOn (α := α) q)
    fun (f : ((i : ι) → α i) → β) (x : ∀ (a b : (i : ι) → α i), f a = f b) ↦
    f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a

Tactic:
funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_empty q) _ _

Premises used: Quotient.finLiftOn_empty, congrFun₂, funext₂
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
α : ι → Sort u_2
β : Sort u_3
a : (i : ι) → α i
⊢ Eq (α := (f : ((i : ι) → α i) → β) → (h : ∀ (a b : (i : ι) → α i), f a = f b) → β)
    (finLiftOn (α := α) fun (x : ι) ↦ ⟦a x⟧) fun (f : ((i : ι) → α i) → β) (x : ∀ (a b : (i : ι) → α i), f a = f b) ↦
    f a

Tactic:
funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_mk a) _ _

Premises used: congrFun₂, funext₂, Quotient.finLiftOn_mk
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
unfold :
  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⟧)
    (fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x))
        (h : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) ⋯ = f b) ↦
      Quotient.finRecOn (α := α) (C := fun (x : (i : ι) → Trunc (α i)) ↦ C x) (fun (x : ι) ↦ ⟦a x⟧)
        (fun (x : (i : ι) → α i) ↦ f 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
⊢ 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

Tactic:
unfold finRecOn
-- Module: Mathlib.Data.Fintype.Quotient
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⟧)
    (fun (f : (a : (i : ι) → α i) → C fun (x : ι) ↦ mk (a x))
        (h : ∀ (a b : (i : ι) → α i), Eq.ndrec (motive := C) (f a) ⋯ = f b) ↦
      Quotient.finRecOn (α := α) (C := fun (x : (i : ι) → Trunc (α i)) ↦ C x) (fun (x : ι) ↦ ⟦a x⟧)
        (fun (x : (i : ι) → α i) ↦ f 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

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : s = t
subst : ∀ [inst_2 : Fintype (↑s : Type u_1)], s.toFinset = s.toFinset
⊢ s.toFinset = t.toFinset

Tactic:
subst h
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst inst_1 : Fintype (↑s : Type u_1)
⊢ s.toFinset = s.toFinset

Tactic:
congr!
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
a : α
⊢ a ∈ s.toFinset ↔ a ∈ s

Tactic:
simp [toFinset]

Premises used: Set.toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
rw : x ∈ p ↔ x ∈ s
rw₁ rw₂ : x ∈ p ↔ x ∈ p
⊢ x ∈ p.toFinset ↔ x ∈ s

Tactic:
rw [@mem_toFinset _ _ (id _), H]

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ (↑s.toFinset : Set α) = s

Tactic:
Set.ext fun _ => mem_toFinset

Premises used: Set.ext, Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
rw : (↑s.toFinset : Set α).Nonempty ↔ s.Nonempty
rw₁ rw₂ : s.Nonempty ↔ s.Nonempty
⊢ s.toFinset.Nonempty ↔ s.Nonempty

Tactic:
rw [← Finset.coe_nonempty, coe_toFinset]

Premises used: Finset.coe_nonempty, Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
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
rw₂ rw₃ : t = t
⊢ s = t

Tactic:
rw [← s.coe_toFinset, h, t.coe_toFinset]

Premises used: Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
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

Tactic:
simp [h]
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
simp [Finset.subset_iff, Set.subset_def]

Premises used: Set.subset_def, Finset.subset_iff
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
t : Finset α
rw : (↑s.toFinset : Set α) ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
rw₁ rw₂ : s ⊂ (↑t : Set α) ↔ s ⊂ (↑t : Set α)
⊢ s.toFinset ⊂ t ↔ s ⊂ (↑t : Set α)

Tactic:
rw [← Finset.coe_ssubset, coe_toFinset]

Premises used: Finset.coe_ssubset, Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
t : Set α
s : Finset α
inst : Fintype (↑t : Type u_1)
rw : (↑s : Set α) ⊆ (↑t.toFinset : Set α) ↔ (↑s : Set α) ⊆ t
rw₁ rw₂ : (↑s : Set α) ⊆ t ↔ (↑s : Set α) ⊆ t
⊢ s ⊆ t.toFinset ↔ (↑s : Set α) ⊆ t

Tactic:
rw [← Finset.coe_subset, coe_toFinset]

Premises used: Set.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
t : Set α
s : Finset α
inst : Fintype (↑t : Type u_1)
rw : (↑s : Set α) ⊂ (↑t.toFinset : Set α) ↔ (↑s : Set α) ⊂ t
rw₁ rw₂ : (↑s : Set α) ⊂ t ↔ (↑s : Set α) ⊂ t
⊢ s ⊂ t.toFinset ↔ (↑s : Set α) ⊂ t

Tactic:
rw [← Finset.coe_ssubset, coe_toFinset]

Premises used: Finset.coe_ssubset, Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]

Premises used: Set.ssubset_def, Finset.ssubset_def, Set.toFinset_subset_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
t : Finset α
rw : (↑s.toFinset : Set α) ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
rw₁ rw₂ : s ⊆ (↑t : Set α) ↔ s ⊆ (↑t : Set α)
⊢ s.toFinset ⊆ t ↔ s ⊆ (↑t : Set α)

Tactic:
rw [← Finset.coe_subset, coe_toFinset]

Premises used: Set.coe_toFinset, Finset.coe_subset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
⊢ Disjoint s.toFinset t.toFinset ↔ Disjoint s t

Tactic:
simp only [← disjoint_coe, coe_toFinset]

Premises used: Finset.disjoint_coe, Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
rw : (↑s.toFinset : Set α).Nontrivial ↔ s.Nontrivial
rw₁ rw₂ : s.Nontrivial ↔ s.Nontrivial
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
rw [Finset.Nontrivial, coe_toFinset]

Premises used: Finset.Nontrivial, Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ Subsingleton.{u_1 + 1} ↥s.toFinset ↔ s.Subsingleton

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
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)
h : ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset
⊢ (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
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)
a : α
⊢ a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
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)
h : ∀ (a : α), a ∈ (s ∪ t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
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)
a : α
⊢ a ∈ (s ∪ t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
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)
h : ∀ (a : α), a ∈ (s \ t).toFinset ↔ a ∈ s.toFinset \ t.toFinset
⊢ (s \ t).toFinset = s.toFinset \ t.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
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)
a : α
⊢ a ∈ (s \ t).toFinset ↔ a ∈ s.toFinset \ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
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)
h : ∀ (a : α), a ∈ (s ∆ t).toFinset ↔ a ∈ s.toFinset ∆ t.toFinset
⊢ (s ∆ t).toFinset = s.toFinset ∆ t.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
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)
a : α
⊢ a ∈ (s ∆ t).toFinset ↔ a ∈ s.toFinset ∆ t.toFinset

Tactic:
simp [mem_symmDiff, Finset.mem_symmDiff]

Premises used: Set.mem_symmDiff, Finset.mem_symmDiff
-- Module: Mathlib.Data.Fintype.Sets
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)
h : ∀ (a : α), a ∈ sᶜ.toFinset ↔ a ∈ s.toFinsetᶜ
⊢ sᶜ.toFinset = s.toFinsetᶜ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
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)
a : α
⊢ a ∈ sᶜ.toFinset ↔ a ∈ s.toFinsetᶜ

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype (↑∅ : Type u_1)
h : ∀ (a : α), Membership.mem (γ := Finset α) (toFinset ∅) a ↔ Membership.mem (γ := Finset α) ∅ a
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset ∅) ∅

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype (↑∅ : Type u_1)
a : α
⊢ Membership.mem (γ := Finset α) (toFinset ∅) a ↔ Membership.mem (γ := Finset α) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Fintype (↑univ : Type u_1)
h : ∀ (a : α), Membership.mem (γ := Finset α) (toFinset univ) a ↔ Membership.mem (γ := Finset α) Finset.univ a
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset univ) Finset.univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Fintype (↑univ : Type u_1)
a : α
⊢ Membership.mem (γ := Finset α) (toFinset univ) a ↔ Membership.mem (γ := Finset α) Finset.univ a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
A : Fintype (↑∅ : Type u_1) := Fintype.ofIsEmpty
rw : s.toFinset = toFinset ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ s.toFinset = ∅ ↔ s = ∅

Tactic:
rw [← toFinset_empty, toFinset_inj]

Premises used: Set.toFinset_inj, Set.toFinset_empty
-- Module: Mathlib.Data.Fintype.Sets
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
rw₂ rw₃ : s = univ ↔ s = univ
⊢ s.toFinset = Finset.univ ↔ s = univ

Tactic:
rw [← coe_inj, coe_toFinset, coe_univ]

Premises used: Finset.coe_univ, Finset.coe_inj, Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype (↑{x : α | p x} : Type u_1)
h : ∀ (a : α), Membership.mem (γ := Finset α) (toFinset {x : α | p x}) a ↔ a ∈ filter p Finset.univ
⊢ toFinset {x : α | p x} = filter p Finset.univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : Fintype (↑{x : α | p x} : Type u_1)
a : α
⊢ Membership.mem (γ := Finset α) (toFinset {x : α | p x}) a ↔ a ∈ filter p Finset.univ

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
⊢ s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑(f '' s) : Type u_2)
⊢ (↑(f '' s).toFinset : Set β) = (↑(Finset.image f s.toFinset) : Set β)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : Fintype β
f : β → α
inst_2 : Fintype (↑(range f) : Type u_1)
h : ∀ (a : α), a ∈ (range f).toFinset ↔ a ∈ Finset.image f Finset.univ
⊢ (range f).toFinset = Finset.image f Finset.univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : Fintype β
f : β → α
inst_2 : Fintype (↑(range f) : Type u_1)
a : α
⊢ a ∈ (range f).toFinset ↔ a ∈ Finset.image f Finset.univ

Tactic:
simp