-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem prod_eq_of_fintype {α : Type u} [h : Fintype α] (f : α → Cardinal.{v}) :
    prod f = Cardinal.lift.{u} (∏ i, f i)

Proof state:
case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)

Tactic:
rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]

Result:
no goals

Proof state:
α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)

Tactic:
refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)

Result:
case refine_1
α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)

case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)

case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : Option α, f i)

Proof state:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i : β, f i)

Tactic:
rw [← e.prod_comp f, ← h]

Result:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i => f (e i)

Proof state:
case refine_1
α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)

Tactic:
intro α β hβ e h f

Result:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : β, f i)

Proof state:
case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)

Tactic:
intro f

Result:
case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)

Proof state:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i => lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a => f (some a)

Tactic:
simp only [lift_id]

Result:
no goals

Proof state:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i => f (e i)

Tactic:
exact mk_congr (e.piCongrLeft _).symm

Result:
no goals

Proof state:
α : Type u
h : Fintype α
f : α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : α, f i)

Tactic:
revert f

Result:
α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)

Proof state:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : β, f i)

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

Result:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i : β, f i)

Proof state:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : Option α, f i)

Tactic:
rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax.{v, u}, mk_out, ←
    Cardinal.prod, lift_prod, Fintype.prod_option, lift_mul, ← h fun a => f (some a)]

Result:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i => lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a => f (some a)

Proof state:
case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : Option α, f i)

Tactic:
intro α hα h f

Result:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : Option α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i : Option α, f i)