awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
⊢ image (fun (f : (a : α) → δ a) ↦ f a) (piFinset (δ := δ) t) ⊆ t a

Tactic:
image_subset_iff.2 fun _x hx ↦ mem_piFinset.1 hx _

Premises used: Iff.mpr, Fintype.mem_piFinset, Finset.image_subset_iff, Iff.mp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun (f : (a : α) → δ a) ↦ f a) (piFinset (δ := δ) t) = t a

Tactic:
(eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_

Premises used: Iff.mpr, Finset.mem_image, Fintype.eval_image_piFinset_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
refine : ∀ (x : δ a) (h : x ∈ t a), ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x
⊢ image (fun (f : (a : α) → δ a) ↦ f a) (piFinset (δ := δ) t) = t a

Tactic:
refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_

Premises used: Iff.mpr, Finset.mem_image, Fintype.eval_image_piFinset_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
x : δ a
h : x ∈ t a
choose : ∀ (f : (b : α) → a ≠ b → δ b) (hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b), ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x
⊢ ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x

Tactic:
choose f hf using ht
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun (b : α) ↦ if h : a = b then Eq.rec (motive := fun (x : α) (h : a = x) ↦ δ x) x h else f b h) ∈
    piFinset (δ := δ) t

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun (b : α) ↦ (if h : a = b then Eq.rec (motive := fun (x : α) (h : a = x) ↦ δ x) x h else f b h : δ b)) a = x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x

Tactic:
exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
t : Finset β
a : α
inl :
  Eq.{u_5 + 1} (α := Finset β) (image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ ∅))
    ∅
inr : ∀ (ht : t.Nonempty), image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t
⊢ image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
a : α
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨a⟩
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
a : α
this : Nonempty α
⊢ Eq.{u_5 + 1} (α := Finset β) (image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ ∅))
    ∅

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t

Tactic:
eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

Premises used: Fintype.eval_image_piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t

Tactic:
exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

Premises used: Fintype.eval_image_piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
s t : (a : α) → Finset (δ a)
⊢ (piFinset (δ := δ) fun (i : α) ↦ s i ∩ t i) = piFinset (δ := δ) s ∩ piFinset (δ := δ) t

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ {f ∈ piFinset (δ := δ) t | f a = x} = ∅

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
⊢ piFinset (δ := δ) (update (β := fun (a : α) ↦ Finset (δ a)) s i t) = {f ∈ piFinset (δ := δ) s | f i ∈ t}

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
a : δ i
ha : a ∈ s i
⊢ piFinset (δ := δ) (update (β := fun (a : α) ↦ Finset (δ a)) s i {a}) = {f ∈ piFinset (δ := δ) s | f i = a}

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : α → Type u_4
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : (a : α) → Fintype (β a)
⊢ ∀ (x : (a : α) → β a), Membership.mem (γ := Finset ((a : α) → β a)) (Fintype.piFinset (δ := β) fun (x : α) ↦ univ) x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_3
β : α → Type u_4
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : (a : α) → Fintype (β a)
⊢ Eq (α := Finset ((a : α) → β a)) (piFinset (δ := β) fun (a : α) ↦ univ) univ

Tactic:
rfl

Premises used: Finset.univ, Finset.map, Fintype.piFinset, rfl
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type ?u.30260
β : Type ?u.30263
inst : Fintype α
inst_1 : Fintype β
⊢ Fintype (α ↪ β)

Tactic:
exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)

Premises used: Fintype.ofEquiv, Equiv.subtypeInjectiveEquivEmbedding
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
⊢ Fintype (α ↪ β)

Tactic:
classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_3
β : α → Type u_4
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : (a : α) → Fintype (β a)
h :
  ∀ (a : (a : α) → Membership.mem (γ := Finset α) univ a → β a),
    Membership.mem (γ := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a))
        (pi (β := β) univ fun (a : α) ↦ univ) a ↔
      Membership.mem (γ := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a)) univ a
⊢ Eq (α := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a)) (pi (β := β) univ fun (a : α) ↦ univ) univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_3
β : α → Type u_4
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : (a : α) → Fintype (β a)
a : (a : α) → Membership.mem (γ := Finset α) univ a → β a
⊢ Membership.mem (γ := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a))
      (pi (β := β) univ fun (a : α) ↦ univ) a ↔
    Membership.mem (γ := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a)) univ a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
ι : Type u_3
inst : DecidableEq (ι → α)
s : Finset α
inst_1 : DecidableEq ι
inst_2 : Fintype ι
⊢ {f ∈ Fintype.piFinset (δ := fun (a : ι) ↦ α) fun (x : ι) ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
ι : Type u_3
inst : DecidableEq (ι → α)
s : Finset α
inst_1 : DecidableEq ι
inst_2 : Fintype ι
⊢ s.piDiag ι ⊆ Fintype.piFinset (δ := fun (a : ι) ↦ α) fun (x : ι) ↦ s

Tactic:
simp [← piFinset_filter_const]

Premises used: Finset.piFinset_filter_const
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
intro : ∀ (val : Fintype ι), (Set.pi (α := κ) univ t).Finite
⊢ (Set.pi (α := κ) univ t).Finite

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val : Fintype ι
⊢ ∀ (i : ι), (t i).Finite

Tactic:
ht
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val : Fintype ι
intro :
  ∀ (t : (i : ι) → Finset (κ i)),
    Set.Finite (α := (i : ι) → κ i) (Set.pi (α := κ) univ fun (i : ι) ↦ (↑(t i) : Set (κ i)))
⊢ (Set.pi (α := κ) univ t).Finite

Tactic:
lift t to ∀ d, Finset (κ d) using ht
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
val : Fintype ι
t : (i : ι) → Finset (κ i)
intro : (↑(Fintype.piFinset (δ := κ) t) : Set ((a : ι) → κ a)).Finite
⊢ Set.Finite (α := (i : ι) → κ i) (pi (α := κ) univ fun (i : ι) ↦ (↑(t i) : Set (κ i)))

Tactic:
rw [← Fintype.coe_piFinset]

Premises used: Fintype.coe_piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
val : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (↑(Fintype.piFinset (δ := κ) t) : Set ((a : ι) → κ a)).Finite

Tactic:
apply Finset.finite_toSet

Premises used: Finset.finite_toSet
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
val : Fintype ι
t : (i : ι) → Finset (κ i)
intro intro₁ intro₂ : (↑(Fintype.piFinset (δ := κ) t) : Set ((a : ι) → κ a)).Finite
⊢ Set.Finite (α := (i : ι) → κ i) (Set.pi (α := κ) univ fun (i : ι) ↦ (↑(t i) : Set (κ i)))

Tactic:
classical
    rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet

Premises used: Fintype.coe_piFinset, Finset.finite_toSet
-- Module: Mathlib.Data.Fintype.Pi
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ Set.Finite (α := (i : ι) → κ i) {f : (i : ι) → κ i | ∀ (i : ι), f i ∈ t i}

Tactic:
simpa [Set.pi] using Finite.pi ht

Premises used: Set.Finite.pi, Set.pi
-- Module: Mathlib.Data.Fintype.Pi
Goal:
δ : Type u_3
inst : Finite δ
κ : δ → Type u_4
s : Set ((d : δ) → κ d)
⊢ (∀ (d : δ), (eval (β := κ) d '' s).Finite) ↔ s.Finite

Tactic:
⟨fun h => (Finite.pi h).subset <| subset_pi_eval_image _ _, fun h _ => h.image _⟩

Premises used: Set.univ, Set.Finite.subset, Set.Finite.image, Function.eval, Iff.intro, Set.Finite.pi, Set.subset_pi_eval_image
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (iUnion (ι := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) s f)) x ↔
      x ∈ s ∪ ⋃ (i : Fin n), f i
⊢ iUnion (ι := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) s f) = s ∪ ⋃ (i : Fin n), f i

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
x : α
⊢ Membership.mem (γ := Set α) (iUnion (ι := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) s f)) x ↔
    x ∈ s ∪ ⋃ (i : Fin n), f i

Tactic:
simp [Fin.exists_iff_succ]

Premises used: Fin.exists_iff_succ
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (iUnion (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) f s)) x ↔
      x ∈ (⋃ (i : Fin n), f i) ∪ s
⊢ iUnion (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) f s) = (⋃ (i : Fin n), f i) ∪ s

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
x : α
⊢ Membership.mem (γ := Set α) (iUnion (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) f s)) x ↔
    x ∈ (⋃ (i : Fin n), f i) ∪ s

Tactic:
simp [Fin.exists_iff_castSucc, or_comm]

Premises used: Fin.exists_iff_castSucc, or_comm
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
cons :
  ∀ (x₀ : Set α) (x : (i : Fin n) → Set α),
    Eq.{u_1 + 1} (α := Set α) (⋃ (i : Fin (n + 1)), Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x i)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x 0 ∪
        iUnion (ι := Fin n) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x ∘ Fin.succ))
⊢ ⋃ (i : Fin (n + 1)), f i = f 0 ∪ iUnion (f ∘ Fin.succ)

Tactic:
cases f using Fin.consCases
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
x₀ : Set α
x : (i : Fin n) → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : Fin (n + 1)), Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x i)
    (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x 0 ∪
      iUnion (ι := Fin n) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x ∘ Fin.succ))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
snoc :
  ∀ (xs : (i : Fin n) → Set α) (x : Set α),
    Eq.{u_1 + 1} (α := Set α) (⋃ (i : Fin (n + 1)), Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x i)
      (iUnion (ι := Fin n) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x ∘ Fin.castSucc) ∪
        Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x (Fin.last n))
⊢ ⋃ (i : Fin (n + 1)), f i = iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)

Tactic:
cases f using Fin.snocCases
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
n : ℕ
xs : (i : Fin n) → Set α
x : Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : Fin (n + 1)), Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x i)
    (iUnion (ι := Fin n) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x ∘ Fin.castSucc) ∪
      Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x (Fin.last n))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : card β < card α
⊢ ∃ (x : α) (y : α), x ≠ y ∧ f x = f y

Tactic:
let ⟨x, _, y, _, h⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to h fun x _ => mem_univ (f x)
  ⟨x, y, h⟩

Premises used: Finset.mem_univ, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Exists, Ne, And, _private.0.Fintype.exists_ne_map_eq_of_card_lt.match_1, Exists.intro, Eq
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
h : Fintype.card β < Fintype.card α
⊢ IsEmpty (α ↪ β)

Tactic:
⟨fun f =>
    let ⟨_x, _y, ne, feq⟩ := Fintype.exists_ne_map_eq_of_card_lt f h
    ne <| f.injective feq⟩

Premises used: Fintype.exists_ne_map_eq_of_card_lt, False, IsEmpty.mk, Function.Embedding.injective, _private.0.Function.Embedding.isEmpty_of_card_lt.match_1, DFunLike.coe
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Sort u_4
β : Sort u_5
inst : Infinite α
inst_1 : Finite β
f : α → β
⊢ ∃ (x : α) (y : α), x ≠ y ∧ f x = f y

Tactic:
simpa [Injective, and_comm] using not_injective_infinite_finite f

Premises used: not_injective_infinite_finite, and_comm, Function.Injective
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
by_contra! : ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)), False
⊢ ∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)

Tactic:
by_contra! hf
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
intro : ∀ (val : Fintype β), False
⊢ False

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
val : Fintype β
⊢ ∀ (x : α), Membership.mem (γ := Finset α) (Finset.biUnion univ fun (y : β) ↦ (f ⁻¹' {y}).toFinset) x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
val : Fintype β
key : Fintype α := { elems := Finset.biUnion univ fun (y : β) ↦ (f ⁻¹' {y}).toFinset, complete := ⋯ }
⊢ False

Tactic:
key.false

Premises used: Fintype.false
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
val : Fintype β
key : Fintype α := { elems := Finset.biUnion univ fun (y : β) ↦ (f ⁻¹' {y}).toFinset, complete := ⋯ }
⊢ False

Tactic:
exact key.false

Premises used: Fintype.false
-- Module: Mathlib.Data.Fintype.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ :
  ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)), False
intro : ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) (val : Fintype β), False
intro₁ : ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) (val : Fintype β), False
⊢ ∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)

Tactic:
classical
    by_contra! hf
    cases nonempty_fintype β
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (Finset α) = HPow.hPow (α := ℕ) 2 (card α)

Tactic:
Finset.card_powerset Finset.univ

Premises used: Finset.univ, Fintype.card, Finset.powerset, Finset.card_powerset
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
⊢ (↑(powerset univ) : Set (Finset α)) = (↑univ : Set (Finset α))

Tactic:
simp [-coe_eq_univ]

Premises used: Finset.coe_eq_univ
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
h : ∀ (a : Finset α), Membership.mem (γ := Finset (Finset α)) {t : Finset α | t ⊆ s} a ↔ a ∈ s.powerset
⊢ {t : Finset α | t ⊆ s} = s.powerset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s a : Finset α
⊢ Membership.mem (γ := Finset (Finset α)) {t : Finset α | t ⊆ s} a ↔ a ∈ s.powerset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
rw : s.powerset = powerset univ ↔ s = univ
rw₁ rw₂ : s = univ ↔ s = univ
⊢ s.powerset = univ ↔ s = univ

Tactic:
rw [← Finset.powerset_univ, powerset_inj]

Premises used: Finset.powerset_inj, Finset.powerset_univ
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
k : ℕ
⊢ Membership.mem (γ := Finset (Finset α)) (powersetCard k univ) s ↔ #s = k

Tactic:
mem_powersetCard.trans <| and_iff_right <| subset_univ _

Premises used: and_iff_right, Finset.mem_powersetCard, Iff.trans, Finset.subset_univ
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
k : ℕ
h :
  ∀ (a : Finset α),
    Membership.mem (γ := Finset (Finset α)) {s : Finset α | #s = k} a ↔
      Membership.mem (γ := Finset (Finset α)) (powersetCard k univ) a
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) {s : Finset α | #s = k} (powersetCard k univ)

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
k : ℕ
a : Finset α
⊢ Membership.mem (γ := Finset (Finset α)) {s : Finset α | #s = k} a ↔
    Membership.mem (γ := Finset (Finset α)) (powersetCard k univ) a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
k : ℕ
⊢ card.{u_1} { s : Finset α // #s = k } = (card α).choose k

Tactic:
simp [Fintype.subtype_card, Finset.card_univ]

Premises used: Finset.card_univ, Fintype.subtype_card
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
s : Set α
⊢ Membership.mem (γ := Finset (Set α))
    (map (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2) coeEmb)
      Finset.univ)
    s

Tactic:
mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.coe_filter, Finset.univ, Membership.mem, And.intro, Exists.intro, Finset.mem_map, Finset.filter, Eq.trans
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
s : Set α
refine : {x : α | Membership.mem (γ := Finset α) Finset.univ x ∧ x ∈ s} = s
⊢ Membership.mem (γ := Finset (Set α))
    (map (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2) coeEmb)
      Finset.univ)
    s

Tactic:
refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.univ, Membership.mem, And.intro, Exists.intro, Finset.mem_map, Finset.filter
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
s : Set α
⊢ {x : α | Membership.mem (γ := Finset α) Finset.univ x ∧ x ∈ s} = s

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
s : Set α
refine : {x : α | Membership.mem (γ := Finset α) Finset.univ x ∧ x ∈ s} = s
⊢ Membership.mem (γ := Finset (Set α))
    (map (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2) coeEmb)
      Finset.univ)
    s

Tactic:
classical
    refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
    simp
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Finite α
intro : ∀ (val : Fintype α), Finite.{u_1 + 1} (Set α)
⊢ Finite.{u_1 + 1} (Set α)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Finite α
val : Fintype α
⊢ Finite.{u_1 + 1} (Set α)

Tactic:
infer_instance
-- Module: Mathlib.Data.Fintype.Powerset
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (Set α) = HPow.hPow (α := ℕ) 2 (card α)

Tactic:
(Finset.card_map _).trans (Finset.card_powerset _)

Premises used: Finset.univ, Finset.card_map, Finset.map, Fintype.card, Eq.trans, Finset.card_powerset
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_2)
inst_2 : Fintype (↑(s ×ˢ t) : Type (max u_1 u_2))
h : ∀ (a : α × β), a ∈ (s ×ˢ t).toFinset ↔ a ∈ s.toFinset ×ˢ t.toFinset
⊢ (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_2)
inst_2 : Fintype (↑(s ×ˢ t) : Type (max u_1 u_2))
a : α × β
⊢ a ∈ (s ×ˢ t).toFinset ↔ a ∈ s.toFinset ×ˢ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑s.offDiag : Type u_1)
⊢ ∀ (a : α × α), a ∈ s.offDiag.toFinset ↔ a ∈ s.toFinset.offDiag

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : Fintype β
x : α × β
a : α
b : β
⊢ (a, b) ∈ SProd.sprod (α := Finset α) (β := Finset β) univ univ

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
⊢ SProd.sprod (α := Finset α) (β := Finset β) univ univ = univ

Tactic:
rfl

Premises used: Finset.univ, rfl