[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = descFactorial ‖β‖ ‖α‖
[PROOFSTEP]
rw [Subsingleton.elim emb Embedding.fintype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = descFactorial ‖β‖ ‖α‖
[PROOFSTEP]
refine'
  Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) (fun α₁ α₂ h₂ e ih ↦ ?_) (?_)
    (fun γ h ih ↦ ?_) α
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₂
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) PEmpty
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) (Option γ)
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖
[PROOFSTEP]
clear! α
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖PEmpty ↪ β‖ = descFactorial ‖β‖ ‖PEmpty‖
[PROOFSTEP]
clear! α
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
clear! α
[GOAL]
case refine'_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖
[PROOFSTEP]
letI := Fintype.ofEquiv _ e.symm
[GOAL]
case refine'_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
this : Fintype α₁ := ofEquiv α₂ e.symm
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖
[PROOFSTEP]
rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
[GOAL]
case refine'_2
β : Type u_2
inst✝ : Fintype β
⊢ ‖PEmpty ↪ β‖ = descFactorial ‖β‖ ‖PEmpty‖
[PROOFSTEP]
rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]
[GOAL]
case refine'_2
β : Type u_2
inst✝ : Fintype β
⊢ ∃ x, ∀ (y : PEmpty ↪ β), y = x
[PROOFSTEP]
exact ⟨Embedding.ofIsEmpty, fun x ↦ FunLike.ext _ _ isEmptyElim⟩
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
classical
dsimp only at ih 
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β), card_sigma, ← ih]
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ, smul_eq_mul, mul_comm]
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
dsimp only at ih 
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = descFactorial ‖β‖ ‖γ‖
⊢ ‖Option γ ↪ β‖ = descFactorial ‖β‖ ‖Option γ‖
[PROOFSTEP]
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β), card_sigma, ← ih]
[GOAL]
case refine'_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = descFactorial ‖β‖ ‖γ‖
⊢ ∑ a : γ ↪ β, ‖↑(Set.range ↑a)ᶜ‖ = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
[PROOFSTEP]
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ, smul_eq_mul, mul_comm]
