case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ (#α →₀ β) = max (lift (#α)) (lift (#β))

case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ (#α →₀ β) = max (lift (#α)) (lift (#β))
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ (#α →₀ β) = max (lift (#α)) (lift (#β))
cases fintypeOrInfinite α
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift (#β) ^ Fintype.card α = max (lift (#α)) (lift (#β))
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ (#α →₀ β) = max (lift (#α)) (lift (#β))
rw [mk_finsupp_lift_of_fintype]
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift (#β)
⊢ lift (#β) ^ Fintype.card α = max (lift (#α)) (lift (#β))
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift (#β) ^ Fintype.card α = max (lift (#α)) (lift (#β))
have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift (#β)
⊢ 1 ≤ Fintype.card α

α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift (#β)
⊢ lift (#α) ≤ ℵ₀
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift (#β)
⊢ lift (#β) ^ Fintype.card α = max (lift (#α)) (lift (#β))
rw [max_eq_right (le_trans _ this), power_nat_eq this]
no goals
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift (#β)
⊢ 1 ≤ Fintype.card α

α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift (#β)
⊢ lift (#α) ≤ ℵ₀
exacts [Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le]
no goals
case inr
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Infinite α
⊢ (#α →₀ β) = max (lift (#α)) (lift (#β))
apply mk_finsupp_lift_of_infinite