case a
α β : Type u
a : Cardinal
b : Cardinal
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
α β : Type u
a : Cardinal
b : Cardinal
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ↑toNat (lift a + lift b) = ↑toNat a + ↑toNat b
apply Cardinal.natCast_injective
case a
α β : Type u
a : Cardinal
b : Cardinal
hb : b < ℵ₀
ha : lift a < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
case a
α β : Type u
a : Cardinal
b : Cardinal
ha : a < ℵ₀
hb : b < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
replace ha : lift.{v, u} a < ℵ₀ := by rwa [lift_lt_aleph0]
case a
α β : Type u
a : Cardinal
b : Cardinal
ha : lift a < ℵ₀
hb : lift b < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
case a
α β : Type u
a : Cardinal
b : Cardinal
hb : b < ℵ₀
ha : lift a < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
replace hb : lift.{u, v} b < ℵ₀ := by rwa [lift_lt_aleph0]
no goals
case a
α β : Type u
a : Cardinal
b : Cardinal
ha : lift a < ℵ₀
hb : lift b < ℵ₀
⊢ ↑(↑toNat (lift a + lift b)) = ↑(↑toNat a + ↑toNat b)
rw [Nat.cast_add, ← toNat_lift.{v, u} a, ← toNat_lift.{u, v} b, cast_toNat_of_lt_aleph0 ha,
  cast_toNat_of_lt_aleph0 hb, cast_toNat_of_lt_aleph0 (add_lt_aleph0 ha hb)]
no goals
α β : Type u
a : Cardinal
b : Cardinal
ha : a < ℵ₀
hb : b < ℵ₀
⊢ lift a < ℵ₀
rwa [lift_lt_aleph0]
no goals
α β : Type u
a : Cardinal
b : Cardinal
hb : b < ℵ₀
ha : lift a < ℵ₀
⊢ lift b < ℵ₀
rwa [lift_lt_aleph0]