[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α × β)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Finite (α × β)
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Finite (α × β)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α ⊕ β)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Finite (α ⊕ β)
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Finite (α ⊕ β)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
β : α → Type u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) × β a)
[PROOFSTEP]
letI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
β : α → Type u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this : Fintype α := Fintype.ofFinite α
⊢ Finite ((a : α) × β a)
[PROOFSTEP]
letI := fun a => Fintype.ofFinite (β a)
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
β : α → Type u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype α := Fintype.ofFinite α
this : (a : α) → Fintype (β a) := fun a => Fintype.ofFinite (β a)
⊢ Finite ((a : α) × β a)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Finite (Set α)
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
val✝ : Fintype α
⊢ Finite (Set α)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : α → Sort u_5
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)
[PROOFSTEP]
haveI := Fintype.ofFinite (PLift α)
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : α → Sort u_5
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this : Fintype (PLift α)
⊢ Finite ((a : α) → β a)
[PROOFSTEP]
haveI := fun a => Fintype.ofFinite (PLift (β a))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : α → Sort u_5
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype (PLift α)
this : (a : α) → Fintype (PLift (β a))
⊢ Finite ((a : α) → β a)
[PROOFSTEP]
exact Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a))) (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
n : ℕ
⊢ Finite (Vector α n)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
n : ℕ
this : Fintype α
⊢ Finite (Vector α n)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
⊢ Finite (α ↪ β)
[PROOFSTEP]
cases' isEmpty_or_nonempty (α ↪ β) with _ h
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)
[PROOFSTEP]
apply Finite.of_subsingleton
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)
[PROOFSTEP]
refine' h.elim fun f => _
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
⊢ Finite (α ↪ β)
[PROOFSTEP]
haveI : Finite α := Finite.of_injective _ f.injective
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
this : Finite α
⊢ Finite (α ↪ β)
[PROOFSTEP]
exact Finite.of_injective _ FunLike.coe_injective
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
e₁ e₂ : α ≃ β
h : Equiv.toEmbedding e₁ = Equiv.toEmbedding e₂
⊢ ∀ (x : α), ↑e₁ x = ↑e₂ x
[PROOFSTEP]
convert FunLike.congr_fun h using 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
⊢ Finite (Sym α n)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
this : Fintype α
⊢ Finite (Sym α n)
[PROOFSTEP]
infer_instance
