α✝ β α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
α✝ β α : Type u
h : Fintype α
f : α → Cardinal
⊢ prod f = lift (∏ i : α, f i)
revert f
case refine'_1
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)) → ∀ (f : β → Cardinal), prod f = lift (∏ i : β, f i)

case refine'_2
α✝ β α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty → Cardinal), prod f = lift (∏ i : PEmpty, f i)

case refine'_3
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)) →
      ∀ (f : Option α → Cardinal), prod f = lift (∏ i : Option α, f i)
α✝ β α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
refine' Fintype.induction_empty_option _ _ _ α (h_fintype := h)
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : β → Cardinal
⊢ prod f = lift (∏ i : β, f i)
case refine'_1
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)) → ∀ (f : β → Cardinal), prod f = lift (∏ i : β, f i)
intro α β hβ e h f
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : β → Cardinal
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift (∏ i : β, f i)
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : β → Cardinal
⊢ prod f = lift (∏ i : β, f i)
letI := Fintype.ofEquiv β e.symm
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : β → Cardinal
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i => f (↑e i)
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : β → Cardinal
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift (∏ i : β, f i)
rw [← e.prod_comp f, ← h]
no goals
case refine'_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : β → Cardinal
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i => f (↑e i)
exact mk_congr (e.piCongrLeft _).symm
case refine'_2
α✝ β α : Type u
h : Fintype α
f : PEmpty → Cardinal
⊢ prod f = lift (∏ i : PEmpty, f i)
case refine'_2
α✝ β α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty → Cardinal), prod f = lift (∏ i : PEmpty, f i)
intro f
no goals
case refine'_2
α✝ β α : Type u
h : Fintype α
f : PEmpty → Cardinal
⊢ prod f = lift (∏ i : PEmpty, f i)
rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
case refine'_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : Option α → Cardinal
⊢ prod f = lift (∏ i : Option α, f i)
case refine'_3
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)) →
      ∀ (f : Option α → Cardinal), prod f = lift (∏ i : Option α, f i)
intro α hα h f
case refine'_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : Option α → Cardinal
⊢ (lift (f none) * prod fun i => lift (f (some i))) = lift (f none) * prod fun a => f (some a)
case refine'_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : Option α → Cardinal
⊢ prod f = lift (∏ i : Option α, f i)
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)]
no goals
case refine'_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal), prod f = lift (∏ i : α, f i)
f : Option α → Cardinal
⊢ (lift (f none) * prod fun i => lift (f (some i))) = lift (f none) * prod fun a => f (some a)
simp only [lift_id]