Lean4
instance commSemiring : CommSemiring Cardinal.{u} where
zero := 0
one := 1
add := (· + ·)
mul := (· * ·)
zero_add a := inductionOn a fun α => mk_congr <| Equiv.emptySum _ α
add_zero a := inductionOn a fun α => mk_congr <| Equiv.sumEmpty α _
add_assoc a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumAssoc α β γ
add_comm a b := inductionOn₂ a b fun α β => mk_congr <| Equiv.sumComm α β
zero_mul a := inductionOn a fun _ => mk_eq_zero _
mul_zero a := inductionOn a fun _ => mk_eq_zero _
one_mul a := inductionOn a fun α => mk_congr <| Equiv.uniqueProd α _
mul_one a := inductionOn a fun α => mk_congr <| Equiv.prodUnique α _
mul_assoc a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodAssoc α β γ
mul_comm a b := inductionOn₂ a b fun α β => mk_congr <| Equiv.prodComm α β
left_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodSumDistrib α β γ
right_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumProdDistrib α β γ
nsmul := nsmulRec
npow n c := c ^ (n : Cardinal)
npow_zero := power_zero
npow_succ n c := by rw [cast_succ, power_add, power_one]
natCast n := lift #(Fin n)
natCast_zero := rfl
natCast_succ n := cast_succ n
