/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.fintype.sigma
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Finset.Sigma

/-!
# fintype instances for sigma types
-/


open Function

open Nat

universe u v

variable {
α: Type ?u.11
α 
β: Type ?u.14
β 
γ: Type ?u.17
γ : 
Type _: Type (?u.2+1)
Type _}

open Finset Function

instance: {α : Type u_1} → (β : α → Type u_2) → [inst : Fintype α] → [inst : (a : α) → Fintype (β a)] → Fintype (Sigma β)
instance {
α: Type ?u.20
α : 
Type _: Type (?u.20+1)
Type _} (
β: α → Type ?u.25
β : 
α: Type ?u.20
α → 
Type _: Type (?u.25+1)
Type _) [
Fintype: Type ?u.28 → Type ?u.28
Fintype 
α: Type ?u.20
α] [∀ 
a: ?m.32
a, 
Fintype: Type ?u.35 → Type ?u.35
Fintype (
β: α → Type ?u.25
β 
a: ?m.32
a)] : 
Fintype: Type ?u.39 → Type ?u.39
Fintype (
Sigma: {α : Type ?u.41} → (α → Type ?u.40) → Type (max?u.41?u.40)
Sigma 
β: α → Type ?u.25
β) :=
  ⟨
univ: {α : Type ?u.58} → [inst : Fintype α] → Finset α
univ.
sigma: {ι : Type ?u.88} → {α : ι → Type ?u.87} → Finset ι → ((i : ι) → Finset (α i)) → Finset ((i : ι) × α i)
sigma fun 
_: ?m.104
_ => 
univ: {α : Type ?u.106} → [inst : Fintype α] → Finset α
univ, fun ⟨
a: α
a, 
b: β a
b⟩ => by
Goals accomplished! 🐙 
α✝: Type ?u.11

β✝: Type ?u.14

γ: Type ?u.17

α: Type ?u.20

β: α → Type ?u.25

inst✝¹: Fintype α

inst✝: (a : α) → Fintype (β a)

x✝: Sigma β

a: α

b: β a

{ fst := a, snd := b } ∈ Finset.sigma univ fun x => univsimp
Goals accomplished! 🐙⟩

@[simp]
theorem 
Finset.univ_sigma_univ: ∀ {α : Type u_1} {β : α → Type u_2} [inst : Fintype α] [inst_1 : (a : α) → Fintype (β a)],
  (Finset.sigma univ fun a => univ) = univ
Finset.univ_sigma_univ {
α: Type ?u.777
α : 
Type _: Type (?u.777+1)
Type _} {
β: α → Type u_2
β : 
α: Type ?u.777
α → 
Type _: Type (?u.782+1)
Type _} [
Fintype: Type ?u.785 → Type ?u.785
Fintype 
α: Type ?u.777
α] [∀ 
a: ?m.789
a, 
Fintype: Type ?u.792 → Type ?u.792
Fintype (
β: α → Type ?u.782
β 
a: ?m.789
a)] :
    ((
univ: {α : Type ?u.799} → [inst : Fintype α] → Finset α
univ : 
Finset: Type ?u.798 → Type ?u.798
Finset 
α: Type ?u.777
α).
sigma: {ι : Type ?u.839} → {α : ι → Type ?u.838} → Finset ι → ((i : ι) → Finset (α i)) → Finset ((i : ι) × α i)
sigma fun 
a: ?m.847
a => (
univ: {α : Type ?u.851} → [inst : Fintype α] → Finset α
univ : 
Finset: Type ?u.850 → Type ?u.850
Finset (
β: α → Type ?u.782
β 
a: ?m.847
a))) = 
univ: {α : Type ?u.895} → [inst : Fintype α] → Finset α
univ :=
  
rfl: ∀ {α : Sort ?u.1029} {a : α}, a = a
rfl
#align finset.univ_sigma_univ 
Finset.univ_sigma_univ: ∀ {α : Type u_1} {β : α → Type u_2} [inst : Fintype α] [inst_1 : (a : α) → Fintype (β a)],
  (Finset.sigma univ fun a => univ) = univ
Finset.univ_sigma_univ

instance 
PSigma.fintype: {α : Type u_1} → {β : α → Type u_2} → [inst : Fintype α] → [inst : (a : α) → Fintype (β a)] → Fintype ((a : α) ×' β a)
PSigma.fintype {
α: Type ?u.1082
α : 
Type _: Type (?u.1082+1)
Type _} {
β: α → Type ?u.1087
β : 
α: Type ?u.1082
α → 
Type _: Type (?u.1087+1)
Type _} [
Fintype: Type ?u.1090 → Type ?u.1090
Fintype 
α: Type ?u.1082
α] [∀ 
a: ?m.1094
a, 
Fintype: Type ?u.1097 → Type ?u.1097
Fintype (
β: α → Type ?u.1087
β 
a: ?m.1094
a)] :
    
Fintype: Type ?u.1101 → Type ?u.1101
Fintype (Σ'
a: ?m.1106
a, 
β: α → Type ?u.1087
β 
a: ?m.1106
a) :=
  
Fintype.ofEquiv: {β : Type ?u.1117} → (α : Type ?u.1116) → [inst : Fintype α] → α ≃ β → Fintype β
Fintype.ofEquiv 
_: Type ?u.1116
_ (
Equiv.psigmaEquivSigma: {α : Type ?u.1151} → (β : α → Type ?u.1150) → (i : α) ×' β i ≃ (i : α) × β i
Equiv.psigmaEquivSigma 
_: ?m.1152 → Type ?u.1150
_).
symm: {α : Sort ?u.1155} → {β : Sort ?u.1154} → α ≃ β → β ≃ α
symm
#align psigma.fintype 
PSigma.fintype: {α : Type u_1} → {β : α → Type u_2} → [inst : Fintype α] → [inst : (a : α) → Fintype (β a)] → Fintype ((a : α) ×' β a)
PSigma.fintype