-- Mathlib/Data/Fintype/CardEmbedding.lean
theorem card_embedding_eq {α β : Type*} [Fintype α] [Fintype β] [emb : Fintype (α ↪ β)] :
    ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Proof state:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ∑ i : γ ↪ β, ‖↑(Set.range ⇑i)ᶜ‖ = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖

Tactic:
simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
  Nat.nsmul_eq_mul, mul_comm]

Result:
no goals

Proof state:
case refine_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : (fun t [Fintype t] => ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₁
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

Tactic:
letI := Fintype.ofEquiv _ e.symm

Result:
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 ‖α₂‖

Proof state:
case refine_2
β : Type u_2
inst✝ : Fintype β
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

Tactic:
rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]

Result:
case refine_2
β : Type u_2
inst✝ : Fintype β
⊢ ∃ x, ∀ (y : PEmpty.{u_1 + 1} ↪ β), y = x

Proof state:
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 ‖α₂‖

Tactic:
rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]

Result:
no goals

Proof state:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Tactic:
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,
  Nat.nsmul_eq_mul, mul_comm]

Result:
no goals

Proof state:
case refine_2
β : Type u_2
inst✝ : Fintype β
⊢ ∃ x, ∀ (y : PEmpty.{u_1 + 1} ↪ β), y = x

Tactic:
exact ⟨Embedding.ofIsEmpty, fun x ↦ DFunLike.ext _ _ isEmptyElim⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
      (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α <;> dsimp only <;> clear! α

Result:
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.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Proof state:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : (fun t [Fintype t] => ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) γ
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Tactic:
dsimp only at ih

Result:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Proof state:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Tactic:
rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
    card_sigma, ← ih]

Result:
case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ∑ i : γ ↪ β, ‖↑(Set.range ⇑i)ᶜ‖ = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖