α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = descFactorial ‖β‖ ‖α‖
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = descFactorial ‖β‖ ‖α‖
rw [Subsingleton.elim emb Embedding.fintype]
case refine'_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = descFactorial ‖β‖ ‖t‖) α₁
⊢ ‖α₂ ↪ β‖ = descFactorial ‖β‖ ‖α₂‖

case refine'_2
β : Type u_2
inst✝ : Fintype β
⊢ ‖PEmpty ↪ β‖ = descFactorial ‖β‖ ‖PEmpty‖

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