case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ (#α →₀ β) ≤ max (lift (#α)) (lift (#β))

case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ max (lift (#α)) (lift (#β)) ≤ (#α →₀ β)
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ (#α →₀ β) = max (lift (#α)) (lift (#β))
apply le_antisymm
no goals
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ (#α →₀ β) ≤ max (lift (#α)) (lift (#β))
calc
  (#α →₀ β) ≤ (#Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
  _ = (#α × β) := mk_finset_of_infinite _
  _ = max (lift.{v} (#α)) (lift.{u} (#β)) :=
    by rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
no goals
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ (#α × β) = max (lift (#α)) (lift (#β))
rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift (#α) ≤ lift (#α →₀ β)

case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift (#β) ≤ lift (#α →₀ β)
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ max (lift (#α)) (lift (#β)) ≤ (#α →₀ β)
apply max_le <;> rw [← lift_id (#α →₀ β), ← lift_umax]
case a.h₁.intro
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift (#α) ≤ lift (#α →₀ β)
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift (#α) ≤ lift (#α →₀ β)
cases' exists_ne (0 : β) with b hb
no goals
case a.h₁.intro
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift (#α) ≤ lift (#α →₀ β)
exact lift_mk_le.{u, max u v, v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
inhabited_h : Inhabited α
⊢ lift (#β) ≤ lift (#α →₀ β)
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift (#β) ≤ lift (#α →₀ β)
inhabit α
no goals
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
inhabited_h : Inhabited α
⊢ lift (#β) ≤ lift (#α →₀ β)
exact lift_mk_le.{v, max u v, u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩